/* Component explorer layout.
   The header, the full-window explorer frame (one reading panel, the drawing
   in the rest of the window, controls top right, key bottom left) and the
   reading pages are adapted from the Plectis site's style.css: the docs
   topbar, the map explorers' frame ("Map explorers (5 October 2026)") and
   the theme switch. Map inks and type come from tokens.css. */

*, *::before, *::after { box-sizing: border-box; }
html { -webkit-text-size-adjust: 100%; text-size-adjust: 100%; }
body {
  margin: 0;
  background: var(--page);
  color: var(--ink);
  font-family: var(--font-sans);
  font-size: var(--fs-base);
  line-height: var(--lh-body);
  font-kerning: normal;
}
a { color: var(--accent); text-decoration: none; }
a:hover { text-decoration: underline; text-underline-offset: 0.16em; }
:where(a, button, input, select, [tabindex]):where(:focus-visible) { outline: 2px solid var(--accent); outline-offset: 2px; }
h1, h2, h3 { text-wrap: balance; }
p { text-wrap: pretty; }
code, .code { font-family: var(--font-mono); font-size: 0.86em; }
.skip-link {
  position: absolute; left: -9999px; top: 0; z-index: 50;
  background: var(--ink); color: var(--page); padding: 0.6rem 0.9rem; border-radius: 0 0 6px 0;
}
.skip-link:focus { left: 0; }
.sr-only {
  position: absolute; width: 1px; height: 1px; padding: 0; margin: -1px;
  overflow: hidden; clip: rect(0, 0, 0, 0); white-space: nowrap; border: 0;
}
.theme-switching, .theme-switching * { transition: none !important; }

/* ---- Header ------------------------------------------------------------- */
.topbar {
  position: sticky; top: 0; z-index: 40;
  background: var(--page);
  border-bottom: 1px solid var(--rule);
}
.topbar__inner {
  display: flex; flex-wrap: wrap; align-items: center; gap: 0.35rem 1rem;
  min-height: var(--topbar-h); padding: 0.5rem 24px;
}
/* The lockup: the Plectis plait opens Will Cook's home page, a short upright
   rule, then the flower mark and "Practical Formal Verification" open the
   map. Copied unchanged from wcook04.github.io assets/family/family.css
   (docs/family.md, "The lockup"); its --fam-* names map in tokens.css. */
/* ---------------------------------------------------------------- lockup
   The start of every site's header: the Plectis plait, which opens the home
   page (every website and film), a short upright rule, then this site's own
   mark and name, which open this site's front page. Two links, two jobs; the
   rule says they are two things. The plait is an image (assets/plectis.svg,
   copied beside the site), so it keeps its own day and night palettes; a site
   mark is inline SVG drawn in the site's inks (--fam-mark-warm, --fam-mark-cool,
   --fam-ink), so it follows the page's theme switch. */
.fam-lockup { display: inline-flex; align-items: center; gap: 0.75rem; min-width: 0; }
.fam-lockup__home {
  position: relative; display: inline-grid; place-items: center; flex: none;
  width: 2rem; height: 2rem; border-radius: 8px;
  transition: background-color 160ms var(--fam-ease);
}
.fam-lockup__home img { display: block; width: 1.6rem; height: 1.6rem; }
@media (hover: hover) and (pointer: fine) {
  .fam-lockup__home:hover { background: color-mix(in srgb, var(--fam-ink) 8%, transparent); }
}
.fam-lockup__home:focus-visible { outline: 2px solid var(--fam-accent); outline-offset: 2px; }
.fam-lockup__rule { flex: none; width: 1px; height: 1.35rem; background: var(--fam-rule-strong); }
.fam-lockup__site {
  display: inline-flex; align-items: center; gap: 0.5rem; min-width: 0;
  color: var(--fam-ink); text-decoration: none;
}
.fam-lockup__site:hover .fam-lockup__name { text-decoration: underline; text-decoration-color: var(--fam-rule-strong); text-underline-offset: 0.18em; }
.fam-lockup__site:focus-visible { outline: 2px solid var(--fam-accent); outline-offset: 3px; border-radius: 4px; }
.fam-lockup__name {
  font-family: var(--fam-serif); font-size: 1.18rem; font-weight: 500; line-height: 1.1; letter-spacing: -0.008em;
  white-space: nowrap; overflow: hidden; text-overflow: ellipsis;
}
.fam-mark { display: block; flex: none; width: 1.5rem; height: 1.5rem; overflow: visible; }
.fam-mark * { vector-effect: non-scaling-stroke; }
.fam-mark__ink { fill: none; stroke: var(--fam-ink); stroke-width: 1.8; stroke-linecap: round; }
.fam-mark__cool { fill: none; stroke: var(--fam-mark-cool, var(--fam-accent)); stroke-width: 1.8; stroke-linecap: round; }
.fam-mark__warm { fill: none; stroke: var(--fam-mark-warm, var(--fam-ink)); stroke-width: 1.4; }
.fam-mark__warm-fill { fill: var(--fam-mark-warm, var(--fam-ink)); }
.fam-mark__cool-fill { fill: var(--fam-mark-cool, var(--fam-accent)); }
.fam-mark__page-fill { fill: var(--fam-page); }
/* A phone keeps both links; a long name gives way first. */
@media (max-width: 420px) { .fam-lockup { gap: 0.55rem; } .fam-lockup__name { font-size: 1.05rem; } }
@media (forced-colors: active) { .fam-lockup__rule { background: CanvasText; } }
.fam-lockup a:hover { text-decoration: none; }
.topbar .fam-lockup { flex: 0 1 auto; }
.topbar__links { margin-left: auto; display: flex; flex-wrap: wrap; align-items: center; gap: 0.35rem 1.3rem; }
.topbar__links a { color: var(--ink-soft); font-size: 0.9rem; white-space: nowrap; }
.topbar__links a[aria-current="page"] { color: var(--ink); font-weight: 600; }
.topbar__links a:hover { color: var(--accent); text-decoration: none; }
.theme-toggle {
  flex: none; display: inline-flex; align-items: center; margin: 0; padding: 0;
  border: 0; background: none; cursor: pointer; line-height: 0;
}
.theme-toggle__track {
  position: relative; display: block; width: 2.9rem; height: 1.6rem; border-radius: var(--r-pill);
  background: var(--surface-sunk); border: 1px solid var(--rule-strong);
}
.theme-toggle__knob {
  position: absolute; top: 50%; left: 0.2rem; width: 1.2rem; height: 1.2rem; border-radius: 50%;
  background: var(--ink); transform: translateY(-50%);
  transition: transform 220ms var(--ease-out);
}
.theme-toggle[aria-checked="true"] .theme-toggle__knob { transform: translate(1.3rem, -50%); }
.theme-toggle:focus-visible { outline: none; }
.theme-toggle:focus-visible .theme-toggle__track { outline: 2px solid var(--accent); outline-offset: 3px; }
/* On a phone the links wrap under the lockup; the lockup's 32px plait is
   taller than the old wordmark, so the rows sit a little closer and the
   header keeps its height. */
@media (max-width: 600px) { .topbar__inner { padding-inline: 16px; row-gap: 0.25rem; } }

/* ---- The explorer frame (style.css "Map explorers") ------------------------ */
html.is-explorer, html.is-explorer body { height: 100%; }
html.is-explorer body { overflow: hidden; }
.explorer {
  --explorer-panel: clamp(340px, 26vw, 420px);
  --explorer-pad: clamp(18px, 1.7vw, 28px);
  position: relative;
  display: grid; grid-template-columns: var(--explorer-panel) minmax(0, 1fr);
  height: calc(100dvh - var(--topbar-h) - 1px);
  background: var(--page);
}
html.is-map-fullscreen .topbar { display: none; }
.explorer.is-fullscreen { position: fixed; inset: 0; z-index: 1000; width: 100%; height: 100dvh; }
.explorer__panel {
  position: relative; z-index: 2; min-height: 0; display: flex; flex-direction: column;
  border-right: 1px solid var(--home-line-strong); background: var(--page);
}
.explorer__head { flex: none; padding: 18px var(--explorer-pad) 14px; border-bottom: 1px solid var(--home-line); }
.explorer__title {
  margin: 0; font-family: var(--font-serif); font-weight: 500;
  font-size: clamp(1.5rem, 1.1rem + 0.8vw, 1.95rem); line-height: 1.12; letter-spacing: -0.005em;
}
.explorer__body {
  flex: 1 1 auto; min-height: 0; overflow-y: auto; overscroll-behavior: contain;
  scrollbar-gutter: stable; scrollbar-width: thin;
  padding: 16px var(--explorer-pad) 40px;
}
.explorer__foot {
  flex: none; padding: 8px var(--explorer-pad); border-top: 1px solid var(--home-line);
  font-size: var(--fs-micro); color: var(--faint);
}
.explorer__stage { position: relative; min-width: 0; min-height: 0; overflow: hidden; background: var(--page); }
.explorer__stage > canvas { display: block; width: 100%; height: 100%; touch-action: none; }
.explorer__stage > canvas:focus-visible { outline: 2px solid var(--accent); outline-offset: -2px; }
.explorer__tools { position: absolute; z-index: 5; top: 14px; right: 14px; display: flex; align-items: center; gap: 6px; }
.explorer__legend {
  position: absolute; z-index: 4; left: 18px; bottom: 14px; right: 18px;
  display: flex; flex-wrap: wrap; align-items: center; gap: 0.35rem 1.1rem;
  pointer-events: none; font-size: 0.85rem; color: var(--muted);
  transition: opacity var(--motion-state) var(--ease-out);
}
.explorer__legend > * { pointer-events: auto; }
.explorer-tool {
  display: inline-flex; align-items: center; justify-content: center; gap: 0.4rem;
  min-height: 36px; min-width: 36px; padding: 0 0.85rem;
  border: 0; border-radius: var(--r-pill); cursor: pointer;
  font: inherit; font-size: 0.85rem; font-weight: 600; line-height: 1; color: var(--ink-soft);
  background: color-mix(in srgb, var(--page) 78%, transparent);
  box-shadow: 0 0 0 1px var(--home-line-strong);
  backdrop-filter: blur(6px); -webkit-backdrop-filter: blur(6px);
  transition: color var(--motion-fast) var(--ease-out), box-shadow var(--motion-fast) var(--ease-out);
}
.explorer-tool--icon { padding: 0; width: 36px; font-size: 1.05rem; }
.explorer-tool svg { width: 15px; height: 15px; flex: none; }
.explorer-tool:hover { color: var(--ink); box-shadow: 0 0 0 1px var(--home-ember); }
.explorer-tool[aria-pressed="true"] { color: var(--ink); box-shadow: 0 0 0 1px var(--home-ember); }
.explorer-tool:active { transform: scale(0.97); }
.explorer__zoom { display: inline-flex; border-radius: var(--r-pill); box-shadow: 0 0 0 1px var(--home-line-strong); }
.explorer__zoom .explorer-tool { box-shadow: none; border-radius: 0; }
.explorer__zoom .explorer-tool:first-child { border-radius: var(--r-pill) 0 0 var(--r-pill); }
.explorer__zoom .explorer-tool:last-child { border-radius: 0 var(--r-pill) var(--r-pill) 0; border-left: 1px solid var(--home-line); }
.explorer.is-panel-collapsed { grid-template-columns: 0 minmax(0, 1fr); }
.explorer.is-panel-collapsed .explorer__panel { visibility: hidden; overflow: hidden; border-right: 0; }
.explorer__views { display: none; }
.explorer__status {
  position: absolute; inset: 0; display: grid; place-items: center; z-index: 3; padding: 24px;
  text-align: center; color: var(--muted); font-size: var(--fs-body);
}
.explorer__status[hidden] { display: none; }
@media (max-width: 899px) {
  html.is-explorer body { overflow: auto; }
  .explorer { grid-template-columns: minmax(0, 1fr); grid-template-rows: auto minmax(0, 1fr); height: calc(100dvh - var(--topbar-h) - 1px); }
  .explorer__views { display: flex; gap: 6px; padding: 10px 16px; border-bottom: 1px solid var(--home-line); }
  .explorer[data-explorer-shown="map"] .explorer__panel { display: none; }
  .explorer[data-explorer-shown="details"] .explorer__stage { display: none; }
  .explorer__panel { border-right: 0; min-height: 0; }
  .explorer__legend { font-size: 0.78rem; gap: 0.2rem 0.8rem; left: 12px; right: 12px; bottom: 10px; }
  .explorer__tools { top: 10px; right: 10px; }
  .explorer__tools [data-explorer-panel-toggle] { display: none; }
}

