/* The release universe (universe.html). Explorer layout after the Plectis
   universe map's full-window explorer (ai_workflow commit 4b1ebab611,
   tools/meta/dissemination/maths_site_assets/maths.css): the reading panel on
   the left, the drawing in the rest of the window, one flat ground.
   The --u-* tokens are what the canvas reads; they are plain colours (the
   canvas cannot resolve color-mix), set from the atlas palette in atlas.css.
   Colour belongs to evidence: steel for Lean, brick for the other machine
   checks; structure stays in low-chroma greys. */

/* The tokens also reach the list of every family under the map, whose rows carry
   the same state dots. */
[data-universe], .u-band--index {
  --u-ground: #f8f0e2;
  --u-ink: #191520;
  --u-muted: #544d5d;
  --u-faint: #6d6473;
  --u-struct: #9c9083;
  --u-struct-soft: #c9bba7;
  /* A paper's ring inside an open family, which tells which results it holds:
     3.8:1 against the ground (struct alone is 2.8:1 in this scheme). */
  --u-paper: #85786a;
  --u-cloud: rgba(25, 21, 32, 0.045);
  --u-slice: rgba(25, 21, 32, 0.05);
  --u-fibre: rgba(25, 21, 32, 0.36);
  --u-cites: #9a322c;
  --u-cited: #6d6473;
  --u-steel: #1f4a73;
  --u-brick: #9a322c;
  --u-paired: #5b7f9f;
  --u-plate: #fffdf7;
  --u-plate-rule: #d9c7ae;
  --u-focus: #191520;
  --u-t-all: #2a5982;
  --u-t-part: #86a8c6;
  --u-t-other: #8a77a8;
  --u-t-split: #b5801f;
  --u-t-none: #978a7c;
  --u-t-unread: #978a7c;
  --u-e-part: #557ea4;
  --u-e-none: #85786a;
  --u-e-unread: #85786a;
  --u-e-split: #9a6c16;
  --u-panel-w: clamp(340px, 26vw, 430px);
}
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) [data-universe], :root:not([data-theme="light"]) .u-band--index {
    --u-ground: #1c1526;
    --u-ink: #f2e6d4;
    --u-muted: #bcb8c6;
    --u-faint: #a6a2b1;
    --u-struct: #7c7585;
    --u-struct-soft: #4d4757;
    --u-paper: #7c7585;
    --u-cloud: rgba(242, 230, 212, 0.05);
    --u-slice: rgba(242, 230, 212, 0.055);
    --u-fibre: rgba(242, 230, 212, 0.40);
    --u-cites: #e18a79;
    --u-cited: #bcb8c6;
    --u-steel: #a9cdea;
    --u-brick: #e18a79;
    --u-paired: #7fa3c2;
    --u-plate: #272132;
    --u-plate-rule: #484251;
    --u-focus: #fff7ea;
    --u-t-all: #7fb4e8;
    --u-t-part: #6c8399;
    --u-t-other: #a493c6;
    --u-t-split: #dba84c;
    --u-t-none: #8a8396;
    --u-t-unread: #8a8396;
  }
}
:root[data-theme="dark"] [data-universe], :root[data-theme="dark"] .u-band--index {
  --u-ground: #1c1526;
  --u-ink: #f2e6d4;
  --u-muted: #bcb8c6;
  --u-faint: #a6a2b1;
  --u-struct: #7c7585;
  --u-struct-soft: #4d4757;
  --u-paper: #7c7585;
  --u-cloud: rgba(242, 230, 212, 0.05);
  --u-slice: rgba(242, 230, 212, 0.055);
  --u-fibre: rgba(242, 230, 212, 0.40);
  --u-cites: #e18a79;
  --u-cited: #bcb8c6;
  --u-steel: #a9cdea;
  --u-brick: #e18a79;
  --u-paired: #7fa3c2;
  --u-plate: #272132;
  --u-plate-rule: #484251;
  --u-focus: #fff7ea;
  --u-t-all: #7fb4e8;
  --u-t-part: #6c8399;
  --u-t-other: #a493c6;
  --u-t-split: #dba84c;
  --u-t-none: #8a8396;
  --u-t-unread: #8a8396;
}

main.u-main { padding: 0; max-width: none; }
.u-explorer {
  --u-gutter: max(24px, calc((100vw - 1600px) / 2));
  position: relative;
  display: grid;
  grid-template-columns: calc(var(--u-panel-w) + var(--u-gutter) - 20px) minmax(0, 1fr);
  grid-template-rows: minmax(0, 1fr);
  height: calc(100vh - var(--top-h, 64px) - 1px);
  height: calc(100dvh - var(--top-h, 64px) - 1px);
  min-height: 520px;
  background: var(--page);
  border-bottom: 1px solid var(--rule);
}
.u-visually-hidden {
  position: absolute; width: 1px; height: 1px; padding: 0; margin: -1px; overflow: hidden;
  clip: rect(0 0 0 0); white-space: nowrap; border: 0;
}

/* ---- Panel ---------------------------------------------------------- */
.u-panel {
  display: flex; flex-direction: column; min-height: 0;
  border-right: 1px solid var(--rule);
  background: var(--page);
}
.u-panel__head { padding: 16px 20px 12px var(--u-gutter); border-bottom: 1px solid var(--rule); }
.u-panel__body { overflow-y: auto; overscroll-behavior: contain; padding: 4px 20px 32px var(--u-gutter); min-height: 0; flex: 1; scrollbar-gutter: stable; }
.u-trail { display: flex; flex-wrap: wrap; align-items: baseline; gap: 2px 6px; font: 500 var(--fs-small)/1.4 var(--sans); color: var(--muted); min-height: 1.4em; }
.u-trail .u-go.u-crumb { width: auto; }
.u-crumb { font: inherit; color: var(--steel-text); background: none; border: 0; padding: 0; cursor: pointer; text-decoration: underline; text-decoration-color: color-mix(in oklab, currentColor 35%, transparent); text-underline-offset: 3px; }
.u-crumb:hover { text-decoration-color: currentColor; }
.u-crumb.is-here { color: var(--ink-soft); text-decoration: none; cursor: default; }
.u-crumb-sep { color: var(--faint); }
.u-title { font: 500 1.625rem/1.18 var(--serif); letter-spacing: -0.01em; margin: 2px 0 14px; color: var(--ink); text-wrap: balance; }
.u-title--deep { font-size: 1.25rem; font-weight: 600; letter-spacing: 0; }
.u-trail[hidden] { display: none; }
.u-step { display: flex; align-items: center; gap: 10px; margin: 6px 0 0; font: 400 var(--fs-small)/1.4 var(--sans); color: var(--muted); }
.u-step[hidden] { display: none; }
.u-step__pos { flex: 1 1 auto; min-width: 0; text-align: center; font-variant-numeric: tabular-nums; }
.u-step__go { flex: none; padding: 2px 8px; border: 1px solid var(--rule); border-radius: var(--r-sm); font: inherit; color: var(--ink); background: var(--surface); }
.u-step__go.u-go { width: auto; cursor: pointer; }
.u-step__go.u-go:hover { border-color: var(--rule-strong); }
.u-step__go.u-go:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 1px; }
.u-step__go.is-end { opacity: 0.35; }
.u-step__go--prev::before { content: "\2190\00a0"; }
.u-step__go--next::after { content: "\00a0\2192"; }
.u-ground { font: 400 var(--fs-small)/1.5 var(--sans); color: var(--ink-soft); margin: -6px 0 14px; max-width: 46ch; text-wrap: pretty; }
.u-ground[hidden] { display: none; }
.u-nobr { display: inline-block; } /* whole where it fits, wrapping inside itself where its line is narrower */
.u-band__note { font: 400 var(--fs-body)/1.6 var(--sans); color: var(--ink-soft); margin: 14px 0 0; max-width: 66ch; }
.u-band__note a { color: var(--steel-text); font-weight: 600; }
.u-title--code { font: 600 1.05rem/1.3 var(--mono); overflow-wrap: anywhere; }
.u-search__in {
  width: 100%; font: 400 var(--fs-body)/1.3 var(--sans); color: var(--ink);
  background: var(--surface); border: 1px solid var(--rule-control); border-radius: var(--r-md);
  padding: 8px 11px;
}
.u-search__in::placeholder { color: var(--faint); }
.u-search__in:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 1px; }

