§02Inside the lab

No filled twin set: selection shows as accent-subtle behind the outline icon. Animated icons are refused except progress, which owns its motion. Sizes 16, 20, 24; optical size stays on the 24 grid.

• A checkbox for something that counts when the form is sent.
• A switch for something that happens as soon as it is moved.
• A switch that needs a save button is the wrong control for the job.

Fields that appear conditionally are announced to assistive technology and never discard what was entered if hidden again. Required fields are marked as required; optional fields are marked as optional; nothing is inferred from an asterisk alone.

Entered information is preserved across navigation and expiry; drafts save where the work is long. Submission disables the action until the response lands, and cancellation and reset both confirm before discarding.

• open
• checking now
• reduced, waiting on premises
• closable in one click
• proved
• disproved

• Queued, pending, processing: named in the run states under Status.
• Offline, reconnecting, stale, synchronising: named in the connection states under Status.
• Draft, dirty, saving, saved, conflicted: the editing cycle; conflicts name both versions.
• Dragging, drop-valid, drop-invalid: the dragged thing stays legible throughout.
• Expanded and collapsed: disclosure groups animate height at --duration-default.

Send with Enter, and start a new line with Shift + Enter.

Ready to close?

1. Daedalian’s agent proved softmax-sum-one

   4 wk. ago

   Accepted by the kernel in 41 s

2. Ajax tried attn-convex-hull

   4 wk. ago

   Rejected: the proof still contains sorry
3. …

   Checking a proof of rope-angle-add

   4 wk. ago

Last proof accepted 4 wk. ago.

• compactionChanged

  Revision 2

  null

  Revision 3

  {
    "plugin": "outline"
  }

The softmax weights $\htmlData{mx=9}{\frac{\htmlData{mx=3}{e^{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{i})}}}}{\htmlData{mx=8}{\sum_{j} \htmlData{mx=7}{e^{\htmlData{mx=6}{\htmlData{mx=4}{w}(\htmlData{mx=5}{j})}}}}}}$ are positive and add up to $1$.

(n k)Binomial coefficient

“n choose k”: the number of ways to pick k things from n. (Nat.choose n k)

·Multiplication

choose(n, k) times k!. (Nat.choose n k * k !)

=Equality

choose(n, k) · k! · (n − k)! and n! are the same. (Nat.choose n k * k ! * (n - k) ! = n !)

n!Factorial

k! = 1 · 2 · … · k. (k !)

-Subtraction

n minus k. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (n - k)

1. #12session.createdAda · 10 minutes ago

   Session started

2. #13configuration.changedAda · 2 minutes ago

   Revision 3 changes compaction

   Record

   json

   Copy

   {
     "revision": 3,
     "previousRevision": 2,
     "fields": [
       "compaction"
     ]
   }

3. #14configuration.activation_failedFailedWorker · just now

   Revision 2 stays in force

   Record

   json

   Copy

   {
     "reason": "The build is rejected, not verified"
   }

• Body text at 4.5:1 against its background, larger text at 3:1.
• A visible focus ring on everything focusable, never removed.
• Colour is never the only carrier of meaning; each state has a word.
• A pointer target is at least 24 by 24 pixels (WCAG 2.2 AA), 44 preferred; inline text controls, visually-hidden native inputs with compliant visible controls, and focus-revealed chrome are the exceptions.
• Motion collapses to nothing when the reader’s system asks it to.
• One main landmark a page, and a skip link before it.
• No information by timing alone: nothing flashes, expires, or moves without a pause, and authentication never depends on solving a puzzle fast.
• Announcements use live regions with manners: status changes politely, errors assertively; decorative motion never announces.

• High contrast is a third theme, applied automatically from prefers-contrast: more: pure black, white text, white borders, no shadows. An explicit light/dark choice always wins.
• Density is one comfortable setting. A compact density waits on density tokens; until then no component shrinks targets to fake one.
• No flash: a blocking script in the document head applies the stored choice, the contrast preference, or the colour-scheme preference before first paint.
• Switching never moves layout or loses state: values swap under stable structure, verified across every section.