/* ---- Map key ---------------------------------------------------------------- */
.key { display: inline-flex; align-items: center; gap: 0.45rem; white-space: nowrap; }
.key svg { width: 13px; height: 13px; flex: none; overflow: visible; }
.mark { color: var(--ink); }
.mark--proved { color: var(--weave-red-glow); }
:root:not([data-theme="dark"]) .mark--proved { color: var(--weave-red); }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .mark--proved { color: var(--weave-red-glow); } }
.mark--stated { color: var(--weave-azure-glow); }
.mark--faint { color: var(--m-faint); }

/* ---- Panel parts ------------------------------------------------------------ */
.panel-lede { margin: 0.5rem 0 0; font-size: 0.95rem; line-height: 1.5; color: var(--ink-soft); max-width: 46ch; }
.find { position: relative; margin-top: 0.9rem; }
.find input {
  width: 100%; min-height: 40px; padding: 0.5rem 0.8rem; border-radius: var(--r-sm);
  border: 1px solid var(--rule-control); background: var(--surface); color: var(--ink);
  font: inherit; font-size: 0.95rem;
}
.find input::placeholder { color: var(--faint); }
.tabs { display: flex; align-items: center; justify-content: space-between; gap: 0.75rem; margin-top: 0.85rem; flex-wrap: wrap; }
.tabs__group { display: flex; gap: 1rem; }
.tab {
  border: 0; background: none; padding: 0.3rem 0; cursor: pointer; font: inherit; font-size: 0.95rem;
  color: var(--muted); border-bottom: 2px solid transparent; min-height: 30px;
}
.tab[aria-pressed="true"] { color: var(--ink); font-weight: 600; border-bottom-color: var(--home-ember); }
.util {
  display: inline-flex; align-items: center; gap: 0.35rem; min-height: 32px; padding: 0 0.75rem;
  border: 1px solid var(--home-line-strong); border-radius: var(--r-pill); background: none; color: var(--ink-soft);
  font: inherit; font-size: 0.82rem; font-weight: 600; cursor: pointer;
}
.util[aria-pressed="true"], .util:hover { color: var(--ink); border-color: var(--home-ember); }
.filtered {
  display: flex; align-items: center; justify-content: space-between; gap: 0.6rem; margin-top: 0.7rem;
  padding: 0.45rem 0.7rem; border-radius: var(--r-md); background: var(--surface-sunk); font-size: var(--fs-meta);
}
.filtered[hidden] { display: none; }
.textbtn { border: 0; background: none; padding: 0.1rem 0.2rem; font: inherit; font-size: inherit; color: var(--accent); cursor: pointer; }
.textbtn:hover { text-decoration: underline; }

.section-title { margin: 1.4rem 0 0.5rem; font-family: var(--font-serif); font-size: 1.12rem; font-weight: 600; }
.section-title:first-child { margin-top: 0.2rem; }
.muted { color: var(--muted); }
.small { font-size: var(--fs-meta); }
.figures { font-variant-numeric: tabular-nums; }

.family-rows { list-style: none; margin: 0; padding: 0; border-top: 1px solid var(--home-line); }
.family-row { border-bottom: 1px solid var(--home-line); }
.family-row button {
  display: grid; grid-template-columns: 1fr auto; gap: 0.15rem 0.8rem; width: 100%; text-align: left;
  padding: 0.6rem 0.2rem; background: none; border: 0; cursor: pointer; font: inherit; color: var(--ink);
}
.family-row button:hover .family-row__name { color: var(--accent); }
.family-row__name { font-size: 0.98rem; }
.family-row__count { font-variant-numeric: tabular-nums; color: var(--muted); font-size: 0.92rem; }
.family-row__tally { grid-column: 1 / -1; font-size: var(--fs-meta); color: var(--muted); }
.family-row__marks { grid-column: 1 / -1; display: flex; flex-wrap: wrap; gap: 3px; margin-top: 0.15rem; }
.family-row__marks svg { width: 11px; height: 11px; }

.rows { list-style: none; margin: 0.4rem 0 0; padding: 0; }
.row { border-bottom: 1px solid var(--home-line); }
.row a, .row button.row__go {
  display: grid; grid-template-columns: 14px 1fr; gap: 0.1rem 0.6rem; padding: 0.55rem 0.15rem;
  color: var(--ink); text-decoration: none; background: none; border: 0; width: 100%; text-align: left; font: inherit; cursor: pointer;
}
.row a:hover .row__title, .row button.row__go:hover .row__title { color: var(--accent); }
.row svg { width: 12px; height: 12px; margin-top: 0.38rem; }
.row__title { font-size: 0.95rem; line-height: 1.35; }
.row__sub { grid-column: 2; font-size: var(--fs-meta); color: var(--muted); line-height: 1.4; }
.more { margin-top: 0.8rem; }
.btn {
  display: inline-flex; align-items: center; justify-content: center; gap: 0.45rem; min-height: 38px; padding: 0 1rem;
  border-radius: var(--r-pill); border: 1px solid var(--rule-control); background: var(--surface); color: var(--ink);
  font: inherit; font-size: 0.9rem; font-weight: 600; cursor: pointer; text-decoration: none;
}
.btn:hover { border-color: var(--home-ember); text-decoration: none; }
.btn--ink { background: var(--ink); color: var(--page); border-color: var(--ink); }
.btn--ink:hover { color: var(--page); }
.btn:active { transform: scale(0.97); }
.actions { display: flex; flex-wrap: wrap; gap: 0.5rem; margin-top: 0.9rem; }

.facet { margin: 0 0 1.1rem; }
.facet h3 { margin: 0 0 0.4rem; font-size: 0.95rem; font-weight: 600; }
.facet__choices { display: flex; flex-wrap: wrap; gap: 0.35rem; }
.chip {
  display: inline-flex; align-items: center; gap: 0.4rem; min-height: 30px; padding: 0 0.7rem;
  border-radius: var(--r-pill); border: 1px solid var(--home-line-strong); background: none; color: var(--ink-soft);
  font: inherit; font-size: 0.84rem; cursor: pointer;
}
.chip[aria-pressed="true"] { color: var(--ink); border-color: var(--home-ember); background: color-mix(in srgb, var(--home-ember) 10%, transparent); }
.chip__n { color: var(--faint); font-variant-numeric: tabular-nums; }

.state {
  margin: 0.8rem 0; padding: 0.7rem 0.85rem; border-radius: var(--r-md);
  background: var(--surface-sunk); font-size: var(--fs-meta); line-height: 1.5;
}
.state--error { box-shadow: inset 3px 0 0 var(--weave-red); }
.state strong { font-weight: 650; }