.u-view > p:not([class]), .u-evidence p:not([class]) { font: 400 var(--fs-meta)/1.55 var(--sans); color: var(--ink-soft); }
.u-lede { font: 400 var(--fs-base)/1.55 var(--serif); color: var(--ink); margin: 14px 0 8px; }
.u-summary, .u-facts { font: 400 var(--fs-meta)/1.5 var(--sans); color: var(--muted); margin: 0 0 10px; }
.u-kicker { font: 600 var(--fs-small)/1.4 var(--sans); color: var(--muted); margin: 14px 0 6px; }
.u-h2 { font: 600 var(--fs-base)/1.3 var(--serif); color: var(--ink); margin: 22px 0 8px; }
.u-h3 { font: 600 var(--fs-small)/1.35 var(--sans); color: var(--ink-soft); margin: 14px 0 6px; }
.u-note { font: 400 var(--fs-small)/1.5 var(--sans); color: var(--muted); margin: 6px 0; }
.u-muted { color: var(--muted); }
.u-desc { font: 400 var(--fs-meta)/1.55 var(--serif); color: var(--ink-soft); margin: 8px 0; }
.u-desc p { margin: 0 0 8px; }
.u-doors { display: flex; flex-wrap: wrap; gap: 6px 14px; margin: 10px 0; font: 500 var(--fs-meta)/1.4 var(--sans); }
.u-link { color: var(--steel-text); }
.u-evidence { font: 400 var(--fs-meta)/1.5 var(--sans); color: var(--ink-soft); }
.u-evidence p { margin: 6px 0; }
.u-checks, .u-finds, .u-reruns { list-style: none; padding: 0; margin: 6px 0; font: 400 var(--fs-small)/1.5 var(--sans); color: var(--ink-soft); }
.u-checks li, .u-finds li, .u-reruns li { padding: 6px 0; border-top: 1px solid var(--rule); }
.u-reruns li.is-not strong { color: var(--brick-text); }
.u-pill { display: inline-block; font: 600 0.6875rem/1.5 var(--sans); padding: 0 6px; border-radius: 9px; background: var(--sunk); color: var(--ink-soft); }
.u-lean-label { font: 400 var(--fs-meta)/1.5 var(--serif); color: var(--ink-soft); margin: 4px 0; }
.u-lean { font-size: 0.75rem; max-height: 22em; overflow: auto; }

.u-rows, .u-subrows, .u-papers { list-style: none; margin: 0; padding: 0; }
.u-papers > li { margin: 0 0 6px; }
.u-go {
  font: inherit; color: inherit; background: none; border: 0; padding: 0; margin: 0; text-align: left; cursor: pointer; width: 100%;
}
.u-row {
  display: grid; grid-template-columns: auto minmax(0, 1fr); column-gap: 8px; row-gap: 1px; align-items: baseline;
  padding: 7px 8px; border-radius: var(--r-sm); font: 400 var(--fs-meta)/1.4 var(--sans); color: var(--ink);
}
.u-row:hover, .u-row:focus-visible, .u-sub:hover, .u-sub:focus-visible { background: var(--sunk); }
.u-row:focus-visible, .u-sub:focus-visible, .u-crumb:focus-visible, .u-inline:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 1px; }
.u-row__num { font: 600 var(--fs-micro)/1.4 var(--sans); color: var(--muted); font-variant-numeric: tabular-nums; }
.u-row__k { font: 600 var(--fs-small)/1.4 var(--sans); color: var(--muted); }
.u-row__t { grid-column: 2; font-family: var(--serif); font-size: var(--fs-body); }
.u-row > .u-row__t:first-child { grid-column: 1 / -1; }
.u-row__n { grid-column: 2; font-size: var(--fs-small); color: var(--muted); }
.u-row > .u-row__t:first-child + .u-row__n { grid-column: 1 / -1; }
.u-row--link { grid-template-columns: auto auto minmax(0, 1fr); }
.u-row--link .u-row__t, .u-row--link .u-row__n { grid-column: 3; }
.u-sub { display: flex; gap: 8px; align-items: baseline; padding: 5px 8px; border-radius: var(--r-sm); font: 400 var(--fs-small)/1.4 var(--sans); color: var(--ink-soft); }
.u-sub code { font-size: 0.8125rem; overflow-wrap: anywhere; }
.u-subrows { margin-left: 8px; }
.u-context { font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); margin: 12px 0 4px; }
.u-inline--plain { font: 500 var(--fs-small)/1.45 var(--serif); }
.u-inline { display: inline; width: auto; color: var(--steel-text); text-decoration: underline; text-underline-offset: 3px; font-weight: 600; }

.u-stmt { margin: 10px 0 6px; padding: 12px 14px; background: var(--surface); border: 1px solid var(--rule); border-radius: var(--r-md); font: 400 var(--fs-body)/1.6 var(--serif); color: var(--ink); overflow-x: auto; }
.u-stmt__body p { margin: 0 0 8px; }
.u-stmt .m-d { overflow-x: auto; overflow-y: hidden; }
.u-stmt .katex { font-size: 1.06em; }
.u-stmt figcaption { margin-top: 6px; }