Deletion names what goes and what survives, then confirms. Where recovery is possible, undo beats confirmation; where it is not, the dialog says so. Costs, limits, and restrictions are stated before commitment, never after.

Memory attachments, grants, and invitations show who can see what before anything is shared. Keys and tokens render masked with deliberate reveal. Unavailable features read differently from unauthorised ones.

Pseudolocalisation (wrapping strings in ⟦…⟧ with padding) runs over this showcase before any translation ships. Dates, times, numbers, currencies, and units format by locale; names and addresses never assume one shape.

Use the component that exists. A new pattern must prove the old ones cannot stretch.

What a component cannot do is written beside what it can. Limits are documentation.

Colour, space, type and motion come from tokens. Applications change values, never forks.

Empty, loading, error, and disabled are designed beside the default, and all are shown here.

Visual hierarchy comes from size, weight, position and spacing, not colour count. Ink is the main action; cobalt marks where you are and what you can follow; semantic colours speak only for status, never for decoration.

evals, meet, bode, and code are wordmarks in the same monospace treatment, never separate lockups. Co-branding on interface surfaces is refused; partner marks appear only on landing pages outside the interface.

Acceptable: a token-coloured diagram explaining a state; a real screenshot with a caption. Unacceptable: decorative gradients, mascot art, stock photography. Two each, no more needed: the interface itself carries the brand.

• A cobalt bar marking exactly the current page in a sidebar.
• A numbered figure whose caption names what the diagram shows.
• Danger red with the word Failed beside a run row.

• A gradient hero behind the login form.
• Green text celebrating a metric that is not a status.
• An icon-only delete button with no accessible name.

Animations run at --duration-fast 120ms to --duration-slow 300ms on transform, opacity, colour, border, and shadow only — never on layout properties, with one named exception: metered fills animate width inside fixed tracks, which moves nothing around them. Lists past a screenful virtualise (virtual-list). Skeletons reserve space so loading never shifts layout.

Failed assets show fallbacks, missing data shows empty states, slow operations show progress with cancellation. Optimistic updates roll back visibly. Baseline content works without JavaScript-driven enhancement.

• Budget: 79 components in ~860KB of source, ceiling 1MB; growth past it splits the package, not the budget.
• Tree-shaking: per-component exports with CSS-only side effects; applications import paths, never barrels.
• Lazy loading: lists virtualise past a screenful; images below the fold load lazily at twice the displayed size.
• Fonts: Geist and Geist Mono variable woff2, about 58KB each, self-hosted through next/font; icons: lucide imports per icon, no sprite.
• Retries, timeouts, and races: every remote operation names its timeout, cancels cleanly, and never applies a stale response over a fresh one.

Proposals arrive as small PRs against packages/ui with a showcase section included. A new component must show evidence: two consuming uses and no existing component that stretches. Duplicates are removed, not adapted.

Releases follow semantic versioning on a weekly cadence. Breaking changes ship with a migration guide and a one-release deprecation window. Retired components leave the showcase with a changelog entry pointing at the replacement.

A defect report names the section, the state, and the theme. Support burden and adoption are reviewed under Adoption; ineffective features are retired, not maintained.

Props are additive within a major version. A removal or rename ships deprecated for one release with a migration guide, then leaves with a changelog entry. Automation covers renames where a codemod is reliable; the guide covers the rest.

A product that cannot use the system component records an approved divergence with its reason and review date. Unapproved variants found in review are promoted into the system or removed.

The roadmap is the open proposal queue; funding and staffing are the maintainer’s capacity, reviewed quarterly. Third-party dependencies need approval and carry their licenses with them; the package itself ships under the repository license with attribution in the readme. Triage is weekly: defects first, then proposals, then polish. Decision records live beside the code they decided.