/* A component card in the panel, and the reading pages. */
.card-kind { font-size: var(--fs-small); color: var(--muted); margin: 0 0 0.25rem; display: flex; gap: 0.45rem; align-items: center; }
.card-kind svg { width: 12px; height: 12px; }
.card-title { margin: 0; font-family: var(--font-serif); font-size: 1.45rem; font-weight: 500; line-height: 1.18; }
.card-summary { margin: 0.45rem 0 0; color: var(--ink-soft); }
.limit {
  margin: 0.9rem 0 0; padding: 0.7rem 0.85rem; border-radius: var(--r-md);
  background: color-mix(in srgb, var(--weave-azure-glow) 9%, var(--page)); font-size: 0.93rem; line-height: 1.5;
}
.limit__label { display: block; font-size: var(--fs-small); font-weight: 650; color: var(--ink-soft); margin-bottom: 0.15rem; }
.facts { list-style: none; margin: 0.4rem 0 0; padding: 0; }
.fact { display: grid; grid-template-columns: 16px 1fr; gap: 0.6rem; padding: 0.5rem 0; border-bottom: 1px solid var(--home-line); font-size: 0.92rem; line-height: 1.45; }
.fact svg { width: 12px; height: 12px; margin-top: 0.3rem; }
.fact__caution { display: block; color: var(--muted); font-size: var(--fs-meta); }
.fact--unknown .fact__text { font-style: italic; }
.ref { font-family: var(--font-mono); font-size: 0.82rem; word-break: break-word; color: var(--code-ink); }
.ref-list { list-style: none; margin: 0.3rem 0 0; padding: 0; }
.ref-list li { padding: 0.25rem 0; font-size: var(--fs-meta); }
.ref-list .absent { color: var(--muted); }
.cmd {
  display: block; margin: 0.4rem 0 0; padding: 0.6rem 0.7rem; border-radius: var(--r-md); background: var(--code-bg);
  color: var(--code-ink); font-family: var(--font-mono); font-size: 0.8rem; line-height: 1.5; white-space: pre-wrap; word-break: break-word;
}
.copy { margin-top: 0.35rem; }

/* ---- Reading pages -------------------------------------------------------- */
.page { width: min(1180px, calc(100% - 48px)); margin: 0 auto; padding: 28px 0 80px; }
.trail { font-size: var(--fs-meta); color: var(--muted); display: flex; flex-wrap: wrap; gap: 0.4rem; align-items: center; }
.trail a { color: var(--muted); }
.page-title { margin: 0.6rem 0 0; font-family: var(--font-serif); font-weight: 500; font-size: clamp(1.9rem, 1.4rem + 1.4vw, 2.7rem); line-height: 1.1; letter-spacing: -0.01em; }
.page-lede { margin: 0.6rem 0 0; font-size: var(--fs-lede); color: var(--ink-soft); max-width: 62ch; }
.page h2 { font-family: var(--font-serif); font-weight: 500; font-size: 1.5rem; margin: 2.6rem 0 0.6rem; }
.page h3 { font-size: 1.02rem; font-weight: 650; margin: 1.4rem 0 0.4rem; }
.prose { max-width: 68ch; }
.reader { display: grid; grid-template-columns: minmax(0, 7fr) minmax(0, 5fr); gap: 48px; align-items: start; margin-top: 1.6rem; }
.reader__figure { position: sticky; top: calc(var(--topbar-h) + 20px); }
.reader__steps > section { padding: 0 0 1.6rem; scroll-margin-top: calc(var(--topbar-h) + 16px); }
.reader__steps > section > h2:first-child { margin-top: 0.4rem; }
@media (max-width: 960px) {
  .reader { grid-template-columns: minmax(0, 1fr); }
  .reader__figure { position: relative; top: 0; order: -1; }
}
.chain-figure { width: 100%; height: auto; display: block; }
.chain-figure text { font-family: var(--font-sans); }
.chain-step { transition: opacity var(--motion-state) var(--ease-out); }
.chain-figure.has-current .chain-step:not(.is-current) { opacity: 0.38; }
.statement {
  margin: 0.6rem 0 0; padding: 0.9rem 1rem; border-radius: var(--r-md); background: var(--surface);
  box-shadow: 0 0 0 1px var(--home-line-strong); font-family: var(--font-serif); font-size: 1.08rem; line-height: 1.5;
}
.split { display: grid; grid-template-columns: repeat(auto-fit, minmax(240px, 1fr)); gap: 0.8rem 1.6rem; }
.table { width: 100%; border-collapse: collapse; font-size: 0.9rem; }
.table th, .table td { text-align: left; padding: 0.5rem 0.6rem 0.5rem 0; border-bottom: 1px solid var(--home-line); vertical-align: top; }
.table th { font-weight: 650; color: var(--ink-soft); font-size: var(--fs-meta); }
.table td.num, .table th.num { text-align: right; font-variant-numeric: tabular-nums; }

/* Coverage squares (lean-exposition site/src/checks/CheckMap.tsx and checks.css). */
.measures { display: grid; gap: 1.6rem; margin-top: 1rem; }
.measure__head { display: flex; flex-wrap: wrap; align-items: baseline; justify-content: space-between; gap: 0.3rem 1rem; }
.measure__name { font-weight: 650; font-size: 1rem; }
.measure__count { font-variant-numeric: tabular-nums; color: var(--ink-soft); font-size: 0.95rem; }
.measure__kind { margin: 0.1rem 0 0.5rem; color: var(--muted); font-size: var(--fs-meta); }
.squares { display: flex; flex-wrap: wrap; gap: 2px; }
.squares__family { display: flex; flex-wrap: wrap; gap: 2px; padding-right: 7px; margin-right: 5px; border-right: 1px solid var(--home-line-strong); }
.squares__family:last-child { border-right: 0; }
.sq { width: 10px; height: 10px; border-radius: 2px; display: inline-block; }
.sq--on { background: var(--ink); }
.sq--proved { background: var(--weave-red-glow); }
:root[data-theme="light"] .sq--proved { background: var(--weave-red); }
.sq--off { box-shadow: inset 0 0 0 1px var(--home-line-strong); }
.sq--unknown { background: repeating-linear-gradient(45deg, transparent 0 3px, color-mix(in srgb, var(--muted) 45%, transparent) 3px 4px); box-shadow: inset 0 0 0 1px var(--home-line-strong); }
a.sq:hover { outline: 2px solid var(--accent); outline-offset: 1px; }
.note { font-size: var(--fs-meta); color: var(--muted); margin: 0.3rem 0 0; }

/* Related records. */
.graph-layout { display: grid; grid-template-columns: minmax(0, 7fr) minmax(0, 5fr); gap: 40px; align-items: start; margin-top: 1.2rem; }
@media (max-width: 960px) { .graph-layout { grid-template-columns: minmax(0, 1fr); } }
.graph-figure { width: 100%; height: auto; display: block; }
.graph-figure text { font-family: var(--font-sans); font-size: 11px; fill: var(--ink-soft); }
.edge-groups h3 { margin-top: 1.2rem; }
.controls { display: flex; flex-wrap: wrap; gap: 0.6rem 1rem; align-items: center; margin-top: 1rem; font-size: var(--fs-meta); }
.controls select, .controls input {
  font: inherit; padding: 0.3rem 0.5rem; border-radius: var(--r-sm); border: 1px solid var(--rule-control); background: var(--surface); color: var(--ink);
}

@media (prefers-reduced-motion: reduce) {
  *, *::before, *::after { transition-duration: 0ms !important; animation-duration: 0ms !important; }
}

/* ---- Inks of the coverage rings ------------------------------------------- */
/* One meaning per ink, on the map and in the panel: red where a machine
   checked and the result was kept, azure where something is stated or
   configured, amber for saved earlier runs, a hatch where nothing is
   established, and a faint cell where no such check is recorded. */
.ink-ran { --ink-fill: var(--weave-red); }
.ink-stated { --ink-fill: color-mix(in oklab, var(--weave-azure-glow) 62%, var(--page)); }
.ink-saved { --ink-fill: var(--m-ember); }
.ink-unknown { --ink-fill: transparent; }
:root[data-theme="dark"] .ink-ran { --ink-fill: var(--weave-red-glow); }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .ink-ran { --ink-fill: var(--weave-red-glow); } }
.swatch {
  display: inline-block; flex: none; width: 12px; height: 12px; border-radius: 3px;
  background: var(--ink-fill, var(--home-line));
}
.swatch.ink-unknown { background: repeating-linear-gradient(135deg, transparent 0 2.4px, color-mix(in srgb, var(--muted) 70%, transparent) 2.4px 3.4px); box-shadow: inset 0 0 0 1px var(--home-line-strong); }
.swatch.is-empty { background: color-mix(in srgb, var(--ink) 8%, transparent); box-shadow: inset 0 0 0 1px var(--home-line-strong); }
.ink-ran-text { color: var(--weave-red); }
:root[data-theme="dark"] .ink-ran-text { color: var(--weave-red-glow); }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .ink-ran-text { color: var(--weave-red-glow); } }
.ink-unknown-text { color: var(--muted); }

/* The ledger: four plain counts, each with what it counts. */
.ledger { display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 0.9rem 1.2rem; margin: 0.2rem 0 0.4rem; }
.ledger__item { display: flex; flex-direction: column; gap: 0.1rem; }
.ledger__n { font-family: var(--font-serif); font-size: 2rem; line-height: 1; font-variant-numeric: lining-nums tabular-nums; letter-spacing: -0.01em; }
.ledger__l { font-size: var(--fs-meta); color: var(--muted); line-height: 1.35; }

/* The rings as strips. */
.rings { list-style: none; margin: 0.5rem 0 0; padding: 0; border-top: 1px solid var(--home-line); }
.ring-row { border-bottom: 1px solid var(--home-line); }
.ring-row__go {
  display: grid; grid-template-columns: minmax(0, 1fr) auto; gap: 0.12rem 0.8rem; align-items: center;
  width: 100%; padding: 0.55rem 0.35rem; text-align: left; background: none; border: 0; border-radius: var(--r-sm);
  font: inherit; color: var(--ink); cursor: pointer;
  transition: background var(--motion-fast) var(--ease-out);
}
.ring-row__go:hover, .ring-row.is-pinned .ring-row__go { background: color-mix(in srgb, var(--ink) 5%, transparent); }
.ring-row__title { display: inline-flex; align-items: center; gap: 0.55rem; font-weight: 600; font-size: 0.95rem; }
.ring-row__count { font-size: 0.9rem; color: var(--ink-soft); }
.ring-row__count.is-unknown { font-style: italic; color: var(--muted); }
.ring-row__by { grid-column: 1 / -1; font-size: var(--fs-small); color: var(--muted); padding-left: calc(12px + 0.55rem); }
.strip { grid-column: 1 / -1; display: block; width: calc(100% - 12px - 0.55rem); height: 12px; margin: 0.25rem 0 0 calc(12px + 0.55rem); }
.strip .cell--empty { fill: color-mix(in srgb, var(--ink) 9%, transparent); }
.strip .cell--has { fill: var(--ink-fill); }
.strip.ink-unknown .cell { fill: color-mix(in srgb, var(--muted) 38%, transparent); }