/* ---- Key ----------------------------------------------------------------- */
.u-legend { border-top: 1px solid var(--rule); margin-top: 22px; }
.u-key { list-style: none; margin: 4px 0 8px; padding: 0; }
.u-key li { display: grid; grid-template-columns: 22px minmax(0, 1fr) auto; gap: 8px; align-items: baseline; padding: 3px 0; font: 400 var(--fs-small)/1.4 var(--sans); color: var(--ink-soft); }
.u-key__n { color: var(--muted); font-variant-numeric: tabular-nums; }
.u-key__g { display: flex; align-items: center; justify-content: center; align-self: center; }
.u-sw { width: 14px; height: 14px; flex: none; overflow: visible; align-self: center; }
.u-sw path, .u-sw circle { fill: none; stroke-width: 1.4; }
.u-sw-lean0 path { stroke: var(--u-steel); fill: var(--u-ground); }
.u-sw-lean1 path { stroke: var(--u-steel); fill: color-mix(in oklab, var(--u-steel) 38%, var(--u-ground)); }
.u-sw-lean2 path { stroke: var(--u-steel); fill: color-mix(in oklab, var(--u-steel) 70%, var(--u-ground)); }
.u-sw-lean3 path { stroke: var(--u-steel); fill: var(--u-steel); }
.u-sw .u-sw-hole { fill: var(--u-ground); stroke: none; }
.u-sw-paired circle { fill: var(--u-paired); stroke: none; }
.u-sw-unpaired circle { fill: var(--u-ground); stroke: var(--u-struct); }
.u-sw-hol circle { stroke: var(--u-brick); }
.u-sw-fin circle { stroke: var(--u-brick); stroke-dasharray: 1.2 2.4; stroke-linecap: round; }
.u-sw-cites path { stroke: var(--u-cites); stroke-width: 1.8; }
.u-sw-cited path { stroke: var(--u-cited); stroke-width: 1.8; }

/* ---- Index (the no-JavaScript map) ----------------------------------------- */
/* ---- A two-line key on the first screen ------------------------------------ */
.u-keyline { list-style: none; margin: 4px 0 6px; padding: 0; font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); }
.u-keyline li { display: grid; grid-template-columns: 18px minmax(0, 1fr); gap: 8px; align-items: baseline; padding: 2px 0; }
.u-keyline .u-sw { align-self: center; }
.u-keyline__more { display: block !important; padding-left: 26px !important; }
.u-keyline__more a { color: var(--steel-text); }

/* ---- Ways in: four families a person may already know of ------------------- */
.u-h2--ways { margin-top: 18px; }
.u-ways { list-style: none; margin: 0 0 4px; padding: 0; }
.u-ways li + li { border-top: 1px solid var(--rule); }
.u-way {
  display: block; padding: 10px 8px 11px; margin: 0 -8px; border-radius: var(--r-sm);
  color: var(--ink); text-decoration: none;
}
.u-way__t { display: block; font: 500 var(--fs-base)/1.35 var(--serif); color: var(--ink); text-wrap: balance; }
.u-way__w { display: block; margin-top: 3px; font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); text-wrap: pretty; }
@media (hover: hover) and (pointer: fine) {
  .u-way:hover { background: var(--sunk); }
  .u-way:hover .u-way__t { text-decoration: underline; text-decoration-color: color-mix(in oklab, currentColor 35%, transparent); text-underline-offset: 3px; }
}
.u-way:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 1px; }

/* ---- Bands under the map: the order a stranger needs them --------------------- */
.u-band { border-top: 1px solid var(--rule); padding: 56px 0 60px; background: var(--page); }
.u-band__in { display: block; }
.u-band__h { font: 500 1.5rem/1.25 var(--serif); letter-spacing: -0.01em; color: var(--ink); margin: 0 0 10px; text-wrap: balance; }
.u-band__intro { font: 400 var(--fs-body)/1.6 var(--sans); color: var(--ink-soft); max-width: 62ch; margin: 0 0 18px; text-wrap: pretty; }
.u-band__links { display: flex; flex-wrap: wrap; gap: 6px 22px; align-items: baseline; margin: 16px 0 0; font: 500 var(--fs-meta)/1.5 var(--sans); }
.u-band__links span { color: var(--muted); font-weight: 400; }
.u-band__links a { color: var(--steel-text); display: inline-block; padding: 3px 0; }
.u-band--example .u-band__in { display: grid; grid-template-columns: minmax(0, 5fr) minmax(0, 7fr); gap: 28px 56px; align-items: start; }
.u-band--example .u-band__head { position: sticky; top: calc(var(--top-h, 64px) + 24px); }
.u-band--bench .u-band__in { grid-template-columns: minmax(0, 1fr); gap: 8px; }
.u-band--bench .u-band__head { position: static; }
/* The embedded family bench keeps any too-wide line (a Lean file name, a formula) inside its own box at large text. */
.u-example { min-width: 0; overflow-x: auto; overflow-y: hidden; }
.u-band--bench .u-example { max-width: 72rem; }
.u-example__card { padding: 0; }
.u-example__num { font: 600 var(--fs-small)/1.4 var(--sans); color: var(--muted); margin: 0 0 4px; }
.u-example__title { font: 500 1.25rem/1.3 var(--serif); color: var(--ink); margin: 0 0 10px; text-wrap: balance; }
.u-example__desc { font: 400 var(--fs-body)/1.6 var(--serif); color: var(--ink-soft); max-width: 66ch; }
.u-example__desc p { margin: 0 0 10px; }
.u-example .stmt { margin-top: 8px; max-width: 46rem; }
.u-band__in--split { display: grid; grid-template-columns: minmax(0, 4fr) minmax(0, 8fr); gap: 16px 56px; align-items: baseline; }
.u-sentences p { font: 400 var(--fs-lede)/1.65 var(--serif); color: var(--ink); max-width: 64ch; margin: 0 0 12px; text-wrap: pretty; }
.u-sentences p.u-band__links { font: 500 var(--fs-meta)/1.5 var(--sans); margin-top: 18px; }
.u-num { color: var(--steel-text); font-variant-numeric: tabular-nums; text-decoration: underline; text-decoration-color: color-mix(in oklab, currentColor 40%, transparent); text-underline-offset: 3px; }
.u-num:hover { text-decoration-color: currentColor; }
.u-who { list-style: none; margin: 0; padding: 0; display: grid; grid-template-columns: repeat(auto-fill, minmax(min(100%, 30rem), 1fr)); gap: 0 48px; }
.u-who li { padding: 14px 0 15px; border-top: 1px solid var(--rule); font: 400 var(--fs-body)/1.6 var(--sans); color: var(--ink-soft); max-width: 66ch; }
.u-who__n { font-weight: 600; color: var(--steel-text); }
.u-help2 { display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 12px 48px; max-width: 70rem; }
.u-help2 > div { border-top: 1px solid var(--rule); padding-top: 12px; }
.u-help2 p { font: 400 var(--fs-body)/1.6 var(--sans); color: var(--ink-soft); margin: 0 0 8px; max-width: 60ch; }
.u-help2 a { font-weight: 500; color: var(--steel-text); }
.u-band--index .u-index { max-width: 72rem; columns: 2 26rem; column-gap: 48px; }
.u-band--index .u-index__d { break-inside: avoid; }
#catalogue:focus { outline: none; }
.u-listsec { border-top: 1px solid var(--rule); margin-top: 18px; }
.u-index { font: 400 var(--fs-small)/1.45 var(--sans); }
.u-index__d { border-bottom: 1px solid var(--rule); }
.u-index__d > summary { cursor: pointer; padding: 8px 0; font-weight: 600; color: var(--ink); }
.u-index__dc { font-weight: 400; color: var(--muted); }
.u-index ul { list-style: none; margin: 0; padding: 0 0 0 12px; }
.u-index__fams { padding-left: 0 !important; }
.u-index__f { margin: 0 0 8px; }
.u-index__f > a { font-family: var(--serif); font-size: var(--fs-body); }
.u-index__num { font: 600 var(--fs-micro)/1 var(--sans); color: var(--muted); }
.u-index a { color: var(--steel-text); }
.u-index__lean code { font-size: 0.75rem; }