/* A component's own column of the rings. */
.column { list-style: none; margin: 0.35rem 0 0; padding: 0; }
.column__row {
  display: grid; grid-template-columns: 12px minmax(0, 1fr) auto; gap: 0.1rem 0.6rem; align-items: center;
  padding: 0.45rem 0; border-bottom: 1px solid var(--home-line); font-size: 0.92rem;
}
.column__title { font-weight: 600; }
.column__by { font-size: var(--fs-small); color: var(--muted); text-align: right; }
.column__words { grid-column: 2 / -1; font-size: var(--fs-meta); color: var(--ink-soft); line-height: 1.45; }
.column__row.is-empty .column__title { font-weight: 500; color: var(--muted); }
.column__row.is-empty .column__words { color: var(--muted); }

/* Saved runs and rules. */
.records li { display: grid; grid-template-columns: 10px minmax(0, 1fr); column-gap: 0.55rem; }
.records li > :not(.rec-dot) { grid-column: 2; }
.records br { display: none; }
.rec-dot { grid-row: span 2; width: 8px; height: 8px; margin-top: 0.38rem; border-radius: 50%; background: var(--m-ember); }
.rec-dot.is-absent { background: none; box-shadow: inset 0 0 0 1px var(--muted); }
.rec-dot.is-blocked { background: none; box-shadow: inset 0 0 0 2px var(--m-ember); }
.doctrine { list-style: none; margin: 0.3rem 0 0; padding: 0; }
.doctrine li { padding: 0.32rem 0; border-bottom: 1px solid var(--home-line); font-size: 0.92rem; }
.doc-id { display: inline-block; min-width: 3.2em; font-family: var(--font-mono); font-size: 0.78rem; color: var(--accent); }
.doc-id--anti_principle { color: var(--weave-red); }
.rows--dense .row a, .rows--dense .row button.row__go { padding: 0.38rem 0.15rem; }
.rows--dense code.row__sub { font-size: 0.76rem; }
.route-list { list-style: none; margin: 0.4rem 0 0; padding: 0; columns: 2 20rem; column-gap: 1.6rem; font-size: var(--fs-meta); }
.route-list li { break-inside: avoid; padding: 0.2rem 0; }
.route-list code { color: var(--muted); font-size: 0.76rem; }
.inline-list { display: inline; margin: 0; padding: 0; list-style: none; }
.inline-list li { display: inline; }
.inline-list li + li::before { content: ' and '; }

/* ---- Dafny, as retained -------------------------------------------------- */
.spec { display: grid; gap: 0.5rem; margin-top: 0.5rem; }
.excerpt { border-radius: var(--r-md); background: var(--code-bg); box-shadow: 0 0 0 1px var(--home-line); overflow: hidden; }
.excerpt > summary {
  display: flex; flex-wrap: wrap; align-items: baseline; gap: 0.2rem 0.6rem; padding: 0.5rem 0.75rem;
  cursor: pointer; list-style: none; font-size: var(--fs-meta);
}
.excerpt > summary::-webkit-details-marker { display: none; }
.excerpt > summary::before { content: '▸'; color: var(--faint); font-size: 0.75rem; transition: transform var(--motion-fast) var(--ease-out); }
.excerpt[open] > summary::before { transform: rotate(90deg); }
.excerpt__kind { color: var(--muted); font-size: var(--fs-small); text-transform: lowercase; font-variant: small-caps; letter-spacing: 0.04em; }
.excerpt__name { font-weight: 650; color: var(--code-ink); font-size: 0.86rem; }
.excerpt__role { font-size: var(--fs-small); color: var(--accent); }
.excerpt__lines { margin-left: auto; font-size: var(--fs-small); color: var(--faint); }
.excerpt__src { margin: 0; padding: 0.35rem 0.75rem 0.55rem; font-size: var(--fs-small); }
.excerpt__src a { font-family: var(--font-mono); font-size: 0.74rem; }
.dafny {
  margin: 0; padding: 0.25rem 0 0.55rem; overflow-x: auto; font-family: var(--font-mono);
  font-size: 0.78rem; line-height: 1.6; color: var(--code-ink); tab-size: 2;
}
.dafny code { font-size: inherit; display: block; min-width: max-content; }
.dafny__line { display: grid; grid-template-columns: 3.2em auto; }
.dafny__no { padding-right: 0.9em; text-align: right; color: var(--faint); user-select: none; font-variant-numeric: tabular-nums; }
.dafny__text { white-space: pre; padding-right: 0.9rem; }
.tok-k { color: var(--accent); font-weight: 600; }
.tok-t { color: color-mix(in oklab, var(--accent) 70%, var(--code-ink)); }
.tok-d { color: var(--weave-red); font-weight: 650; }
:root[data-theme="dark"] .tok-d { color: var(--weave-red-glow); }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .tok-d { color: var(--weave-red-glow); } }
.tok-n { color: var(--link-ext); }
.tok-o { color: var(--ink-soft); font-weight: 600; }
.tok-c, .tok-s { color: var(--muted); }

/* A broken variant: the specified line over the variant's line. */
.variants { display: grid; gap: 0.7rem; margin-top: 0.4rem; }
.variant { padding: 0.6rem 0.75rem 0.55rem; border-radius: var(--r-md); box-shadow: 0 0 0 1px var(--home-line-strong); }
.variant__head { display: flex; align-items: center; gap: 0.5rem; margin: 0 0 0.4rem; font-size: var(--fs-meta); }
.variant__cross { font-weight: 700; color: var(--ink); }
.diff { display: grid; gap: 2px; margin: 0.2rem 0; overflow-x: auto; }
.diff__row { display: grid; grid-template-columns: 4.4em 2.6em auto; align-items: baseline; font-size: 0.78rem; border-radius: 4px; padding: 0.15rem 0.4rem; }
.diff__row code { white-space: pre; font-size: inherit; color: var(--code-ink); }
.diff__row--was { background: color-mix(in srgb, var(--weave-azure-glow) 10%, transparent); }
.diff__row--now { background: color-mix(in srgb, var(--ink) 6%, transparent); }
.diff__mark { font-size: var(--fs-small); color: var(--muted); font-variant: small-caps; letter-spacing: 0.04em; }
.diff__no { color: var(--faint); }
.diff mark { background: none; color: inherit; font-weight: 700; border-radius: 3px; padding: 0 0.1em; }
.diff__was { box-shadow: inset 0 -2px 0 var(--weave-azure-glow); }
.diff__now { text-decoration: line-through; text-decoration-color: var(--weave-red); text-decoration-thickness: 2px; }

/* The ownership repair, played through. */
.own { margin: 0.5rem 0 0; padding: 0.8rem 0.9rem 0.7rem; border-radius: var(--r-lg); background: var(--surface); box-shadow: 0 0 0 1px var(--home-line-strong); }
.own__head { display: flex; flex-wrap: wrap; align-items: center; gap: 0.3rem 0.8rem; margin-bottom: 0.6rem; }
.own__title { margin: 0; font-family: var(--font-serif); font-size: 1.02rem; font-weight: 600; }
.own__path { font-size: 0.74rem; color: var(--muted); }
.segs { display: inline-flex; margin-left: auto; border-radius: var(--r-pill); box-shadow: 0 0 0 1px var(--home-line-strong); overflow: hidden; }
.seg { border: 0; background: none; padding: 0.35rem 0.75rem; font: inherit; font-size: var(--fs-small); font-weight: 600; color: var(--muted); cursor: pointer; min-height: 30px; }
.seg + .seg { border-left: 1px solid var(--home-line); }
.seg[aria-pressed="true"] { background: var(--ink); color: var(--page); }
.own__row { display: grid; grid-template-columns: 4.6em minmax(0, auto) minmax(0, 1fr); align-items: center; gap: 0.4rem 0.8rem; padding: 0.45rem 0; border-top: 1px solid var(--home-line); }
.own__order { font-size: var(--fs-small); color: var(--muted); }
.own__claims { display: inline-flex; align-items: center; gap: 0.4rem; flex-wrap: wrap; }
.own__then { font-size: var(--fs-small); color: var(--faint); }
.claim {
  display: inline-flex; flex-direction: column; padding: 0.22rem 0.55rem; border-radius: var(--r-sm); line-height: 1.2;
  box-shadow: inset 0 0 0 1px var(--home-line-strong); transition: box-shadow var(--motion-state) var(--ease-out), background var(--motion-state) var(--ease-out);
}
.claim__state { font-weight: 650; font-size: 0.82rem; }
.claim__session { font-size: 0.7rem; color: var(--muted); }
.claim--live .claim__state { color: var(--accent); }
.claim--stale .claim__state { color: var(--muted); }
.claim.is-picked { box-shadow: inset 0 0 0 2px var(--ink); background: color-mix(in srgb, var(--ink) 6%, transparent); }
.own__decision { font-size: 0.86rem; color: var(--ink-soft); }
.own__code { font-family: var(--font-mono); font-size: 0.76rem; padding: 0.05rem 0.35rem; border-radius: 4px; background: color-mix(in srgb, var(--ink) 7%, transparent); color: var(--code-ink); }
.own__code.is-unsafe { box-shadow: inset 0 0 0 1px var(--weave-red); }
.own__verdict { margin: 0.55rem 0 0.2rem; font-size: 0.9rem; font-weight: 600; }
.own__verdict.is-unsafe { color: var(--weave-red); }
:root[data-theme="dark"] .own__verdict.is-unsafe { color: var(--weave-red-glow); }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .own__verdict.is-unsafe { color: var(--weave-red-glow); } }
@media (max-width: 560px) {
  .own__row { grid-template-columns: minmax(0, 1fr); }
  .segs { margin-left: 0; }
}

/* The rings' key, top left of the drawing: a slice of the map's top. */
.explorer__rings {
  position: absolute; z-index: 4; top: 14px; left: 18px;
  padding: 0.5rem 0.65rem 0.45rem; border-radius: var(--r-md);
  background: color-mix(in srgb, var(--page) 82%, transparent);
  box-shadow: 0 0 0 1px var(--home-line);
  backdrop-filter: blur(6px); -webkit-backdrop-filter: blur(6px);
  font-size: 0.74rem; color: var(--ink-soft);
  transition: opacity var(--motion-state) var(--ease-out);
}
.ringkey__title { margin: 0 0 0.35rem; font-size: 0.72rem; font-weight: 650; letter-spacing: 0.02em; color: var(--muted); }
.ringkey { list-style: none; margin: 0; padding: 0; display: grid; gap: 2px; }
.ringkey__row { display: grid; grid-template-columns: 1.6em 22px max-content minmax(2.6em, auto); align-items: center; gap: 0.45rem; line-height: 1.3; cursor: default; white-space: nowrap; }
.ringkey__row .swatch { width: 22px; height: 9px; border-radius: 2px; }
.ringkey__by { color: var(--faint); font-size: 0.68rem; padding-left: 0.4rem; }
.ringkey__base { display: flex; align-items: center; gap: 0.45rem; margin: 0.3rem 0 0; padding-top: 0.3rem; border-top: 1px solid var(--home-line); font-size: 0.72rem; color: var(--muted); }
.ringkey__mark { width: 22px; height: 9px; display: inline-grid; place-items: center; }
.ringkey__mark::after { content: ''; width: 7px; height: 7px; border-radius: 50%; border: 1.4px solid var(--ink); }

/* A proof page gives its text column the room code needs. */
.reader--proof { grid-template-columns: minmax(0, 8fr) minmax(0, 3fr); gap: 40px; }
.reader--proof .reader__steps { max-width: none; }
.reader--proof .reader__steps > section > p, .reader--proof .statement, .reader--proof .limit, .reader--proof .split, .reader--proof .facts { max-width: 72ch; }
@media (max-width: 960px) { .reader--proof { grid-template-columns: minmax(0, 1fr); } }
a.ref { color: var(--accent); }
a.ref:hover { text-decoration: underline; }

/* ---- Plain words first ------------------------------------------------------ */
.card-plain { margin: 0.6rem 0 0.2rem; font-family: var(--font-serif); font-size: 1.08rem; line-height: 1.6; color: var(--ink); }

/* A write-up, rendered. */
.fullwriteup { margin-top: 1.2rem; border-top: 1px solid var(--home-line); padding-top: 0.6rem; }
.fullwriteup > summary { cursor: pointer; list-style: none; font-family: var(--font-serif); font-size: 1.12rem; font-weight: 600; padding: 0.3rem 0; }
.fullwriteup > summary::-webkit-details-marker { display: none; }
.fullwriteup > summary::after { content: '  ▾'; color: var(--faint); font-size: 0.8rem; }
.fullwriteup:not([open]) > summary::after { content: '  ▸'; }
.writeup { font-size: 0.95rem; line-height: 1.62; color: var(--ink-soft); }
.writeup p { margin: 0.55rem 0; }
.writeup code { font-size: 0.82em; padding: 0.05em 0.3em; border-radius: 4px; background: color-mix(in srgb, var(--ink) 6%, transparent); color: var(--code-ink); }
.writeup a { color: var(--accent); }
.writeup a.md-ext::after { content: '↗'; font-size: 0.75em; margin-left: 0.15em; opacity: 0.7; }
.md-plain { margin: 0.4rem 0 0.8rem; font-family: var(--font-serif); font-size: 1.1rem; line-height: 1.6; color: var(--ink); }
.md-section h3, .md-section h4 { margin: 1.1rem 0 0.3rem; font-family: var(--font-serif); font-size: 1.05rem; font-weight: 600; color: var(--ink); }
.md-section--formal { margin: 1rem 0; padding: 0.1rem 0 0.3rem 0.9rem; box-shadow: inset 2px 0 0 var(--weave-red); }
:root[data-theme="dark"] .md-section--formal { box-shadow: inset 2px 0 0 var(--weave-red-glow); }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .md-section--formal { box-shadow: inset 2px 0 0 var(--weave-red-glow); } }
.md-section--formal h3::before { content: ''; display: inline-block; width: 7px; height: 7px; border-radius: 50%; margin: 0 0.45rem 0.12rem 0; background: var(--weave-red); box-shadow: 0 0 0 2px color-mix(in srgb, var(--weave-azure-glow) 55%, transparent); }
.md-list { margin: 0.4rem 0; padding-left: 1.1rem; }
.md-list li { margin: 0.25rem 0; }
.md-run { margin: 0.5rem 0; font-size: var(--fs-meta); }
.md-run > summary { cursor: pointer; color: var(--muted); font-weight: 600; font-size: var(--fs-small); }
.md-run .cmd { white-space: pre-wrap; }
.md-nolink { color: var(--ink); }

/* Saved runs as dated marks. */
.runs { list-style: none; display: flex; flex-wrap: wrap; gap: 0.35rem; margin: 0.4rem 0 0; padding: 0; }
.run > a, .run > span:first-child, .run { text-decoration: none; }
.run { display: inline-flex; }
.run > a, .run:not(:has(> a)) { display: inline-flex; align-items: center; gap: 0.4rem; padding: 0.22rem 0.6rem 0.22rem 0.45rem; border-radius: var(--r-pill); box-shadow: inset 0 0 0 1px var(--home-line-strong); font-size: var(--fs-small); color: var(--ink-soft); }
.run > a:hover { box-shadow: inset 0 0 0 1px var(--m-ember); text-decoration: none; }
.run__dot { width: 8px; height: 8px; border-radius: 50%; background: var(--m-ember); flex: none; }
.run__date { font-variant-numeric: tabular-nums; color: var(--ink); }
.run__status { color: var(--muted); }
.run.is-absent .run__dot { background: none; box-shadow: inset 0 0 0 1px var(--muted); }
.run.is-blocked .run__dot { background: none; box-shadow: inset 0 0 0 2px var(--m-ember); }
.callers { list-style: none; margin: 0.3rem 0 0; padding: 0; font-size: 0.92rem; }
.callers li { padding: 0.25rem 0; }

/* A component page: plain words first, the write-up, its checks beside. */
.page-plain { margin: 0.7rem 0 0; max-width: 64ch; font-family: var(--font-serif); font-size: 1.22rem; line-height: 1.6; color: var(--ink); }
.reader--component { grid-template-columns: minmax(0, 7fr) minmax(0, 4fr); }
.reader--component .reader__steps > section { max-width: 70ch; }
.checks-aside { padding: 0.9rem 1rem; border-radius: var(--r-lg); background: var(--surface); box-shadow: 0 0 0 1px var(--home-line-strong); }
.checks-aside__title { margin: 0 0 0.3rem; font-family: var(--font-serif); font-size: 1.05rem; font-weight: 600; }
.checks-aside .column__row { grid-template-columns: 12px minmax(0, 1fr) auto; }
.kernel-callout { margin-top: 0.6rem; padding: 0.8rem 0.95rem; border-radius: var(--r-lg); box-shadow: inset 2px 0 0 var(--weave-red), 0 0 0 1px var(--home-line-strong); background: var(--surface); }
.kernel-callout__name { display: flex; align-items: center; gap: 0.5rem; margin: 0; font-family: var(--font-serif); font-size: 1.15rem; font-weight: 600; }
.kernel-callout .statement { box-shadow: none; padding: 0.4rem 0 0; background: none; }
.squares .sq--on { background: var(--ink-fill, var(--ink)); }
.squares.ink-unknown .sq--unknown, .sq--unknown { background: repeating-linear-gradient(45deg, transparent 0 3px, color-mix(in srgb, var(--muted) 45%, transparent) 3px 4px); box-shadow: inset 0 0 0 1px var(--home-line-strong); }
.measure__name { display: inline-flex; align-items: center; gap: 0.4rem; }
@media (max-width: 960px) { .reader--component { grid-template-columns: minmax(0, 1fr); } .reader--component .reader__figure { order: 0; } }