/* ---- Stage ------------------------------------------------------------- */
.u-stage { position: relative; min-width: 0; min-height: 0; overflow: hidden; background: var(--page); }
.u-canvas { position: absolute; inset: 0; width: 100%; height: 100%; display: block; touch-action: none; cursor: grab; }
.u-canvas.is-over { cursor: pointer; }
.u-canvas.is-panning { cursor: grabbing; }
.u-canvas:focus-visible { outline: 2px solid var(--steel-text); outline-offset: -2px; }
.u-tools { position: absolute; top: 12px; right: 12px; display: flex; flex-direction: column; gap: 6px; }
.u-tool {
  width: 32px; height: 32px; display: grid; place-items: center; border-radius: var(--r-sm);
  background: var(--surface); border: 1px solid var(--rule-strong); color: var(--ink); cursor: pointer;
}
.u-tool:hover { border-color: var(--rule-control); }
.u-tool:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 1px; }
.u-tool svg { width: 16px; height: 16px; fill: none; stroke: currentColor; stroke-width: 1.6; stroke-linecap: round; }
.u-help { position: absolute; left: 14px; bottom: 10px; margin: 0; max-width: min(560px, calc(100% - 80px)); font: 400 var(--fs-micro)/1.4 var(--sans); color: var(--muted); pointer-events: none; }
.u-status { position: absolute; inset: 0 0 0 calc(var(--u-panel-w) + var(--u-gutter) - 20px); pointer-events: none; display: grid; place-items: center; margin: 0; font: 400 var(--fs-meta)/1.4 var(--sans); color: var(--muted); }
.u-status[hidden] { display: none; }
.u-switch { display: none; }

/* ---- Narrow: Map | List, the list first ----------------------------------- */
@media (max-width: 899px) {
  .u-band { padding: 40px 0 44px; }
  .u-band--example .u-band__in, .u-band__in--split, .u-help2 { grid-template-columns: minmax(0, 1fr); }
  .u-band--example .u-band__head { position: static; }
  .u-explorer { display: block; height: auto; min-height: 0; }
  .u-switch { display: flex; gap: 4px; padding: 10px 16px; border-bottom: 1px solid var(--rule); position: sticky; top: 0; background: var(--page); z-index: 2; }
  .u-switch__b { flex: 1; font: 600 var(--fs-meta)/1 var(--sans); padding: 9px 0; border-radius: var(--r-sm); border: 1px solid var(--rule-strong); background: var(--surface); color: var(--ink); cursor: pointer; }
  .u-switch__b[aria-pressed="true"] { background: var(--ink); color: var(--on-ink); border-color: var(--ink); }
  .u-panel { border-right: 0; }
  .u-panel__head { padding: 12px 16px; }
  .u-panel__body { overflow: visible; padding: 4px 16px 28px; }
  .u-stage { height: 72vh; height: 72svh; }
  /* The same status stays visible while List hides the map, including when
     the chosen family is far down the list. One live region serves both views. */
  .u-status { position: fixed; inset: auto 16px 16px; z-index: 4; padding: 12px 16px; background: var(--surface); border: 1px solid var(--rule-strong); border-radius: var(--r-sm); text-align: center; }
  [data-universe][data-view="list"] .u-stage { display: none; }
  [data-universe][data-view="map"] .u-panel { display: block; }
  [data-universe][data-view="map"] .u-panel__body,
  [data-universe][data-view="map"] .u-panel__head > :not(.u-trail):not(.u-step) { display: none; }
  [data-universe][data-view="map"] .u-panel__head { padding: 0; border-bottom: 0; }
  [data-universe][data-view="map"] .u-trail:not([hidden]) { margin: 0; padding: 10px 16px; border-bottom: 1px solid var(--rule); }
  [data-universe][data-view="map"] .u-step:not([hidden]) { margin: 0; padding: 6px 16px; border-bottom: 1px solid var(--rule); }
  .u-help { display: none; }
  /* The list starts with something to open: the disciplines and the ways in come
     straight after the release's two sentences, and the colour key, which explains
     the map more than the list, follows them behind a link at the top. */
  .u-view { display: flex; flex-direction: column; }
  .u-view .u-keyjump { display: block; order: 1; margin: 0 0 4px; font: 400 var(--fs-meta)/1.4 var(--sans); }
  .u-discsec { order: 2; }
  .u-wayssec { order: 3; }
  .u-keysec { order: 4; scroll-margin-top: 64px; }
}
.u-keyjump { display: none; }
@media (prefers-reduced-motion: reduce) {
  .u-row, .u-sub { transition: none; }
}