/* The key, opened as a window. */
.explain {
  width: min(820px, calc(100vw - 32px)); max-height: min(88vh, 960px); padding: 0; border: 0;
  border-radius: var(--r-lg); background: var(--surface); color: var(--ink);
  box-shadow: 0 0 0 1px var(--home-line-strong), 0 30px 80px -20px rgba(var(--ink-rgb), 0.6);
  overflow: hidden;
}
.explain[open] { display: flex; flex-direction: column; }
.explain::backdrop { background: rgba(10, 6, 16, 0.55); backdrop-filter: blur(2px); }
.explain__head { display: flex; align-items: center; justify-content: space-between; gap: 1rem; padding: 1rem 1.3rem 0.8rem; border-bottom: 1px solid var(--home-line); }
.explain__head h2 { margin: 0; font-family: var(--font-serif); font-weight: 500; font-size: 1.5rem; }
.explain__close { width: 36px; height: 36px; border-radius: 50%; border: 0; background: none; color: var(--ink-soft); font-size: 1.5rem; line-height: 1; cursor: pointer; box-shadow: 0 0 0 1px var(--home-line-strong); }
.explain__close:hover { color: var(--ink); box-shadow: 0 0 0 1px var(--home-ember); }
.explain__body { overflow-y: auto; padding: 0.4rem 1.3rem 1.6rem; font-size: 0.95rem; line-height: 1.55; }
.explain__body h3 { margin: 1.5rem 0 0.6rem; font-family: var(--font-serif); font-size: 1.15rem; font-weight: 600; }
.explain__lede { margin: 0.8rem 0 0; font-family: var(--font-serif); font-size: 1.08rem; color: var(--ink); max-width: 66ch; }
.explain__rings { list-style: none; margin: 0; padding: 0; display: grid; grid-template-columns: repeat(auto-fit, minmax(330px, 1fr)); gap: 0.8rem; }
.explain__ring { padding: 0.8rem 0.9rem 0.7rem; border-radius: var(--r-md); background: var(--page); box-shadow: 0 0 0 1px var(--home-line); scroll-margin-top: 12px; }
.explain__ring-head { display: grid; grid-template-columns: 26px minmax(0, 1fr); align-items: center; column-gap: 0.55rem; }
.explain__ring-head .swatch { width: 26px; height: 12px; border-radius: 3px; }
.explain__ring-head h4 { margin: 0; font-size: 1rem; font-weight: 650; }
.explain__by { grid-column: 2; font-size: var(--fs-small); color: var(--muted); }
.explain__ring > p { margin: 0.5rem 0 0.4rem; color: var(--ink-soft); }
.explain__ring dl { margin: 0; display: grid; grid-template-columns: auto minmax(0, 1fr); gap: 0.25rem 0.7rem; font-size: var(--fs-meta); }
.explain__ring dt { font-weight: 650; color: var(--ink); white-space: nowrap; }
.explain__ring dd { margin: 0; color: var(--ink-soft); }
.explain__marks { list-style: none; margin: 0; padding: 0; display: grid; gap: 0.55rem; }
.explain__marks li { display: grid; grid-template-columns: 18px minmax(0, 1fr); gap: 0.6rem; align-items: start; }
.explain__marks li > svg, .explain__marks li > .swatch { margin-top: 0.3rem; width: 14px; height: 14px; }
.ringkey__row { cursor: pointer; border-radius: 4px; }
.ringkey__row:hover { background: color-mix(in srgb, var(--ink) 7%, transparent); }
.ringkey__more { display: block; width: 100%; margin-top: 0.45rem; padding: 0.35rem 0; border: 0; border-top: 1px solid var(--home-line); background: none; color: var(--accent); font: inherit; font-size: 0.74rem; font-weight: 650; text-align: left; cursor: pointer; }
.ringkey__more:hover { text-decoration: underline; }
.section-head { display: flex; align-items: baseline; justify-content: space-between; gap: 1rem; }
.section-head .section-title { margin-bottom: 0.5rem; }

.column__none { padding: 0.5rem 0 0; font-size: var(--fs-meta); color: var(--muted); list-style: none; }

/* The doctrine: the halo's rules in the panel, in the map's own inks. */
.rule-mark { color: var(--m-doctrine); flex: none; }
.rule-mark--anti_principle { color: var(--m-threat); }
.ink-doctrine-text { color: var(--m-doctrine); }
.ink-threat-text { color: var(--m-threat); }
.doc-id--axiom, .doc-id--principle { color: var(--m-doctrine); }
.doc-id--anti_principle { color: var(--m-threat); }
.rule-row .ring-row__title { font-weight: 550; }
.rule-row .ring-row__title .doc-id { min-width: 2.9em; font-weight: 600; }
.strip--doctrine { --ink-fill: var(--m-doctrine); }
.strip--doctrine .cell--witness { stroke: var(--ink); stroke-width: 0.9px; vector-effect: non-scaling-stroke; }
.rule-statement { font-family: var(--font-serif); font-size: 1.02rem; line-height: 1.55; color: var(--ink-soft); }
.rule-statement p { margin: 0.5rem 0; }
.rule-statement table { font-family: var(--font-sans); font-size: 0.84rem; }
.obligations { list-style: none; margin: 0.4rem 0 0; padding: 0; }
.obligation { display: grid; grid-template-columns: 16px 1fr; gap: 0.6rem; padding: 0.45rem 0; border-bottom: 1px solid var(--home-line); font-size: 0.9rem; line-height: 1.45; }
.obligation__arc { width: 12px; height: 12px; margin-top: 0.25rem; border-radius: 50%; border: 2px solid transparent; border-top-color: var(--m-doctrine); border-right-color: var(--m-doctrine); transform: rotate(-20deg); }
.obligation--debt .obligation__arc { border-top-color: var(--m-threat); border-right-color: var(--m-threat); }
.obligation--blocked .obligation__arc, .obligation--unknown .obligation__arc { border-top: 2px dotted var(--muted); border-right: 2px dotted var(--muted); }
.obligation__predicate { display: block; font-family: var(--font-mono); font-size: 0.8rem; color: var(--ink); }
.obligation__status { display: block; font-size: var(--fs-meta); color: var(--muted); }
.ringkey__halo { margin-bottom: 0.45rem; padding-bottom: 0.4rem; border-bottom: 1px solid var(--home-line); }
.ringkey__glyph { width: 22px; display: inline-grid; place-items: center; }
.ringkey__glyph svg { width: 10px; height: 10px; }
.key--rules svg { color: var(--m-doctrine); }
.key--rules svg.rule-mark--anti_principle { color: var(--m-threat); }
.key--rules svg + svg { margin-left: -0.25rem; }

/* What the map is showing: one line per lit thing, its ink, then its limit. */
.readout { margin: 0.8rem 0 0.4rem; padding: 0.65rem 0.8rem 0.7rem; border: 1px solid var(--home-line-strong); border-radius: 8px; background: color-mix(in srgb, var(--ink) 3%, transparent); }
.readout__head { margin: 0 0 0.35rem; font-size: 0.72rem; font-weight: 650; letter-spacing: 0.04em; text-transform: uppercase; color: var(--muted); }
.readout__lines { list-style: none; margin: 0; padding: 0; display: grid; gap: 0.32rem; }
.readout__line { display: grid; grid-template-columns: 14px 1fr; gap: 0.5rem; font-size: 0.86rem; line-height: 1.42; color: var(--ink-soft); }
.readout__ink { width: 12px; height: 3px; margin-top: 0.55em; border-radius: 2px; background: var(--muted); }
.readout--red .readout__ink { background: var(--weave-red-glow); }
.readout--stated .readout__ink { background: var(--weave-azure-glow); }
.readout--doctrine .readout__ink { background: var(--m-doctrine); }
.readout--doctrine-soft .readout__ink { background: color-mix(in srgb, var(--m-doctrine) 45%, transparent); }
.readout--threat .readout__ink { background: repeating-linear-gradient(90deg, var(--m-threat) 0 3px, transparent 3px 5px); }
.readout--absent .readout__ink { background: repeating-linear-gradient(90deg, var(--muted) 0 2px, transparent 2px 4px); }
.readout--column .readout__ink { height: 9px; margin-top: 0.3em; width: 7px; margin-left: 2px; border: 1.4px solid var(--ink); background: none; }
.readout--obligations .readout__ink { height: 10px; width: 10px; margin-top: 0.25em; border-radius: 50%; background: none; border: 2px solid transparent; border-top-color: var(--m-doctrine); border-right-color: var(--m-doctrine); }
.readout--ink .readout__ink { background: var(--ink); }
.guide { margin: 0.6rem 0 0.4rem; }
.guide__rows { list-style: none; margin: 0.3rem 0 0.5rem; padding: 0; }
.guide__row { display: grid; grid-template-columns: 34px 5.6em 1fr; gap: 0.55rem; align-items: start; padding: 0.42rem 0; border-bottom: 1px solid var(--home-line); font-size: 0.88rem; line-height: 1.42; }
.guide__mark { display: inline-flex; align-items: center; justify-content: center; min-height: 1.3em; }
.guide__mark svg { width: 12px; height: 12px; }
.guide__mark .swatch { width: 18px; height: 8px; border-radius: 2px; }
.guide__rules { display: inline-flex; gap: 1px; }
.guide__rules svg { width: 10px; height: 10px; }
.guide__name { font-weight: 600; color: var(--ink); }
.guide__words { color: var(--ink-soft); }

/* With the panel open it already lists every ring in its colour, so the
   corner key steps aside and the drawing takes the stage's full height. */
.explorer__legend { font-size: 0.8rem; gap: 0.3rem 1rem; }
.readout__mark { font-weight: 650; color: var(--ink); }
.explorer__head--compact { padding: 14px var(--explorer-pad) 8px; }
.explorer__head--compact .find { margin-top: 0; }
.guide__title { margin-top: 0.2rem; }

/* A rule's card: its meaning first, in the serif of the write-ups. */
.rule-said { margin: 0.6rem 0 0.2rem; }
.rule-plain { margin: 0; font-family: var(--font-serif); font-size: 1.16rem; line-height: 1.5; color: var(--ink); }
.rule-analogy { margin: 0.9rem 0 0; padding: 0.7rem 0.85rem; border-radius: 8px; background: color-mix(in srgb, var(--m-doctrine) 8%, transparent); border-left: 2px solid var(--m-doctrine); }
.rule-analogy__label { display: block; font-size: 0.72rem; font-weight: 650; letter-spacing: 0.04em; text-transform: uppercase; color: var(--muted); margin-bottom: 0.25rem; }
.rule-analogy p { margin: 0; font-size: 0.95rem; line-height: 1.5; color: var(--ink-soft); }
.rule-why { margin: 0.8rem 0 0; font-size: 0.95rem; line-height: 1.5; color: var(--ink-soft); }
.rule-facts { list-style: none; margin: 0.3rem 0 0; padding: 0; }
.rule-facts li { display: grid; grid-template-columns: 16px 1fr; gap: 0.6rem; padding: 0.45rem 0; border-bottom: 1px solid var(--home-line); font-size: 0.92rem; line-height: 1.45; }
.rule-facts li svg { width: 12px; height: 12px; margin-top: 0.25rem; color: var(--m-doctrine); }
.rule-example p, .rule-counter { font-size: 0.95rem; line-height: 1.5; color: var(--ink-soft); }
.rule-counter { padding-left: 0.75rem; border-left: 2px dashed var(--m-threat); }
.rule-source { margin-top: 1rem; }
.rule-row__ties { font-size: 0.74rem; opacity: 0.85; }

/* Card heads, context, placement and stations (after the maths universe map). */
.card-head { display: flex; align-items: center; justify-content: space-between; gap: 0.8rem; margin: 0.2rem 0 0.35rem; }
.card-head .card-kind { margin: 0; }
.card-head__back { flex: none; border: 0; background: none; padding: 0.2rem 0; font: inherit; font-size: var(--fs-small); font-weight: 600; color: var(--accent); cursor: pointer; }
.card-head__back:hover { text-decoration: underline; }
.card-head__tag { flex: none; padding: 0.12rem 0.5rem; border-radius: var(--r-pill); font-size: 0.68rem; font-weight: 650; letter-spacing: 0.05em; text-transform: uppercase; color: var(--muted); box-shadow: 0 0 0 1px var(--home-line-strong); }
.card-context { margin: 0.1rem 0 0.15rem; font-size: var(--fs-small); color: var(--muted); }
.card-context__go { border: 0; background: none; padding: 0; font: inherit; color: var(--accent); cursor: pointer; text-align: left; }
.card-context__go:hover { text-decoration: underline; }
.card-placed { display: flex; gap: 0.5rem; align-items: baseline; margin: 0.55rem 0 0; font-size: var(--fs-meta); line-height: 1.45; color: var(--muted); }
.card-placed__mark { flex: none; width: 7px; height: 7px; border-radius: 50%; border: 1.4px solid currentColor; transform: translateY(1px); }
.stations { list-style: none; margin: 0.35rem 0 0; padding: 0; }
.station { display: grid; grid-template-columns: 22px minmax(0, 1fr); gap: 0.55rem; align-items: start; padding: 0.42rem 0; border-bottom: 1px solid var(--home-line); }
.station > .swatch { width: 20px; height: 9px; margin-top: 0.38rem; border-radius: 2px; }
.station > svg { width: 12px; height: 12px; margin: 0.28rem 0 0 4px; color: var(--m-doctrine); }
.station__text { margin: 0; font-size: 0.9rem; line-height: 1.45; color: var(--ink-soft); }
.station__text b { color: var(--ink); font-weight: 650; }
.station--empty .station__text, .station--unknown .station__text { color: var(--muted); }
.station--empty .station__text b, .station--unknown .station__text b { color: var(--muted); font-weight: 600; }
.card-hint { margin: 1.1rem 0 0; font-size: var(--fs-meta); color: var(--muted); }
.card-hint kbd { font: inherit; font-size: 0.72rem; padding: 0.05rem 0.35rem; border-radius: 4px; box-shadow: 0 0 0 1px var(--home-line-strong); }
.card-foot { margin-top: 1.1rem; } .card-foot .card-hint { margin-top: 0.4rem; }
.rule-table { display: grid; grid-template-columns: max-content 1fr; gap: 0.3rem 0.9rem; margin: 0.5rem 0; font-family: var(--font-sans); font-size: 0.86rem; } .rule-table dt { color: var(--muted); } .rule-table dd { margin: 0; color: var(--ink-soft); }

/* The purpose stays visible while the overview teaches the map. */
.explorer__title { margin: 0 0 12px; font-family: var(--font-serif); font-size: 1.48rem; line-height: 1.2; font-weight: 500; }
.introduction .card-plain { margin-top: 0; }
.introduction .rows { margin: 0.8rem 0; }

/* A selected component leads with its source summary and usable proof route. */
.component-summary { font-family: var(--font-sans); font-size: 0.98rem; line-height: 1.5; }
.component-proof > .section-title { margin-top: 1rem; }
.component-proof > .small { margin: 0.35rem 0 0.6rem; }
.component-proof .actions { margin-top: 0.4rem; }
.component-card .plain-explanation > p { line-height: 1.55; }
.component-card .proof-scope h4 { margin: 0.8rem 0 0.25rem; }


/* ==== Lane 4: the reading panel, preview dock, keys and wording ============ */
.doc-id { white-space: nowrap; }
.explorer__body { min-width: 0; overflow-x: hidden; }
.explorer__body > *, .rule-card, .component-card, .kernel-card, .fullwriteup, .variants, .variant, .excerpt, .tech { min-inline-size: 0; max-inline-size: 100%; }
.variants { grid-template-columns: minmax(0, 1fr); }
.diff { max-inline-size: 100%; overflow-x: auto; overscroll-behavior-x: contain; }
.diff__row { grid-template-columns: 4.4em 2.6em max-content; width: max-content; min-width: 100%; box-sizing: border-box; }
.dafny { max-inline-size: 100%; overflow-x: auto; }

/* The compact head: search, three views and the key; no permanent title. */
.explorer__head--compact { padding: 12px var(--explorer-pad) 6px; }
.explorer__head--compact .tabs { margin-top: 0.55rem; flex-wrap: nowrap; }
.explorer__head--compact .tabs__group { gap: 0.9rem; }
.explorer__head--compact .tabs__group + .tabs__group { gap: 0.4rem; }
.explorer__head--compact .util { min-height: 30px; padding: 0 0.65rem; }

/* Card typography (art direction §8). */
.card-title { font-family: var(--font-serif); font-size: 26px; line-height: 30px; font-weight: 500; letter-spacing: -0.005em; margin: 0.1rem 0 0; }
.card-kind { font-weight: 650; color: var(--ink); }
.card-kind__sub { font-weight: 450; color: var(--muted); }
.card-context { margin: 0.05rem 0 0.25rem; }
.rule-plain, .card-plain { font-family: var(--font-serif); font-size: 17px; line-height: 25px; color: var(--ink); margin: 0.65rem 0 0; }
.component-summary { font-family: var(--font-serif); font-size: 17px; line-height: 25px; }
.section-aside { font-size: var(--fs-small); color: var(--muted); }
.limit { border-left: 2px solid var(--rule-control); border-radius: 0 var(--r-md) var(--r-md) 0; background: color-mix(in srgb, var(--ink) 3.5%, transparent); }
.limit__label { color: var(--ink); }

/* The overview. */
.overview .explorer__title { margin: 0.25rem 0 0.4rem; font-family: var(--font-serif); font-size: 28px; line-height: 32px; font-weight: 500; }
.overview__lead { margin: 0 0 0.6rem; font-family: var(--font-serif); font-size: 17px; line-height: 25px; color: var(--ink); }
.guide__row { grid-template-columns: 34px 5.9em minmax(0, 1fr); }
.guide__mark .dial { width: 26px; height: 26px; }
.guide__rings { display: inline-grid; grid-template-columns: repeat(2, 12px); gap: 1px; }
.guide__rings .swatch { width: 12px; height: 4px; border-radius: 1px; }
.ring-key .ring-row__go { grid-template-columns: minmax(0, 1fr) auto; }
.ring-row__no { font-size: var(--fs-small); color: var(--muted); font-weight: 500; width: 1.4em; }
.ring-key .ring-row__title .swatch { width: 18px; height: 8px; border-radius: 2px; flex: none; }
.ring-key .ring-row__by { padding-left: calc(1.4em + 18px + 1.1rem); color: var(--ink-soft); }
.ring-key .strip { margin-left: calc(1.4em + 18px + 1.1rem); width: calc(100% - 1.4em - 18px - 1.1rem); height: 8px; }
.row__go--start { box-shadow: inset 2px 0 0 var(--home-ember); padding-left: 0.6rem !important; }