/* ---- The list: one colour per meaning, said in words -------------------------- */
.u-dot { display: inline-block; flex: none; width: 10px; height: 10px; border-radius: 50%; margin-right: 8px; vertical-align: -0.05em; background: var(--u-t-none); }
.u-dot--all { background: var(--u-t-all); }
.u-dot--part { background: var(--u-t-part); }
.u-dot--other { background: var(--u-t-other); }
.u-dot--split { background: var(--u-t-split); }
.u-dot--none, .u-dot--unread { background: transparent; box-shadow: inset 0 0 0 1.5px var(--u-t-none); }
.u-key li { grid-template-columns: 18px minmax(0, 1fr) auto; }
.u-key .u-dot { margin: 0; align-self: center; }
.u-entries { list-style: none; margin: 4px 0 0; padding: 0; }
.u-entries li + li { border-top: 1px solid var(--rule); }
.u-entry { display: block; padding: 9px 8px 10px; margin: 0 -8px; border-radius: var(--r-sm); color: var(--ink); text-decoration: none; }
.u-entry__t { display: flex; align-items: baseline; font: 500 var(--fs-base)/1.35 var(--serif); color: var(--ink); text-wrap: balance; }
.u-entry__t .u-dot { position: relative; top: -0.05em; }
.u-entry__s { display: block; margin: 3px 0 0 18px; font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); }
.u-entry__more { display: none; }
.u-entry.is-active .u-entry__more, .u-entry:focus-visible .u-entry__more { display: block; }
.u-entry.is-active { background: var(--sunk); }
.u-role { font: 600 var(--fs-micro)/1.4 var(--sans); color: var(--muted); }
.u-qual { margin: -2px 0 8px; font: italic 400 var(--fs-small)/1.45 var(--sans); color: var(--ink-soft); }
.u-entry__c { display: block; margin: 5px 0 0 18px; font: 400 var(--fs-meta)/1.5 var(--serif); color: var(--ink-soft); text-wrap: pretty; }
.u-entry__e { display: block; margin: 5px 0 0 18px; font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); text-wrap: pretty; }
@media (hover: hover) and (pointer: fine) {
  .u-entry:hover { background: var(--sunk); }
  .u-entry:hover .u-entry__t > span:last-child { text-decoration: underline; text-decoration-color: color-mix(in oklab, currentColor 35%, transparent); text-underline-offset: 3px; }
}
.u-entry:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 1px; }
.u-cat { margin: 6px 0 10px; }
.u-cat figcaption { font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); margin: 0 0 4px; }
.u-cat blockquote { margin: 0; padding: 0 0 0 12px; border-left: 2px solid var(--rule-strong); font: 400 var(--fs-body)/1.55 var(--serif); color: var(--ink); text-wrap: pretty; }
.u-btn { display: inline-flex; align-items: center; min-height: 32px; padding: 5px 12px; border-radius: var(--r-sm); border: 1px solid var(--rule-control); background: var(--surface); color: var(--ink); font: 500 var(--fs-meta)/1.25 var(--sans); text-decoration: none; }
.u-btn--primary { background: var(--ink); border-color: var(--ink); color: var(--on-ink); }
/* The site-wide a:hover colour must not reach a primary button: its label stays legible. */
.u-btn--primary:hover, .u-btn--primary:focus-visible { color: var(--on-ink); }
.u-btn:hover { border-color: var(--ink); }
.u-btn:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }
.u-doors { gap: 8px; margin: 12px 0 6px; }
.u-tone { display: flex; align-items: baseline; font: 400 var(--fs-meta)/1.5 var(--sans); color: var(--ink-soft); margin: 6px 0; }
.u-tone .u-dot { position: relative; top: 0.05em; }
.u-readers { list-style: none; margin: 4px 0 6px 18px; padding: 0; font: 400 var(--fs-small)/1.5 var(--sans); color: var(--ink-soft); }
.u-readers li { padding: 6px 0; border-top: 1px solid var(--rule); }
.u-readers p { margin: 0; }
.u-readers a { color: var(--steel-text); font-weight: 600; }
.u-term { color: var(--muted); }
.u-readers__note { margin-top: 3px !important; color: var(--muted); font-style: italic; }
.u-sub { flex-wrap: wrap; column-gap: 10px; }
.u-sub__t { font: 500 var(--fs-meta)/1.35 var(--sans); color: var(--ink); }
.u-sub__n { font-size: var(--fs-small); color: var(--muted); overflow-wrap: anywhere; }
.u-sub__w { margin: 0 0 6px 8px; font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); }
.u-join { display: inline-block; width: 18px; height: 0; margin-right: 6px; vertical-align: 0.3em; border-top: 1.5px solid var(--u-steel); }
.u-join--candidate { border-top-style: dashed; }
.u-more { margin: 14px 0 4px; padding: 10px 0 0; border-top: 1px solid var(--rule); font: 400 var(--fs-small)/1.5 var(--sans); color: var(--ink-soft); }
.u-more p { margin: 0 0 4px; }
.u-paper-title { font: 500 var(--fs-base)/1.4 var(--serif); color: var(--ink); margin: 4px 0; }
.u-stmt__head { margin: 0 0 6px; }
.u-h3.is-cites::before, .u-h3.is-cited::before { content: ""; display: inline-block; width: 16px; height: 0; margin-right: 7px; vertical-align: 0.3em; border-top: 2px solid var(--u-cites); }
.u-h3.is-cited::before { border-top-color: var(--u-cited); }
.u-rows .u-row__t .u-dot { margin-right: 7px; }
.u-index__d { break-inside: avoid; margin: 0 0 18px; }
.u-index__dn { font: 600 var(--fs-base)/1.35 var(--serif); color: var(--ink); margin: 0 0 6px; }
.u-index__fams li { margin: 0 0 4px; }
.u-index__fams a { display: inline-flex; align-items: baseline; min-height: 24px; padding: 2px 0; font: 400 var(--fs-meta)/1.4 var(--serif); color: var(--steel-text); }
.u-nowrap { white-space: nowrap; }
.u-panel .u-lean { font-size: 0.75rem; line-height: 1.5; max-height: none; overflow-x: auto; }

/* Reading a theorem or a Lean statement: the panel takes about two fifths of the
   workspace so the mathematics keeps its size, and the map refits beside it. */
@media (min-width: 900px) {
  .u-explorer.is-reading { grid-template-columns: calc(clamp(440px, 40vw, 760px) + var(--u-gutter) - 20px) minmax(0, 1fr); }
}

/* The family map's own key, bottom left of the drawing, in words. */
.u-maplegend { position: absolute; left: 14px; bottom: 12px; max-width: 290px; padding: 9px 12px 10px; background: var(--page); border: 1px solid var(--rule); border-radius: var(--r-md); font: 400 var(--fs-micro)/1.4 var(--sans); color: var(--ink-soft); }
.u-maplegend[hidden] { display: none; }
.u-maplegend__h { margin: 0 0 5px; font-weight: 600; color: var(--ink); }
.u-maplegend ul { list-style: none; margin: 0; padding: 0; display: grid; gap: 3px; }
.u-maplegend li { display: grid; grid-template-columns: 20px minmax(0, 1fr); gap: 6px; align-items: center; }
.u-maplegend svg { overflow: visible; }
.u-lg-dot { stroke: none; fill: var(--u-t-none); }
.u-lg-dot--all { fill: var(--u-t-all); } .u-lg-dot--part { fill: var(--u-t-part); } .u-lg-dot--other { fill: var(--u-t-other); } .u-lg-dot--split { fill: var(--u-t-split); }
.u-lg-dot--none, .u-lg-dot--unread { fill: var(--u-struct); }
.u-lg-dia { fill: var(--u-ground); stroke: var(--u-steel); stroke-width: 1.6; }
.u-lg-ring { fill: none; stroke: var(--u-paper); stroke-width: 1.2; }
.u-lg-line { fill: none; stroke: var(--u-steel); stroke-width: 1.4; }
.u-lg-line--cand { stroke-dasharray: 3 3; }
.u-lg-cite { fill: none; stroke-width: 1.6; }
.u-lg-cite--out { stroke: var(--u-cites); } .u-lg-cite--in { stroke: var(--u-cited); }
@media (max-width: 899px) { .u-maplegend { max-width: calc(100% - 28px); } }

/* The map key for the release and a discipline, top left of the drawing. */
/* The bar over the drawing: the key's button and one line saying what the drawing shows. */
.u-mapbar { position: absolute; left: 14px; right: 14px; top: 10px; display: flex; align-items: center; gap: 8px 14px; pointer-events: none; }
.u-mapbar > * { pointer-events: auto; }
.u-cap { margin: 0; max-width: 78ch; font: 400 var(--fs-small)/1.4 var(--sans); color: var(--ink-soft); text-wrap: pretty; }
.u-edge-guide { display: block; margin-top: 5px; }
.u-edge-key { display: inline-flex; align-items: baseline; gap: 4px; margin-right: 10px; font-weight: 600; white-space: nowrap; }
.u-edge-key--out { color: var(--u-cites); }
.u-edge-key--in { color: var(--u-cited); }
[data-board] .u-mapbar { display: none; }
.u-mapkey-btn { flex: none; position: static; min-height: 32px; padding: 5px 12px; border-radius: var(--r-sm); border: 1px solid var(--rule-strong); background: var(--surface); color: var(--ink); font: 500 var(--fs-small)/1.2 var(--sans); cursor: pointer; }
.u-mapkey-btn[hidden] { display: none; }
.u-mapkey-btn[aria-expanded="true"] { border-color: var(--ink); }
.u-mapkey-btn:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }
.u-mapkey { position: absolute; left: 14px; top: 52px; width: min(330px, calc(100% - 28px)); padding: 10px 12px 11px; background: var(--page); border: 1px solid var(--rule); border-radius: var(--r-md); font: 400 var(--fs-micro)/1.45 var(--sans); color: var(--ink-soft); }
.u-mapkey[hidden] { display: none; }
.u-mapkey ul { list-style: none; margin: 4px 0 8px; padding: 0; display: grid; gap: 3px; }
.u-mapkey li { display: flex; align-items: center; }
.u-mapkey .u-dot { width: 9px; height: 9px; }
.u-mapkey__p { margin: 0 0 6px; }
.u-arrow { display: inline-block; width: 22px; height: 0; margin-right: 6px; vertical-align: 0.3em; border-top: 1.6px solid var(--u-cites); position: relative; }
.u-arrow::after { content: ""; position: absolute; right: -1px; top: -4.6px; border: 4px solid transparent; border-left: 6px solid var(--u-cites); border-right: 0; }
/* Re-run entries and the pair the map traces. */
.u-runs { list-style: none; margin: 2px 0 6px 8px; padding: 0; font: 400 var(--fs-small)/1.45 var(--sans); color: var(--ink-soft); }
.u-runs li { padding: 3px 0; }
.u-why { margin: 0 0 6px 8px; font: 400 var(--fs-small)/1.45 var(--sans); color: var(--muted); }
.u-why summary { cursor: pointer; color: var(--ink-soft); min-height: 24px; }
.u-why p { margin: 4px 0 0; }
.u-subrows--lean > li.is-shown { box-shadow: inset 2px 0 0 var(--u-steel); padding-left: 6px; }
.u-shown { margin: 0 0 4px 8px; font: 600 var(--fs-micro)/1.4 var(--sans); color: var(--steel-text); }
.u-pairbtn { margin: 0 0 4px 8px; min-height: 26px; padding: 3px 10px; border-radius: var(--r-sm); border: 1px solid var(--rule-control); background: var(--surface); color: var(--ink); font: 500 var(--fs-micro)/1.2 var(--sans); cursor: pointer; }
.u-pairbtn:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }

/* Search matches folded away after one is opened; one button brings them back. */
.u-results.is-folded > :not(.u-unfold) { display: none; }
.u-unfold { display: none; }
.u-results.is-folded .u-unfold { display: inline-flex; align-items: center; min-height: 28px; margin: 2px 0 8px; padding: 0; border: 0; background: none;
  font: 400 var(--fs-meta)/1.4 var(--sans); color: var(--steel-text); text-decoration: underline; text-underline-offset: 0.18em; cursor: pointer; }
.u-unfold:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }

/* With JavaScript off the map cannot draw: its stage and the List/Map switch stand
   down, and one line points to the list of every family below. */
.u-nojs { display: none; }
html:not(.js) .u-nojs { display: block; font: 400 var(--fs-meta)/1.5 var(--sans); color: var(--ink-soft); }
html:not(.js) .u-stage, html:not(.js) .u-switch, html:not(.js) .u-status { display: none; }

/* ---- The family board -------------------------------------------------------- */
/* Inside a family the map is a board of cards, read left to right: the families whose
   papers cite it, its papers in columns (each result's statement, typeset, with the Lean
   statements paired with it joined beneath), and the families its papers cite. Every
   name is written on its card; nothing waits for the pointer. Cards grow with the
   screen, so a 27-inch monitor reads as easily as a laptop. */