/* The ring key on the stage: always fully readable; a chip where there is no room. */
.explorer__rings { font-size: 0.76rem; }
.ringkey__no { color: var(--muted); font-size: 0.68rem; }
.ringkey__name { color: var(--ink); }
.ringkey__n { color: var(--ink-soft); text-align: right; padding-left: 0.5rem; }
.ringkey__chip { display: none; border: 0; background: none; font: inherit; font-weight: 650; color: var(--ink); cursor: pointer; padding: 0.1rem 0.25rem; }
.explorer__rings.is-compact { padding: 0.25rem 0.5rem; }
.explorer__rings.is-compact .ringkey__chip { display: inline-block; }
.explorer__rings.is-compact:not(.is-open) .ringkey__panel { display: none; }
.explorer__rings.is-compact.is-open .ringkey__panel { margin-top: 0.35rem; }
.explorer__rings.is-compact.is-open { padding: 0.35rem 0.65rem 0.45rem; }
.dial__face { fill: var(--page, transparent); stroke: none; }
.dial__ticks line { stroke: var(--weave-red); stroke-width: 0.8; }
.dial__band { fill: none; stroke: var(--weave-red); opacity: 0.32; }
.dial__ring { fill: none; stroke: var(--weave-red); stroke-width: 1.3; }
.dial__rules { fill: none; stroke: var(--weave-azure-glow); stroke-width: 1.2; }
.dial__code { fill: var(--weave-red); }
.dial__num { fill: var(--weave-red); font-family: var(--font-sans); font-weight: 700; }
.dial__many { fill: var(--ink); font-family: var(--font-sans); font-weight: 600; }
.dial__cross { stroke: var(--ink); stroke-width: 1.1; stroke-linecap: round; fill: none; }
:root[data-theme="dark"] .dial__ticks line, :root[data-theme="dark"] .dial__ring { stroke: #ff8a7a; }
:root[data-theme="dark"] .dial__code, :root[data-theme="dark"] .dial__num { fill: #ff8a7a; }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .dial__ticks line, :root:not([data-theme="light"]) .dial__ring, :root:not([data-theme="light"]) .dial__band { stroke: #ff8a7a; } :root:not([data-theme="light"]) .dial__code, :root:not([data-theme="light"]) .dial__num { fill: #ff8a7a; } }

/* A rule's map fact, ties and citers by family. */
.mapfact { margin: 0.9rem 0 0.2rem; padding: 0.65rem 0.8rem; border-radius: var(--r-md); background: color-mix(in srgb, var(--m-doctrine) 8%, transparent); border-left: 2px solid var(--m-doctrine); }
.mapfact__n { margin: 0; font-size: 0.98rem; line-height: 1.4; color: var(--ink); }
.mapfact__n strong { font-size: 1.15rem; font-weight: 700; color: var(--m-doctrine); }
.mapfact__limit { margin: 0.3rem 0 0; font-size: var(--fs-meta); line-height: 1.45; color: var(--ink-soft); }
.tie { display: grid; grid-template-columns: 6.6em minmax(0, 1fr); gap: 0.5rem; align-items: baseline; margin: 0.6rem 0 0; font-size: var(--fs-meta); }
.tie__label { color: var(--muted); font-weight: 600; }
.tie__chips { display: flex; flex-wrap: wrap; gap: 0.3rem; }
.idchip { font: inherit; font-size: 0.8rem; font-weight: 650; white-space: nowrap; padding: 0.12rem 0.5rem; border-radius: var(--r-sm); border: 1px solid currentColor; background: none; cursor: pointer; font-variant-numeric: tabular-nums; }
.idchip:hover, .idchip:focus-visible { background: color-mix(in srgb, currentColor 12%, transparent); }
.citers { list-style: none; margin: 0.35rem 0 0; padding: 0; border-top: 1px solid var(--home-line); }
.citers__fam { border-bottom: 1px solid var(--home-line); }
.citers__go { display: grid; grid-template-columns: minmax(0, 1fr) 3.6em; grid-template-areas: 'name n' 'bar bar'; gap: 0.2rem 0.6rem; width: 100%; padding: 0.45rem 0.15rem; border: 0; background: none; font: inherit; color: var(--ink); text-align: left; cursor: pointer; }
.citers__go:disabled { cursor: default; color: var(--muted); }
.citers__go:not(:disabled):hover .citers__name { color: var(--accent); }
.citers__go::before { content: none; }
.citers__name { grid-area: name; font-size: 0.92rem; }
.citers__go:not(:disabled) .citers__name::before { content: '▸ '; color: var(--faint); font-size: 0.75em; }
.citers__go[aria-expanded="true"] .citers__name::before { content: '▾ '; }
.citers__n { grid-area: n; text-align: right; font-size: 0.9rem; color: var(--ink-soft); }
.citers__bar { grid-area: bar; display: flex; gap: 1px; }
.citers__bar i { flex: 1; height: 5px; border-radius: 1px; background: color-mix(in srgb, var(--ink) 9%, transparent); }
.citers__bar i.on { background: var(--m-doctrine); }
.citers__list { margin: 0 0 0.4rem 0.9rem; }
.rows--dense .row__go { padding: 0.38rem 0.15rem; }
.row__title .doc-id { display: inline-block; min-width: 3.4em; font-weight: 650; }
.rule-row .ring-row__title .doc-id { display: inline-block; min-width: 3.4em; }
.row__code { font-size: 0.72rem; overflow-wrap: anywhere; }

/* A component's eight evidence rows, in the key's order. */
.evidence { list-style: none; margin: 0.3rem 0 0; padding: 0; border-top: 1px solid var(--home-line); }
.evidence__row { display: grid; grid-template-columns: 1.6em 20px minmax(0, 1fr) auto; grid-template-areas: 'no sw name state' '. . detail detail'; align-items: center; column-gap: 0.55rem; padding: 0.38rem 0.1rem; border-bottom: 1px solid var(--home-line); font-size: 0.9rem; }
.evidence__no { grid-area: no; font-size: var(--fs-small); color: var(--muted); }
.evidence__row > .swatch { grid-area: sw; width: 20px; height: 9px; border-radius: 2px; }
.evidence__name { grid-area: name; color: var(--ink); }
.evidence__state { grid-area: state; text-align: right; color: var(--ink); font-weight: 600; white-space: nowrap; }
.evidence__detail { grid-area: detail; font-size: var(--fs-small); color: var(--muted); line-height: 1.35; margin-top: 0.1rem; }
.evidence__row--empty .evidence__name, .evidence__row--empty .evidence__state { color: var(--muted); font-weight: 450; }
.evidence__row--unknown .evidence__state { font-style: italic; font-weight: 500; color: var(--ink-soft); }

/* A proof's counts, with its dial. */
.proofcount { display: grid; grid-template-columns: auto minmax(0, 1fr); gap: 0.75rem; align-items: center; margin: 0.8rem 0 0.2rem; }
.proofcount__text { margin: 0; font-size: 0.98rem; line-height: 1.4; color: var(--ink); }
.proofcount__text strong { font-weight: 700; }
.proofcount__note { display: block; font-size: var(--fs-small); color: var(--muted); margin-top: 0.15rem; }
.promise { margin: 0.8rem 0 0; padding: 0.7rem 0.85rem; border-radius: var(--r-md); background: var(--surface); box-shadow: 0 0 0 1px var(--home-line-strong); }
.promise__label { display: block; font-size: var(--fs-small); font-weight: 650; color: var(--weave-red); margin-bottom: 0.2rem; }
.promise__text { margin: 0; font-family: var(--font-serif); font-size: 16px; line-height: 23px; color: var(--ink); }
.chain .station > svg { color: var(--ink); }
.tech h4 { margin: 1rem 0 0.35rem; font-size: 0.95rem; font-weight: 650; }
.map-details .readout { margin-top: 0.5rem; }

/* The preview dock, at the foot of the panel: never over the drawing. */
.dock {
  position: absolute; z-index: 4; left: 0; right: 0; bottom: 0; max-height: 42%; overflow-y: auto; overscroll-behavior: contain;
  padding: 0.75rem var(--explorer-pad) 0.7rem; background: var(--surface);
  border-top: 1px solid var(--home-line-strong); box-shadow: 0 -14px 30px -18px rgba(var(--ink-rgb), 0.35);
  transform: translateY(100%); visibility: hidden; opacity: 0.6;
  transition: transform 140ms var(--ease-out), opacity 140ms var(--ease-out), visibility 0s linear 140ms;
}
.dock.is-on { transform: none; visibility: visible; opacity: 1; transition: transform 140ms var(--ease-out), opacity 140ms var(--ease-out), visibility 0s; }
.dock__kind { display: flex; align-items: center; gap: 0.45rem; margin: 0; font-size: var(--fs-small); font-weight: 650; letter-spacing: 0.02em; color: var(--muted); }
.dock__kind svg { width: 11px; height: 11px; flex: none; }
.dock__name { margin: 0.15rem 0 0; font-family: var(--font-serif); font-size: 20px; line-height: 24px; color: var(--ink); }
.dock__relation { margin: 0.45rem 0 0; padding-left: 0.6rem; border-left: 2px solid var(--m-doctrine); font-size: 0.95rem; font-weight: 700; line-height: 1.4; color: var(--ink); }
.dock__purpose { display: -webkit-box; -webkit-box-orient: vertical; -webkit-line-clamp: 2; overflow: hidden; margin: 0.45rem 0 0; font-family: var(--font-serif); font-size: 15px; line-height: 21px; color: var(--ink-soft); }
.dock__rings { display: flex; gap: 3px; margin: 0.45rem 0 0; }
.dock__ring .swatch { width: 16px; height: 7px; border-radius: 2px; display: block; }
.dock__counts { list-style: none; margin: 0.4rem 0 0; padding: 0; font-size: var(--fs-meta); color: var(--ink); line-height: 1.45; }
.dock__hint { margin: 0.4rem 0 0; font-size: var(--fs-small); color: var(--faint); }
.dock__hint kbd { font: inherit; padding: 0 0.3rem; border-radius: 4px; box-shadow: 0 0 0 1px var(--home-line-strong); }
@media (prefers-reduced-motion: reduce) { .dock, .dock.is-on { transition: none; } }

/* The phone sheet: a choice keeps the map; the card rises over its foot. */
.sheetbar { display: none; }
@media (max-width: 899px) {
  .explorer__rings { top: 10px; left: 10px; }
  .dock { display: none; }
  .explorer[data-explorer-sheet] .explorer__panel {
    display: flex; position: absolute; z-index: 8; left: 0; right: 0; bottom: 0; height: 200px;
    border-top: 1px solid var(--home-line-strong); border-radius: 14px 14px 0 0; overflow: hidden;
    box-shadow: 0 -18px 40px -20px rgba(var(--ink-rgb), 0.5); background: var(--page);
    transition: height 180ms var(--ease-out);
  }
  .explorer[data-explorer-sheet="full"] .explorer__panel { height: 72%; }
  .explorer[data-explorer-sheet] .explorer__head, .explorer[data-explorer-sheet] .explorer__foot { display: none; }
  .explorer[data-explorer-sheet] .sheetbar { display: flex; justify-content: space-between; gap: 0.5rem; padding: 8px 14px 4px; flex: none; }
  .explorer[data-explorer-sheet] .sheetbar .explorer-tool { min-height: 32px; }
  .explorer[data-explorer-sheet] .explorer__body { padding: 4px 16px 24px; }
  .explorer[data-explorer-sheet] .explorer__legend { display: none; }
  .explorer[data-explorer-sheet="peek"] .explorer__body { overflow: hidden; }
}

.card-kind__rule { font-weight: 650; white-space: nowrap; }
.section-head { align-items: baseline; }
.section-head .section-title { flex: none; }
.section-head > .section-aside, .section-head > .textbtn { flex: none; white-space: nowrap; }

/* The pointer arm's swatch in the key window: a fine rule with an index
   notch, as the map draws it. */
.explain__arm { display: inline-block; flex: none; width: 22px; height: 12px; margin-top: 4px; background: linear-gradient(var(--muted), var(--muted)) center / 100% 1px no-repeat, linear-gradient(var(--muted), var(--muted)) right center / 1.5px 9px no-repeat; }

/* A failure mode's reach is exposure, derived through its axioms: the card's
   fact and its family strips take the threat ink, never the citation ink. */
.mapfact--threat { background: color-mix(in srgb, var(--m-threat) 9%, transparent); border-left-color: var(--m-threat); }
.citers--threat .citers__bar i.on { background: var(--m-threat); }
.row__via { margin-left: auto; padding-left: 0.6rem; font-size: 0.78rem; color: var(--m-threat); white-space: nowrap; }

/* The ring key in plain words: one short sentence per ring, on one line
   (the wedge on the map carries each ring's name). */
.ringkey__title { display: flex; flex-wrap: wrap; align-items: baseline; gap: 0 0.45rem; font-size: 0.78rem; color: var(--ink); }
.ringkey__sub { font-weight: 400; color: var(--muted); }
.ringkey__name { white-space: nowrap; }