.u-board {
  position: absolute; inset: 0; z-index: 2; overflow: auto; overscroll-behavior: contain;
  scrollbar-gutter: stable;
  background: var(--page); color: var(--ink-soft);
  font: 400 clamp(15px, calc(0.42vw + 9.5px), 20px)/1.45 var(--sans);
  opacity: 0; visibility: hidden; pointer-events: none; transform: translateY(8px);
  transition: opacity var(--t-open) var(--ease-out), transform var(--t-open) var(--ease-out), visibility 0s;
}
.u-board.is-on { opacity: 1; visibility: visible; pointer-events: auto; transform: none; transition: opacity var(--t-open) var(--ease-out), transform var(--t-open) var(--ease-out), visibility 0s; }
.u-board:focus { outline: none; }
.u-board:focus-visible { outline: 2px solid var(--steel-text); outline-offset: -2px; }
.u-title:focus { outline: none; }
[data-board] .u-tools, [data-board] .u-mapkey-btn, [data-board] .u-mapkey, [data-board] .u-maplegend { display: none; }
.u-board__in { position: relative; box-sizing: border-box; min-height: 100%; padding: 1em 1.25em 1.25em; }
.u-board__wires { position: absolute; left: 0; top: 0; overflow: visible; pointer-events: none; }
.u-board__wires path { fill: none; stroke-width: 1.5; stroke-linecap: round; }
.u-board__wires .w-lean { stroke: var(--u-steel); }
.u-board__wires .w-cand { stroke-dasharray: 5 4; }
.u-board__wires .w-out { stroke: var(--u-cites); opacity: 0.85; marker-start: url(#u-cite-out); }
.u-board__wires .w-in { stroke: var(--u-cited); opacity: 0.85; marker-end: url(#u-cite-in); }
.u-board__wires .w-arrow-out { fill: var(--u-cites); stroke: none; }
.u-board__wires .w-arrow-in { fill: var(--u-cited); stroke: none; }
.u-board__wires .is-hot { opacity: 1; stroke-width: 2.2; }
.u-board__head { margin: 0 0 0.9em; max-width: 72em; }
.u-board__k { margin: 0; font: 600 0.8125em/1.4 var(--sans); color: var(--muted); }
.u-board__t { display: none; margin: 0.15em 0 0.3em; font: 500 1.3em/1.25 var(--serif); color: var(--ink); text-wrap: balance; }
.u-board__r { margin: 0.25em 0 0; max-width: 60em; font-size: 0.875em; color: var(--ink-soft); text-wrap: pretty; }
.u-board__r b { font-weight: 600; color: var(--ink); }
.u-board__cols { display: grid; grid-template-columns: minmax(8.5em, 11em) minmax(0, 1fr) minmax(8.5em, 11em); gap: 0 2.25em; align-items: start; }
.u-board__side h3, .u-board__colh { margin: 0 0 0.55em; font: 600 0.875em/1.3 var(--sans); color: var(--ink); }
.u-board__side .u-bc + .u-bc { margin-top: 0.6em; }
.u-board__none { margin: 0; font-size: 0.8125em; color: var(--muted); }
.u-board__papers { column-gap: 1.25em; padding-top: 1.5em; }
.u-board__papers > .u-col { break-inside: avoid; margin-bottom: 1.25em; }
.u-board__papers > [hidden] { display: none; }
.u-col { min-width: 0; }
.u-col > ol { list-style: none; margin: 0; padding: 0; }
.u-col > ol > li { margin: 0.7em 0 0; }
.u-leans > .u-bc { margin: 0.55em 0 0 1.4em; }
.u-board__foot { margin: 1.1em 0 0; font-size: 0.8125em; color: var(--muted); }
.u-board__foot::before { content: ""; display: inline-block; width: 1.6em; margin-right: 0.5em; vertical-align: 0.3em; border-top: 1.5px dashed var(--u-steel); }
/* A card: one object, named on it, its words kept inside it. */
.u-bc {
  position: relative; display: block; box-sizing: border-box; min-width: 0; padding: 0.55em 0.75em 0.65em;
  background: var(--surface); border: 1px solid var(--rule-strong); border-radius: var(--r-md);
  color: var(--ink-soft); cursor: pointer; overflow: hidden; overflow-wrap: break-word;
  transition: border-color var(--t-hover) var(--ease-out), box-shadow var(--t-hover) var(--ease-out);
}
.u-bc p { margin: 0; }
@media (hover: hover) and (pointer: fine) { .u-bc:hover { border-color: var(--ink-soft); } }
.u-bc:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }
.u-bc.is-sel { border-color: var(--ink); box-shadow: 0 0 0 1px var(--ink); }
.u-bc.is-pair { border-color: var(--u-steel); box-shadow: 0 0 0 1px var(--u-steel); }
.u-bc.is-ring { animation: u-bc-ring 700ms var(--ease-out) 1; }
@keyframes u-bc-ring { from { box-shadow: 0 0 0 1px var(--ink), 0 0 0 0 color-mix(in oklab, var(--ink) 40%, transparent); } to { box-shadow: 0 0 0 1px var(--ink), 0 0 0 12px color-mix(in oklab, var(--ink) 0%, transparent); } }
.u-bc.is-dim { opacity: 0.45; }
.u-bc--p { background: var(--sunk); border-color: var(--sunk); }
.u-bc__pt { font: 500 1.0625em/1.3 var(--serif); color: var(--ink); text-wrap: balance; }
.u-bc__d { margin-top: 0.15em !important; font-size: 0.8125em; color: var(--muted); }
.u-bc__acts { display: flex; flex-wrap: wrap; gap: 0.2em 1em; margin-top: 0.35em !important; font: 500 0.8125em/1.4 var(--sans); }
.u-bc__acts a { color: var(--steel-text); }
.u-bc__lab { font: 600 0.8125em/1.35 var(--sans); color: var(--ink); }
.u-bc__lab .u-bc__ttl { font-weight: 400; color: var(--ink-soft); }
/* Give typeset glyphs room beyond the text line box; a few pixels of ink must
   not create an inner vertical scrollbar and narrow the whole statement. */
.u-bc__x { margin-top: 0.3em; padding-block: 0.25em; font: 400 1em/1.5 var(--serif); color: var(--ink); overflow-x: auto; overflow-wrap: break-word; }
.u-bc__x p { margin: 0 0 0.4em; }
.u-bc__x p:last-child { margin-bottom: 0; }
.u-bc__x .katex { font-size: 1.02em; }
.u-bc__x--none { font: 400 0.8125em/1.45 var(--sans); color: var(--muted); max-height: none; }
.u-bc--l { border-color: color-mix(in oklab, var(--u-steel) 40%, var(--rule-strong)); }
.u-bc__lt { font: italic 400 1em/1.35 var(--serif); color: var(--steel-text); }
.u-bc__id { margin-top: 0.1em !important; }
.u-bc__id code { font: 400 0.8125em/1.35 var(--mono); color: var(--ink-soft); overflow-wrap: anywhere; }
.u-bc__ln { margin-top: 0.3em !important; font-size: 0.8125em; line-height: 1.45; color: var(--ink-soft); text-wrap: pretty; }
.u-bc__ln--q { color: var(--ink); }
.u-bc--f .u-bc__k { font: 600 0.75em/1.4 var(--sans); color: var(--muted); }
.u-bc__ft { font: 500 0.9375em/1.3 var(--serif); color: var(--ink); }
.u-bc--f .u-bc__ln { margin-top: 0.2em !important; color: var(--muted); }
.u-bc--f .u-dot { width: 0.6em; height: 0.6em; margin-right: 0.4em; }
/* On a wide screen the panel beside the board names the family; on a phone the board
   is one column under the switch and names it first. */
@media (max-width: 899px) {
  [data-universe][data-board] .u-stage { height: auto; min-height: 0; overflow: visible; }
  [data-universe][data-board] .u-canvas { display: none; }
  .u-board { position: static; overflow: visible; font-size: 15px; transform: none; }
  .u-board:not(.is-on) { display: none; }
  .u-board__in { padding: 0.9em 16px 1.5em; }
  .u-board__t { display: block; }
  .u-board__cols { display: flex; flex-direction: column; gap: 1.5em; }
  .u-board__main { order: 1; }
  .u-board__side--in { order: 2; }
  .u-board__side--out { order: 3; }
  .u-board__papers { display: block; padding-top: 0; }
  .u-col + .u-col { margin-top: 1.4em; }
  .u-board__papers > .u-col { margin-bottom: 0; }
}
@media (prefers-reduced-motion: reduce) {
  .u-board, .u-board.is-on { transition: none; transform: none; }
  .u-bc.is-ring { animation: none; }
}

/* ---- Motion (DESIGN.md "Motion and hover") ---------------------------------- */
/* The card beside what the pointer names on the map: its name, where it belongs,
   its counts and its state in words. It never takes the pointer, fades in over
   --t-hover and leaves a little faster. */
.u-card {
  position: absolute; left: 0; top: 0; z-index: 4; box-sizing: border-box;
  width: max-content; max-width: min(300px, calc(100% - 16px)); padding: 9px 12px 10px;
  background: var(--surface); border: 1px solid var(--rule-strong); border-radius: var(--r-md, 8px);
  box-shadow: 0 1px 2px rgba(25, 21, 32, 0.08), 0 6px 18px -8px rgba(25, 21, 32, 0.2);
  font: 400 var(--fs-small)/1.45 var(--sans); color: var(--ink-soft);
  pointer-events: none; visibility: hidden; opacity: 0;
  transition: opacity 80ms var(--ease-out), visibility 0s linear 80ms;
}
.u-card.is-on { visibility: visible; opacity: 1; transition: opacity var(--t-hover) var(--ease-out), visibility 0s; }
.u-card p { margin: 0; }
.u-card__t { font: 500 0.9375rem/1.3 var(--serif); color: var(--ink); text-wrap: balance; margin-bottom: 3px !important; }
.u-card__t--lean { font-style: italic; }
.u-card__t code { display: block; margin-top: 2px; font: 400 0.75rem/1.35 var(--mono); font-style: normal; color: var(--muted); overflow-wrap: anywhere; }
.u-card__sub { font-weight: 400; }
.u-card__k { color: var(--muted); }
.u-card__n { color: var(--ink-soft); }
.u-card__e { display: flex; align-items: baseline; margin-top: 4px !important; color: var(--ink-soft); text-wrap: pretty; }
.u-card__e .u-dot { position: relative; top: 0.05em; }
.u-card__e .u-join { flex: none; }
/* On the board the card says more (a statement's opening, a pairing's terms), and the
   pointer can move onto it to read it; a click on it selects what it names. */
.u-card.is-board { max-width: min(23rem, calc(100% - 16px)); }
.u-card.is-on { pointer-events: auto; cursor: pointer; }
.u-card__x { margin: 5px 0 2px; font: 400 0.9375rem/1.5 var(--serif); color: var(--ink); overflow-wrap: break-word; }
.u-card__n + .u-card__n { margin-top: 3px !important; }
.u-card__n b { font-weight: 600; color: var(--ink); }
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) .u-card { box-shadow: 0 0 0 1px rgba(0, 0, 0, 0.2), 0 10px 26px -10px rgba(0, 0, 0, 0.6); }
}
:root[data-theme="dark"] .u-card { box-shadow: 0 0 0 1px rgba(0, 0, 0, 0.2), 0 10px 26px -10px rgba(0, 0, 0, 0.6); }
@media (hover: none) { .u-card { display: none; } }
/* The panel's new content rises 6 px into place as a selection changes. Filled
   backwards only, so nothing keeps a transform once it has arrived. */
@keyframes u-arrive { from { opacity: 0; transform: translateY(6px); } }
.u-view.is-arriving, .u-title.is-arriving { animation: u-arrive var(--t-state) var(--ease-out) backwards; }
@media (prefers-reduced-motion: reduce) {
  .u-view.is-arriving, .u-title.is-arriving { animation: none; }
  .u-card, .u-card.is-on { transition: none; }
}

/* The selection has one scrolling reading surface. Section links stay reachable
   without hiding evidence in folds or imposing a second vertical scrollbar. */
.u-sections { position: sticky; top: -4px; z-index: 2; display: flex; flex-wrap: wrap; gap: 2px 12px; margin: -4px 0 12px; padding: 8px 0; background: var(--page); border-bottom: 1px solid var(--rule); }
.u-sections button { border: 0; background: none; color: var(--steel-text); padding: 4px 0; min-height: 28px; cursor: pointer; font: 500 var(--fs-small)/1.4 var(--sans); text-decoration: underline; text-underline-offset: 3px; }
.u-sections button:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }
.u-abstract { font: 400 var(--fs-body)/1.6 var(--serif); color: var(--ink); }
.u-result-previews { margin-left: 0; }
.u-result-previews > li { padding: 8px 0 14px; border-top: 1px solid var(--rule); }
.u-excerpt { margin: 2px 8px 6px; font: 400 var(--fs-body)/1.55 var(--serif); }
.u-excerpt .u-role { margin: 0 0 5px; }
.u-excerpt__text { overflow-wrap: anywhere; }
.u-excerpt__text p { margin: 0 0 8px; }
.u-excerpt__open { margin: 0 8px 8px; }
.u-excerpt .m-d { overflow-x: auto; }
.u-papers > li + li { border-top: 1px solid var(--rule); }
.u-lean-label { font: 500 var(--fs-base)/1.4 var(--serif); }
@media (max-width: 899px) { .u-sections { position: static; } }

/* map + search: usability pass (13 October 2026) */
/* Inline numbers that link (the release sentences) keep a 24 px target without changing the line. */
.u-num, a.u-key__n { display: inline-block; min-width: 24px; min-height: 24px; padding: 3px 4px; margin: -3px -2px; text-align: center; box-sizing: border-box; }
a.u-key__n { color: var(--steel-text); text-decoration: underline; text-underline-offset: 3px; text-decoration-color: color-mix(in oklab, currentColor 40%, transparent); }
.u-key__counted a { display: inline-block; min-height: 24px; padding: 3px 0; margin: -3px 0; }
.u-since { font: 400 var(--fs-small)/1.55 var(--sans); color: var(--ink-soft); margin: 4px 0 12px; padding: 8px 10px; border-left: 2px solid var(--rule-strong); background: var(--surface); border-radius: 0 var(--r-sm) var(--r-sm) 0; }
.u-since__h { color: var(--ink); font-weight: 600; }
.u-since a { color: var(--steel-text); padding: 3px 0; }
/* Search results: the kinds as chips, a heading per kind, and why each matched. */
.u-results__head { margin-bottom: 6px; }
.u-chips { display: flex; flex-wrap: wrap; gap: 6px; margin: 0 0 8px; }
.u-chip { min-height: 28px; padding: 3px 10px; border: 1px solid var(--rule-strong); border-radius: 14px; background: var(--surface); color: var(--ink-soft); font: 500 var(--fs-small)/1.3 var(--sans); cursor: pointer; }
.u-chip:hover { border-color: var(--rule-control); color: var(--ink); }
.u-chip[aria-pressed="true"] { background: var(--ink); border-color: var(--ink); color: var(--page); }
.u-chip:focus-visible, .u-more-btn:focus-visible, .u-suggest__w:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 2px; }
.u-chip__n { font-variant-numeric: tabular-nums; opacity: 0.8; }
.u-results__kind { margin: 10px 0 2px; font: 600 var(--fs-small)/1.4 var(--sans); color: var(--muted); }
.u-row--hit .u-row__t, .u-row--hit .u-row__n, .u-row--hit .u-row__x { grid-column: 1 / -1; overflow-wrap: break-word; }
.u-row__x { display: block; font: 400 var(--fs-small)/1.45 var(--serif); color: var(--ink-soft); overflow-wrap: break-word; }
.u-row__x:empty { display: none; }
.u-row__x code { font: 400 0.75rem/1.45 var(--mono); color: var(--ink-soft); white-space: normal; overflow-wrap: anywhere; }
.u-row__x mark, .u-row__x code mark { background: color-mix(in oklab, var(--steel-text) 22%, transparent); color: inherit; border-radius: 2px; padding: 0 1px; }
.u-row__x .katex { font-size: 1em; }
.u-results__more { display: flex; flex-wrap: wrap; align-items: baseline; gap: 8px; margin: 8px 0 4px; }
.u-more-btn, .u-suggest__w { min-height: 28px; padding: 3px 10px; border: 1px solid var(--rule-strong); border-radius: var(--r-sm); background: var(--surface); color: var(--steel-text); font: 600 var(--fs-small)/1.3 var(--sans); cursor: pointer; }
.u-suggest__w { padding: 2px 8px; font-weight: 500; }
/* A formula wider than its card that takes focus to scroll. */
[data-u-scroller]:focus-visible { outline: 2px solid var(--steel-text); outline-offset: 1px; }

/* round 2: pairing consistency */
/* A short card under a second theorem a Lean statement is paired with points back to its full card. */
.u-bc--l.u-bc--also { background: transparent; padding-block: 0.4em; }
.u-bc--l.u-bc--also .u-bc__lt { font-size: 0.92em; }