/* style.css — the whole site's styling.  No framework, no build step. */

/* ------------------------------------------------------------------ tokens */

:root {
  color-scheme: light dark;

  --bg: #fbfbfa;
  --panel: #ffffff;
  --panel-2: #f3f4f6;
  --fg: #1b1d1e;
  --muted: #5f676e;
  --faint: #8b939b;
  --border: #dcdfe3;
  --border-strong: #c2c7ce;
  --accent: #2f6fd0;
  --accent-soft: #e6eefb;
  --accent-fg: #ffffff;
  --shadow: 0 1px 2px rgba(16, 20, 26, .07), 0 4px 14px rgba(16, 20, 26, .06);

  --st-absent: #97a0a8;
  --st-missing: #d34b4b;
  --st-stated: #cc8f1c;
  --st-proved: #2c9a62;
  --st-proved_with_axioms: #1f9b9b;
  --st-none: #b6bcc2;

  --lv-error: #d34b4b;
  --lv-warning: #cc8f1c;
  --lv-info: #4d7fc4;

  --graph-node: #ffffff;
  --graph-compound: #f1f3f6;
  --graph-edge: #7b848d;
  --graph-junction: #55606a;
  --graph-hl: #f0a202;

  --mono: ui-monospace, SFMono-Regular, "SF Mono", Menlo, Consolas,
          "Liberation Mono", monospace;
  --sans: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, "Helvetica Neue",
          Arial, "Noto Sans", sans-serif;

  --radius: 7px;
  --topbar-h: 52px;
}

@media (prefers-color-scheme: dark) {
  :root {
    --bg: #131619;
    --panel: #1b1f23;
    --panel-2: #22272c;
    --fg: #e4e7ea;
    --muted: #9aa3ac;
    --faint: #767f88;
    --border: #2b3137;
    --border-strong: #3c444c;
    --accent: #6ea8ff;
    --accent-soft: #1d2a3d;
    --accent-fg: #0d1117;
    --shadow: 0 1px 2px rgba(0, 0, 0, .4), 0 6px 18px rgba(0, 0, 0, .35);

    --st-absent: #7d868e;
    --st-missing: #e06a6a;
    --st-stated: #dda93a;
    --st-proved: #4cba82;
    --st-proved_with_axioms: #3fbdbd;
    --st-none: #4d555c;

    --lv-error: #e06a6a;
    --lv-warning: #dda93a;
    --lv-info: #7ba7e8;

    --graph-node: #1f242a;
    --graph-compound: #191d21;
    --graph-edge: #8c959e;
    --graph-junction: #aab3bb;
    --graph-hl: #f0a202;
  }
}

/* ------------------------------------------------------------------- base */

* { box-sizing: border-box; }

html, body { height: 100%; }

body {
  margin: 0;
  background: var(--bg);
  color: var(--fg);
  font: 15px/1.55 var(--sans);
  -webkit-text-size-adjust: 100%;
}

a { color: var(--accent); text-decoration: none; }
a:hover { text-decoration: underline; }

code, kbd, pre, .mono { font-family: var(--mono); font-size: .92em; }

pre {
  background: var(--panel-2);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  padding: .7em .9em;
  overflow-x: auto;
}

code:not(pre code) {
  background: var(--panel-2);
  border: 1px solid var(--border);
  border-radius: 4px;
  padding: .08em .35em;
}

h1, h2, h3, h4 { line-height: 1.25; margin: 1.4em 0 .5em; font-weight: 620; }
h1 { font-size: 1.6rem; margin-top: 0; }
h2 { font-size: 1.25rem; }
h3 { font-size: 1.05rem; }
h4 { font-size: .95rem; }

hr { border: 0; border-top: 1px solid var(--border); margin: 1.5em 0; }

button, select, input[type="text"], input[type="search"] {
  font: inherit;
  color: inherit;
  background: var(--panel);
  border: 1px solid var(--border-strong);
  border-radius: var(--radius);
  padding: .3em .6em;
}
button { cursor: pointer; }
button:hover { background: var(--panel-2); }
button.active { background: var(--accent-soft); border-color: var(--accent); }
button:disabled { opacity: .5; cursor: default; }

input[type="range"] { accent-color: var(--accent); }

label.chk {
  display: inline-flex;
  align-items: center;
  gap: .32em;
  padding: .12em .45em .12em .3em;
  border: 1px solid var(--border);
  border-radius: 999px;
  background: var(--panel);
  cursor: pointer;
  font-size: .85rem;
  white-space: nowrap;
}
label.chk input { margin: 0; }

/* ----------------------------------------------------------------- topbar */

.topbar {
  position: sticky;
  top: 0;
  z-index: 30;
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 1rem;
  height: var(--topbar-h);
  padding: 0 1rem;
  background: var(--panel);
  border-bottom: 1px solid var(--border);
}

.topbar-main { display: flex; align-items: center; gap: 1.2rem; min-width: 0; }

.brand {
  display: flex;
  align-items: center;
  gap: .5rem;
  color: var(--fg);
  font-weight: 640;
  white-space: nowrap;
  overflow: hidden;
  text-overflow: ellipsis;
}
.brand:hover { text-decoration: none; }
.brand-mark {
  width: 15px; height: 15px;
  border: 2px solid var(--accent);
  border-radius: 3px;
  position: relative;
  flex: none;
}
.brand-mark::after {
  content: "";
  position: absolute;
  inset: 3px 3px auto auto;
  width: 5px; height: 5px;
  background: var(--accent);
  border-radius: 1px;
}

.tabs { display: flex; gap: .15rem; }
.tabs a {
  color: var(--muted);
  padding: .3em .7em;
  border-radius: var(--radius);
  font-size: .92rem;
}
.tabs a:hover { background: var(--panel-2); text-decoration: none; }
.tabs a.active { color: var(--fg); background: var(--accent-soft); font-weight: 560; }

/* The experimental style menu (app.js, THEMES). */
.topbar-aside .theme-select { font-size: .8rem; padding: .15em .3em; max-width: 7.5rem; }
.topbar-aside { display: flex; align-items: center; gap: .5rem; font-size: .85rem; color: var(--muted); }

/* The search box sits between the tabs and the progress figure, and its list
   hangs below the top bar, over the page, right-aligned with the box so it
   never runs off the right edge. */
.gsearch {
  position: relative;
  flex: 0 1 18rem;
  min-width: 9rem;
  margin-left: auto;
}
.gsearch input[type="search"] { width: 100%; padding-right: 1.8em; font-size: .88rem; }
.gsearch-key {
  position: absolute;
  right: .45em;
  top: 50%;
  transform: translateY(-50%);
  font-size: .72rem;
  line-height: 1.3;
  padding: 0 .35em;
  color: var(--faint);
  border: 1px solid var(--border-strong);
  border-radius: 4px;
  pointer-events: none;
}
.gsearch input:focus ~ .gsearch-key,
.gsearch input:not(:placeholder-shown) ~ .gsearch-key { display: none; }
.gsearch-panel {
  position: absolute;
  top: calc(100% + 6px);
  right: 0;
  width: min(34rem, calc(100vw - 2rem));
  max-height: min(70vh, 34rem);
  overflow-y: auto;
  background: var(--panel);
  border: 1px solid var(--border-strong);
  border-radius: var(--radius);
  box-shadow: var(--shadow);
  z-index: 40;
}
.gsearch-panel[hidden] { display: none; }
.gsearch-item {
  display: block;
  padding: .45em .75em;
  color: var(--fg);
  border-bottom: 1px solid var(--border);
}
.gsearch-item:hover { text-decoration: none; }
.gsearch-item.active { background: var(--accent-soft); }
.gsearch-title { display: block; font-weight: 560; overflow-wrap: anywhere; }
.gsearch-meta { display: flex; flex-wrap: wrap; align-items: center; gap: .4em; margin-top: .15em; }
.gsearch-id, .gsearch-lean {
  font-family: var(--mono);
  font-size: .76rem;
  color: var(--muted);
  overflow-wrap: anywhere;
}
.gsearch-lean::before { content: "Lean: "; font-family: var(--sans); }
.gsearch-foot { padding: .4em .75em; font-size: .8rem; color: var(--muted); }

/* ----------------------------------------------------------------- banner */

.banner {
  padding: .5em 1rem;
  background: var(--accent-soft);
  border-bottom: 1px solid var(--border);
  font-size: .88rem;
  display: flex;
  align-items: center;
  gap: .75rem;
  flex-wrap: wrap;
}
.banner.warn { background: color-mix(in srgb, var(--lv-warning) 18%, var(--panel)); }
/* `display: flex` above beats the user agent's `[hidden] { display: none }`,
   so without this the *empty* banner still laid out its padding and border: a
   15px strip under the top bar on every page, and 15px of the graph page —
   whose height is measured from the viewport — pushed off the bottom, which
   clipped the legend and the status line. */
.banner[hidden] { display: none; }

/* -------------------------------------------------------------- app frame */

/* The shell is a column — top bar, the banner when there is one, then the
   page filling exactly what is left.  Pages that measure themselves from the
   viewport instead (the graph did: `calc(100vh - var(--topbar-h))`) cannot
   know whether the banner is there, and while a historical snapshot was on
   screen the graph ran 47px off the bottom, taking the status line and the
   legend with it.
   The top bar and the banner keep their own height: a flex item shrinks by
   default, and on any page taller than the window the column squeezed the
   52px top bar to the 33px of its tallest child, so the tabs sat cramped on
   every page but the graph, the one page that fits the window exactly. */
body { display: flex; flex-direction: column; }
.topbar, .banner { flex: none; }
.app { flex: 1 1 auto; min-height: 0; }

.page {
  max-width: 62rem;
  margin: 0 auto;
  padding: 1.6rem 1.25rem 5rem;
}
.page.wide { max-width: 78rem; }

.loading, .empty {
  padding: 3rem 1.25rem;
  color: var(--muted);
  text-align: center;
}

.error-box {
  max-width: 40rem;
  margin: 3rem auto;
  padding: 1.5rem;
  background: var(--panel);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  box-shadow: var(--shadow);
}
.error-box h1 { font-size: 1.2rem; }
.error-box .detail {
  font-family: var(--mono);
  font-size: .82rem;
  color: var(--muted);
  word-break: break-all;
  margin: .6em 0 1.2em;
}

/* ----------------------------------------------------------------- badges */

.badge {
  display: inline-flex;
  align-items: center;
  gap: .35em;
  font-size: .76rem;
  font-weight: 560;
  line-height: 1.5;
  padding: .1em .5em;
  border-radius: 999px;
  border: 1px solid transparent;
  white-space: nowrap;
}
.badge .dot { width: .5em; height: .5em; border-radius: 50%; background: currentColor; flex: none; }

.badge.status-absent { color: var(--st-absent); border-color: var(--st-absent); }
.badge.status-missing { color: var(--st-missing); border-color: var(--st-missing); }
.badge.status-stated { color: var(--st-stated); border-color: var(--st-stated); }
.badge.status-proved { color: var(--st-proved); border-color: var(--st-proved); }
.badge.status-proved_with_axioms { color: var(--st-proved_with_axioms); border-color: var(--st-proved_with_axioms); }
.badge.status-none { color: var(--faint); border-color: var(--border-strong); }

.badge.kind {
  color: var(--muted);
  border-color: var(--border-strong);
  background: var(--panel-2);
  font-family: var(--mono);
  font-weight: 500;
}
.badge.level-error { color: var(--lv-error); border-color: var(--lv-error); }
.badge.level-warning { color: var(--lv-warning); border-color: var(--lv-warning); }
.badge.level-info { color: var(--lv-info); border-color: var(--lv-info); }

.chip {
  display: inline-block;
  font-size: .74rem;
  padding: .05em .45em;
  border-radius: 4px;
  background: var(--panel-2);
  border: 1px solid var(--border);
  color: var(--muted);
}

/* --------------------------------------------------------- progress bars */

.bar {
  position: relative;
  height: 8px;
  min-width: 60px;
  border-radius: 999px;
  background: var(--panel-2);
  border: 1px solid var(--border);
  overflow: hidden;
}
.bar > span {
  display: block;
  height: 100%;
  background: var(--st-proved);
  transition: width .25s ease;
}
.bar.mix { display: flex; }
.bar.mix > span { flex: none; }
.bar-row { display: flex; align-items: center; gap: .6rem; }
.bar-row .bar { flex: 1; }
.bar-row .num { font-family: var(--mono); font-size: .8rem; color: var(--muted); white-space: nowrap; }

/* ----------------------------------------------------------------- tables */

table.grid {
  width: 100%;
  border-collapse: collapse;
  font-size: .9rem;
}
table.grid th, table.grid td {
  text-align: left;
  padding: .45em .6em;
  border-bottom: 1px solid var(--border);
  vertical-align: middle;
}
table.grid th {
  font-weight: 580;
  color: var(--muted);
  font-size: .8rem;
  text-transform: uppercase;
  letter-spacing: .03em;
}
table.grid tr:last-child td { border-bottom: 0; }
.table-wrap { overflow-x: auto; border: 1px solid var(--border); border-radius: var(--radius); background: var(--panel); }

/* ------------------------------------------------------------ graph page */

.graph-page {
  display: grid;
  grid-template-columns: 1fr 22rem;
  grid-template-rows: auto 1fr;
  height: 100%;
  overflow: hidden;
}

.toolbar {
  grid-column: 1 / -1;
  display: flex;
  align-items: center;
  gap: .5rem .75rem;
  flex-wrap: wrap;
  padding: .5rem .9rem;
  background: var(--panel);
  border-bottom: 1px solid var(--border);
}
.toolbar .group { display: flex; align-items: center; gap: .35rem; flex-wrap: wrap; }
.toolbar .group > .lbl { font-size: .78rem; color: var(--muted); text-transform: uppercase; letter-spacing: .03em; }
.toolbar .sep { width: 1px; align-self: stretch; background: var(--border); }
.toolbar .spacer { flex: 1; }
.toolbar input[type="search"] { width: 12rem; }

.graph-stage {
  position: relative;
  overflow: hidden;
  background:
    radial-gradient(circle at 1px 1px, var(--border) 1px, transparent 0) 0 0 / 22px 22px;
  cursor: grab;
}
.graph-stage.panning { cursor: grabbing; }
/* The child combinator matters: the stage also contains the legend, whose
   sample lines and arrowheads are tiny `svg` elements of their own.  As a
   descendant selector this rule blew each of them up to the width of the
   legend and ~90px tall, which made the legend 455px high at 1400x900 — it
   covered nodes and ran off the bottom of the stage. */
.graph-stage > svg { display: block; width: 100%; height: 100%; touch-action: none; }

.graph-status {
  position: absolute;
  left: .75rem;
  bottom: .6rem;
  font-size: .78rem;
  color: var(--muted);
  background: color-mix(in srgb, var(--bg) 82%, transparent);
  padding: .2em .5em;
  border-radius: 4px;
  pointer-events: none;
}

/* Layout gave up: said in the pane itself, not only in the status line. */
.graph-error {
  position: absolute;
  left: .75rem;
  right: .75rem;
  top: .6rem;
  font-size: .8rem;
  color: var(--lv-error);
  background: color-mix(in srgb, var(--bg) 92%, transparent);
  border: 1px solid var(--lv-error);
  border-radius: 4px;
  padding: .35em .6em;
  pointer-events: none;
}

/* While ELK is thinking — in a worker, so panning and zooming still work, but
   the drawing on screen is the previous view until it answers. */
.graph-stage.laying-out .glayer { opacity: .55; }
.graph-stage.laying-out .graph-status {
  color: var(--fg);
  border: 1px solid var(--border);
}
.graph-stage.laying-out .graph-status::after {
  content: "";
  display: inline-block;
  width: .55em;
  height: .55em;
  margin-left: .45em;
  vertical-align: baseline;
  border-radius: 50%;
  background: currentColor;
  animation: bp-pulse 1s ease-in-out infinite;
}
@keyframes bp-pulse {
  0%, 100% { opacity: .25; }
  50% { opacity: 1; }
}
@media (prefers-reduced-motion: reduce) {
  .graph-stage.laying-out .graph-status::after { animation: none; opacity: .7; }
}

.legend {
  position: absolute;
  right: .75rem;
  bottom: .6rem;
  font-size: .74rem;
  color: var(--muted);
  background: color-mix(in srgb, var(--panel) 92%, transparent);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  padding: .4em .6em;
  display: grid;
  gap: .18em;
  pointer-events: none;
  max-width: 15rem;
}
.legend b { color: var(--fg); font-weight: 560; }
.legend .row { display: flex; align-items: center; gap: .4em; }
.legend .sw { width: 1.1em; height: .62em; border-radius: 2px; border: 1.5px solid currentColor; flex: none; }

/* graph svg internals */
.gnode .shape {
  fill: var(--graph-node);
  stroke: var(--border-strong);
  stroke-width: 1.5;
  transition: stroke .15s, stroke-width .15s;
}
.gnode.compound > .shape { fill: var(--graph-compound); stroke-dasharray: none; }
.gnode .label { fill: var(--fg); font-size: 12px; font-weight: 550; pointer-events: none; }
.gnode .sub { fill: var(--muted); font-size: 10px; pointer-events: none; }
.gnode { cursor: pointer; }
.gnode:hover .shape { stroke-width: 2.2; }
.gnode.selected .shape { stroke: var(--accent); stroke-width: 2.6; }
.gnode.match .shape { stroke: var(--graph-hl); stroke-width: 2.6; }
.gnode.dim { opacity: .22; }

.gnode .statusbar { stroke: none; }
.gnode .junction-dot { fill: var(--graph-junction); stroke: var(--panel); stroke-width: 1.5; }

.gedge path {
  fill: none;
  stroke: var(--graph-edge);
  stroke-width: 1.6;
}
.gedge.state-derived-only path { stroke-dasharray: 5 4; }
.gedge.kind-refines path { stroke-dasharray: 2 3; }
.gedge.dim { opacity: .18; }
.gedge .elabel { fill: var(--muted); font-size: 9.5px; pointer-events: none; }
.gedge.hover path, .gedge.selected path { stroke: var(--accent); stroke-width: 2.6; }

.glayer { transition: transform .28s cubic-bezier(.3, .7, .3, 1); }
.glayer.no-anim { transition: none; }

/* side panel */
.side {
  border-left: 1px solid var(--border);
  background: var(--panel);
  overflow-y: auto;
  padding: 1rem;
  font-size: .9rem;
}
.side h2 { margin-top: 0; font-size: 1.05rem; }
.side .meta { display: flex; gap: .4rem; flex-wrap: wrap; margin-bottom: .7rem; }
.side .excerpt { color: var(--fg); font-size: .88rem; max-height: 16rem; overflow: auto; }
.side section { margin-top: 1.1rem; }
.side section > h3 {
  margin: 0 0 .35rem;
  font-size: .76rem;
  text-transform: uppercase;
  letter-spacing: .04em;
  color: var(--muted);
  font-weight: 600;
}
/* A long listing behind a disclosure: the summary reads as the other sections'
   headings, with the browser's own marker in front saying it opens. */
.side section.fold > details > summary {
  cursor: pointer;
  font-size: .76rem;
  text-transform: uppercase;
  letter-spacing: .04em;
  color: var(--muted);
  font-weight: 600;
}
.side section.fold > details > summary:hover { color: var(--fg); }
.side section.fold > details[open] > summary { margin-bottom: .35rem; }
.side ul { margin: 0; padding-left: 1.05rem; }
.side li { margin: .12em 0; }
.side .hint { color: var(--faint); font-size: .84rem; }

/* ---------------------------------------------------------- object page */

.obj-head { display: flex; gap: .6rem; align-items: flex-start; flex-wrap: wrap; }
.obj-head h1 { flex: 1 1 18rem; }
.obj-id {
  font-family: var(--mono);
  font-size: .82rem;
  color: var(--muted);
  word-break: break-all;
}

.panel {
  background: var(--panel);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  padding: .9rem 1.1rem;
  margin: 1rem 0;
}
.panel > h2:first-child, .panel > h3:first-child { margin-top: 0; }

/* A panel behind a disclosure (the object page's long listings): its heading
   is the summary, with the browser's own marker in front saying it opens, and
   a shut panel is that one line. */
details.panel > summary { cursor: pointer; }
details.panel > summary > h3 { display: inline; margin: 0; }
details.panel > summary:hover > h3 { color: var(--accent); }
details.panel[open] > summary { margin-bottom: .6rem; }

dl.kv { display: grid; grid-template-columns: max-content 1fr; gap: .25em .9em; margin: 0; }
dl.kv dt { color: var(--muted); font-size: .85rem; }
dl.kv dd { margin: 0; min-width: 0; overflow-wrap: anywhere; }

.body-prose { overflow-wrap: break-word; }
.body-prose p:first-child { margin-top: 0; }
.body-prose img { max-width: 100%; }
.body-prose blockquote {
  margin: 1em 0;
  padding: .1em 1em;
  border-left: 3px solid var(--border-strong);
  color: var(--muted);
}
.body-prose .katex-display { overflow-x: auto; overflow-y: hidden; padding: .2em 0; }

a.objlink { font-weight: 500; }
a.objlink.broken { color: var(--lv-missing, var(--st-missing)); text-decoration: line-through dotted; cursor: help; }

.lean-decl { margin: .7rem 0; }
.lean-decl pre { margin: .25em 0; white-space: pre-wrap; }
/* The axiom and dependency lists are runs of `code` chips with nothing but a
   margin between them, and a margin is not a break opportunity: on a theorem
   with forty Lean dependencies the row became one unbreakable 14,000px line
   and the whole site grew a horizontal scrollbar.  A wrapping flex row gives
   the browser somewhere to break and keeps the spacing. */
.lean-decl .where {
  font-size: .82rem;
  color: var(--muted);
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: .15em .45em;
  min-width: 0;
}
.lean-decl .where code { overflow-wrap: anywhere; }
.lean-decl .doc { font-size: .88rem; color: var(--muted); margin-top: .3em; }

ul.objlist { list-style: none; margin: 0; padding: 0; }
ul.objlist li { padding: .2em 0; display: flex; gap: .45rem; align-items: baseline; flex-wrap: wrap; }
ul.objlist .role {
  font-family: var(--mono);
  font-size: .76rem;
  color: var(--muted);
  min-width: 3.2em;
}

.chain { font-size: .88rem; }
.chain .sep { color: var(--faint); margin: 0 .35em; }

/* -------------------------------------------------------- document page */

.doc-entry { margin: 0 0 1.6rem; scroll-margin-top: calc(var(--topbar-h) + 1rem); }
.doc-entry .head { display: flex; align-items: baseline; gap: .55rem; flex-wrap: wrap; }
.doc-entry .head h2, .doc-entry .head h3, .doc-entry .head h4, .doc-entry .head h5 { margin: 0; }
.doc-entry .head .num { color: var(--faint); font-family: var(--mono); font-size: .85em; }
.doc-entry.depth-0 { border-top: 2px solid var(--border-strong); padding-top: 1.2rem; margin-top: 2.2rem; }
.doc-entry.depth-0:first-child { border-top: 0; margin-top: 0; padding-top: 0; }
.doc-entry .prose { margin-top: .5rem; }
.doc-entry.dup { opacity: .75; }

/* A proof follows its statement as in a paper: "Proof." run in, its prose,
   and an end mark at the right (`proofDisclosure` in app.js, which also
   makes it fold; see "Proofs fold" below). */
.proof { margin: .6rem 0 1rem; }
a.proof-word { font-style: italic; font-weight: 400; color: inherit; }
.proof-prose > p:first-child { margin-top: 0; }
.proof-body > :last-child { margin-bottom: .3em; }
.proof-end { text-align: right; line-height: 1; color: var(--muted); }

.step {
  margin: .8rem 0 .8rem 1.2rem;
  padding: .55rem .9rem;
  border-left: 3px solid var(--accent);
  background: var(--panel);
  border-radius: 0 var(--radius) var(--radius) 0;
}
.step .step-head {
  font-size: .8rem;
  text-transform: uppercase;
  letter-spacing: .04em;
  color: var(--muted);
  font-weight: 600;
  display: flex;
  gap: .45rem;
  align-items: baseline;
  flex-wrap: wrap;
}

.toc {
  position: sticky;
  top: calc(var(--topbar-h) + .8rem);
  font-size: .86rem;
  max-height: calc(100vh - var(--topbar-h) - 3rem);
  overflow-y: auto;
}
.toc ul { list-style: none; margin: 0; padding: 0; }
.toc li { margin: .15em 0; }
.toc li.lvl-1 { padding-left: .9rem; }
.toc li.lvl-2 { padding-left: 1.8rem; }
/* The outline sidebar (`data-sidebar="outline"` on the page): every top-level
   entry, the ones on the way to this page opened, this page marked. */
.toc-outline ul { list-style: none; margin: 0; padding: 0; }
.toc-outline li > a { display: block; padding: .25em .5em; color: var(--fg); border-radius: var(--radius); }
.toc-outline li > a:hover { background: var(--panel-2); text-decoration: none; }
.toc-outline li > a .num { color: var(--muted); font-variant-numeric: tabular-nums; }
.toc-outline li > ul { margin: .1em 0 .3em .9em; padding-left: .5em; border-left: 1px solid var(--border); }
.toc-outline li.on-path > a { font-weight: 600; }
.toc-outline li.current > a { background: var(--accent-soft); color: var(--fg); }
.doc-layout { display: grid; grid-template-columns: 15rem 1fr; gap: 2rem; align-items: start; }

/* The split document: where a page sits, and its neighbours. */
.doc-crumbs { font-size: .86rem; color: var(--muted); margin: 0 0 .6rem; }
.doc-crumbs .sep { color: var(--faint); margin: 0 .4em; }
.doc-crumbs .here { color: var(--fg); }
.doc-pager {
  display: grid; grid-template-columns: 1fr auto 1fr; gap: 1rem; align-items: baseline;
  font-size: .88rem; margin: .8rem 0 1.4rem; padding: .5rem 0;
  border-top: 1px solid var(--border); border-bottom: 1px solid var(--border);
}
.doc-pager .up { text-align: center; }
.doc-pager .next { text-align: right; }
.doc-pager .num { color: var(--faint); font-family: var(--mono); font-size: .85em; }
.doc-entry.page-head { margin-bottom: 1.4rem; }
.doc-entry.page-head .head h1 { margin: 0; }
.doc-entry.page-head.is-statement { border-left: 0; padding-left: 0; }
/* On a section's page its statements are the first level; the rule between
   top-level parts is for parts, not for statements set one after another. */
.doc-entry.depth-0.is-statement { border-top: 0; padding-top: 0; margin-top: 1.1rem; }
.doc-entry .head a.num { text-decoration: none; }
.doc-entry .head a.num:hover { text-decoration: underline; }
.doc-open { margin: .5rem 0 0; font-size: .9rem; }

/* -------------------------------------------------------- progress page */

.stat-row {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(9rem, 1fr));
  gap: .7rem;
  margin: 1rem 0 1.6rem;
}
.stat {
  background: var(--panel);
  border: 1px solid var(--border);
  border-left: 3px solid var(--st-none);
  border-radius: var(--radius);
  padding: .6rem .8rem;
}
.stat .n { font-size: 1.5rem; font-weight: 620; font-variant-numeric: tabular-nums; }
.stat .l { font-size: .78rem; color: var(--muted); }
.stat.s-absent { border-left-color: var(--st-absent); }
.stat.s-missing { border-left-color: var(--st-missing); }
.stat.s-stated { border-left-color: var(--st-stated); }
.stat.s-proved { border-left-color: var(--st-proved); }
.stat.s-proved_with_axioms { border-left-color: var(--st-proved_with_axioms); }

.stackbar { display: flex; height: 14px; border-radius: 999px; overflow: hidden; border: 1px solid var(--border); }
.stackbar > span { display: block; }

.chart { width: 100%; background: var(--panel); border: 1px solid var(--border); border-radius: var(--radius); }
.chart .axis { stroke: var(--border-strong); stroke-width: 1; }
.chart .grid-line { stroke: var(--border); stroke-width: 1; stroke-dasharray: 2 3; }
.chart .tick { fill: var(--muted); font-size: 10px; }
.chart .line-total { fill: none; stroke: var(--st-none); stroke-width: 2; }
.chart .line-proved { fill: none; stroke: var(--st-proved); stroke-width: 2; }
.chart .area-proved { fill: var(--st-proved); opacity: .12; }
.chart .pt { fill: var(--panel); stroke-width: 2; cursor: pointer; }
.chart .pt.sel { fill: var(--accent); stroke: var(--accent); }

.slider-row { display: flex; align-items: center; gap: .8rem; flex-wrap: wrap; margin: .8rem 0; }
.slider-row input[type="range"] { flex: 1; min-width: 12rem; }

/* ---------------------------------------------------------- checks page */

.check {
  display: grid;
  grid-template-columns: max-content 1fr;
  gap: .3rem .8rem;
  padding: .6rem .8rem;
  border: 1px solid var(--border);
  border-left-width: 3px;
  border-radius: var(--radius);
  background: var(--panel);
  margin: .5rem 0;
}
.check.level-error { border-left-color: var(--lv-error); }
.check.level-warning { border-left-color: var(--lv-warning); }
.check.level-info { border-left-color: var(--lv-info); }
.check .code { font-family: var(--mono); font-size: .8rem; color: var(--muted); }
.check .msg { grid-column: 2; }
.check .objs { grid-column: 2; font-size: .85rem; display: flex; gap: .5rem; flex-wrap: wrap; }

.filter-row { display: flex; gap: .4rem; flex-wrap: wrap; align-items: center; margin: 1rem 0; }

/* The progress listing's search and filters. */
.listing-filters { display: flex; gap: .5rem .9rem; flex-wrap: wrap; align-items: center; margin: .6rem 0 .4rem; }
.listing-filters label { display: inline-flex; align-items: center; gap: .4em; }
.listing-filters .lbl { font-size: .78rem; color: var(--muted); text-transform: uppercase; letter-spacing: .03em; }
.listing-filters select { max-width: 16rem; }
.listing-search { flex: 1 1 16rem; min-width: 12rem; max-width: 26rem; }
.listing-count { margin: .2rem 0 .5rem; }

/* -------------------------------------------------------------- utility */

.muted { color: var(--muted); }
.small { font-size: .85rem; }
.nowrap { white-space: nowrap; }
.row { display: flex; gap: .5rem; align-items: center; flex-wrap: wrap; }
.stack { display: grid; gap: .5rem; }
.visually-hidden {
  position: absolute; width: 1px; height: 1px; overflow: hidden;
  clip: rect(0 0 0 0); clip-path: inset(50%); white-space: nowrap;
}

/* ---------------------------------------------------------- responsive */

@media (max-width: 900px) {
  .graph-page {
    grid-template-columns: 1fr;
    grid-template-rows: auto minmax(20rem, 1fr) auto;
    height: auto;
    min-height: calc(100vh - var(--topbar-h));
  }
  .graph-stage { min-height: 58vh; }
  .side { border-left: 0; border-top: 1px solid var(--border); max-height: none; }
  .doc-layout { grid-template-columns: 1fr; }
  .toc { position: static; max-height: none; border-bottom: 1px solid var(--border); padding-bottom: .8rem; }
  .topbar { flex-wrap: wrap; height: auto; padding: .5rem 1rem; gap: .4rem; }
  .topbar-main { flex: 1 1 100%; justify-content: space-between; }
  /* On its own row the box starts at the left edge, so its list hangs from
     there; anchored right it ran off the left of a phone screen. */
  .gsearch { flex: 1 1 12rem; margin-left: 0; }
  .gsearch-panel { left: 0; right: auto; }
  :root { --topbar-h: 86px; }
  .legend { display: none; }
}

@media (max-width: 560px) {
  .page { padding: 1rem .8rem 4rem; }
  .tabs a { padding: .3em .5em; font-size: .85rem; }
  dl.kv { grid-template-columns: 1fr; }
  dl.kv dt { margin-top: .5em; }
}

@media (prefers-reduced-motion: reduce) {
  .glayer, .bar > span { transition: none; }
}

/* ============================================================== graph svg */

.gnode { transition: transform .3s cubic-bezier(.3, .7, .3, 1); }
.glayer.no-anim .gnode { transition: none; }
@media (prefers-reduced-motion: reduce) { .gnode { transition: none; } }

.gnode .kindmark {
  fill: var(--faint);
  font-family: var(--mono);
  font-size: 9px;
  letter-spacing: .02em;
  pointer-events: none;
}
.gnode .expander {
  fill: var(--muted);
  font-family: var(--mono);
  font-size: 13px;
  font-weight: 700;
  pointer-events: none;
}
.gnode .ptrack { fill: var(--panel-2); }
.gnode .pfill { fill: var(--st-proved); }
.gnode:focus { outline: none; }
.gnode:focus-visible .shape { stroke: var(--accent); stroke-width: 2.6; }
.gnode.hovered .shape { stroke-width: 2.2; }

/* fill / outline by derived status */
.gnode.status-none    .shape { fill: var(--graph-node); stroke: var(--border-strong); }
.gnode.status-absent  .shape { fill: color-mix(in srgb, var(--st-absent) 12%, var(--graph-node)); stroke: var(--st-absent); }
.gnode.status-missing .shape { fill: color-mix(in srgb, var(--st-missing) 10%, var(--graph-node)); stroke: var(--st-missing); stroke-dasharray: 5 3; }
.gnode.status-stated  .shape { fill: color-mix(in srgb, var(--st-stated) 16%, var(--graph-node)); stroke: var(--st-stated); }
.gnode.status-proved  .shape { fill: color-mix(in srgb, var(--st-proved) 18%, var(--graph-node)); stroke: var(--st-proved); }
.gnode.status-proved_with_axioms .shape { fill: color-mix(in srgb, var(--st-proved_with_axioms) 18%, var(--graph-node)); stroke: var(--st-proved_with_axioms); }

.gnode.compound > .shape {
  fill: var(--graph-compound);
  stroke: var(--border-strong);
  stroke-dasharray: 4 3;
}
.gnode.compound .label { fill: var(--muted); font-size: 12.5px; }

/* Node type by shape (graph.js, `nodeShape`): a remark's folded corner and a
   section's inner frame take the outline colour of the status. */
.gnode { --node-stroke: var(--border-strong); }
.gnode.status-absent { --node-stroke: var(--st-absent); }
.gnode.status-missing { --node-stroke: var(--st-missing); }
.gnode.status-stated { --node-stroke: var(--st-stated); }
.gnode.status-proved { --node-stroke: var(--st-proved); }
.gnode.status-proved_with_axioms { --node-stroke: var(--st-proved_with_axioms); }
.gnode.compound { --node-stroke: var(--border-strong); }
.gnode .fold, .gnode .frame2 { fill: none; stroke: var(--node-stroke); stroke-width: 1; pointer-events: none; }
.gnode.type-section > .shape { stroke-width: 2; }
.gnode.compound.type-section > .shape { stroke-dasharray: none; }
.legend .shp { width: 1.6em; height: .9em; flex: none; border: 1.5px solid currentColor; color: var(--muted); }
.legend .shp.definition { border-radius: 1px; }
.legend .shp.statement { border-radius: 999px; }
.legend .shp.remark { border-radius: 0; clip-path: polygon(0 0, 70% 0, 100% 35%, 100% 100%, 0 100%); }
.legend .shp.section { border-radius: 3px; border-width: 1px; box-shadow: inset 0 0 0 1.5px var(--panel), inset 0 0 0 2.5px currentColor; }

/* A title with maths: KaTeX's HTML in a <foreignObject> (see graph.js,
   `measureMathTitles`).  The same font as the SVG labels, the colour from
   `color` since HTML has no `fill`, and every line on one line: the lines were
   broken when the node was measured, and must not be broken again. */
/* Not selectable either: a drag that pans across it would paint it as a text
   selection, which SVG text in the graph never shows. */
.gnode foreignObject.label { overflow: visible; pointer-events: none; -webkit-user-select: none; user-select: none; }
.gmath { font-size: 12px; font-weight: 550; line-height: 15px; color: var(--fg); text-align: center; }
.gmath.section { font-size: 12.5px; color: var(--muted); text-align: left; }
.gmath .gm-line, .gmath .gm-tok { white-space: nowrap; }
.gmath .katex { font-size: 1.1em; }
.gmath .katex-html { white-space: nowrap; }
.gmath-measure {
  position: absolute; left: -100000px; top: 0;
  visibility: hidden; pointer-events: none; contain: layout style;
}
.gmath-measure .gm-tok { display: inline-block; }
.gmath-measure .gm-line { width: max-content; }
.gnode.junction .shape { fill: var(--graph-junction); stroke: var(--bg); stroke-width: 2; }
.gnode.junction.selected .shape { fill: var(--accent); stroke: var(--accent); }

.arrowhead { fill: var(--graph-edge); stroke: none; }
.arrowhead.hollow { fill: var(--bg); stroke: var(--graph-edge); stroke-width: 1.4; }

.gedge .hit { stroke: transparent; stroke-width: 12; fill: none; cursor: pointer; }
.gtitle .title-hit { fill: transparent; cursor: pointer; }
.gedge.hovered path:not(.hit) { stroke: var(--accent); stroke-width: 2.4; }
.gedge.synthetic path:not(.hit) { opacity: .8; }
.gedge.spoke path:not(.hit) { stroke-width: 1.3; }
.edges.fade-in { opacity: 0; }
.edges { transition: opacity .25s ease; }

.legend .sw.status-none { color: var(--border-strong); background: var(--graph-node); }
.legend .sw.status-absent { color: var(--st-absent); background: color-mix(in srgb, var(--st-absent) 25%, transparent); }
.legend .sw.status-missing { color: var(--st-missing); background: color-mix(in srgb, var(--st-missing) 20%, transparent); }
.legend .sw.status-stated { color: var(--st-stated); background: color-mix(in srgb, var(--st-stated) 28%, transparent); }
.legend .sw.status-proved { color: var(--st-proved); background: color-mix(in srgb, var(--st-proved) 30%, transparent); }
.legend .sw.status-proved_with_axioms { color: var(--st-proved_with_axioms); background: color-mix(in srgb, var(--st-proved_with_axioms) 30%, transparent); }
.legend .lgsvg { flex: none; }

/* status filter chips pick up the status colour */
label.chk.st-chip.status-absent { border-color: var(--st-absent); }
label.chk.st-chip.status-missing { border-color: var(--st-missing); }
label.chk.st-chip.status-stated { border-color: var(--st-stated); }
label.chk.st-chip.status-proved { border-color: var(--st-proved); }
label.chk.st-chip.status-proved_with_axioms { border-color: var(--st-proved_with_axioms); }

/* ========================================================= document extras */

.toc-head {
  margin: 0 0 .4rem;
  font-size: .78rem;
  text-transform: uppercase;
  letter-spacing: .04em;
  color: var(--muted);
  font-weight: 600;
}
.doc-progress { margin: .45rem 0; max-width: 22rem; }
.doc-entry .head .role {
  font-family: var(--mono);
  font-size: .76rem;
  color: var(--faint);
}
.doc-entry > p.muted.small .role { margin-right: .2em; }

.step .step-head { align-items: center; }
.step .step-head > span:first-child {
  font-family: var(--mono);
  color: var(--accent);
}
.step .step-target { text-transform: none; letter-spacing: 0; font-weight: 400; }
.step .step-link { margin-left: auto; text-transform: none; letter-spacing: 0; font-weight: 400; }
.step .step-title { margin: .3rem 0 0; font-weight: 560; }
.step .step-prose { margin-top: .3rem; }
.step .step-prose > p:first-child { margin-top: .2em; }
.step .step-prose > p:last-child { margin-bottom: .2em; }

/* --- document view: statements set like a paper ------------------------ */
/* A statement is a numbered block under its section, not a heading of its
   own: the kind is the lead word, the title follows in parentheses style, and
   the prose is indented by a rule so consecutive statements read as blocks. */
.doc-entry.is-statement { margin: 1.1rem 0 1.1rem; padding-left: .9rem; border-left: 2px solid var(--border); }
.doc-entry.is-statement .head { gap: .4rem; }
.doc-entry.is-statement .head h2, .doc-entry.is-statement .head h3,
.doc-entry.is-statement .head h4, .doc-entry.is-statement .head h5 {
  font-size: 1rem; font-weight: 600;
}
.doc-entry .head .kindword { font-weight: 700; }
.doc-entry.is-statement .head .num { font-family: inherit; font-size: 1rem; font-weight: 700; color: var(--fg); }
.doc-entry.is-statement .head .badge { font-size: .72rem; }
/* Headings inside a body ("## Proof") are run-in labels, never larger than
   the statement they belong to. */
.body-prose h1, .body-prose h2, .body-prose h3, .body-prose h4, .body-prose h5, .body-prose h6 {
  font-size: 1rem; font-weight: 600; font-style: italic; margin: .9em 0 .25em; line-height: 1.3;
}
.body-prose h1::after, .body-prose h2::after, .body-prose h3::after { content: '.'; }
.doc-entry.is-section .prose { margin-top: .6rem; }
/* A grid track sized 1fr still has min-width:auto, so one wide formula or an
   unbreakable token pushes the prose column past the viewport. */
.doc-layout > * { min-width: 0; }

/* ===================================================== search, proofs, comments */

.row > .spacer { flex: 1; }
textarea {
  font: inherit;
  color: inherit;
  background: var(--panel);
  border: 1px solid var(--border-strong);
  border-radius: var(--radius);
  padding: .45em .6em;
  width: 100%;
  resize: vertical;
}
button.primary { background: var(--accent); border-color: var(--accent); color: var(--accent-fg); }
button.primary:hover { background: var(--accent); filter: brightness(1.08); }

/* The entry a focus link led to, or a proof's, marked briefly. */
@keyframes doc-flash {
  from { background: var(--accent-soft); }
  to { background: transparent; }
}
.doc-entry.flash, .step.flash, .proof.flash { animation: doc-flash 1.6s ease-out; }
@media (prefers-reduced-motion: reduce) {
  .doc-entry.flash, .step.flash, .proof.flash { animation: none; outline: 2px solid var(--accent-soft); }
}

/* Proofs fold under their "Proof." heading. */
.doc-controls .proof-toggle { font-size: .82rem; padding: .15em .55em; margin-left: .4rem; }
details.proof > summary {
  cursor: pointer;
  list-style: none;
  display: flex;
  align-items: baseline;
  gap: .35em;
}
details.proof > summary::-webkit-details-marker { display: none; }
details.proof > summary::before {
  content: "▸";
  color: var(--muted);
  font-size: .8em;
  transition: transform .15s;
}
details.proof[open] > summary::before { transform: rotate(90deg); }
details.proof > summary > :is(h1, h2, h3, h4, h5, h6) { margin: .9em 0 .25em; }
details.proof:not([open]) > summary::after {
  content: "(folded: click to show)";
  color: var(--faint);
  font-size: .82rem;
}
details.proof > summary:hover > :is(h1, h2, h3, h4, h5, h6) { color: var(--accent); }

/* Comments, at the foot of an object's page. */
.comments h3 { margin-top: 0; }
.comment-list { display: flex; flex-direction: column; gap: .8rem; margin-bottom: 1.2rem; }
.comment { border-left: 2px solid var(--border); padding-left: .8rem; }
.comment-head { display: flex; flex-wrap: wrap; align-items: baseline; gap: .6rem; margin-bottom: .2rem; }
.comment-anchor { margin-left: auto; font-family: var(--mono); }
.comment-form { border-top: 1px solid var(--border); padding-top: .9rem; }
.comment-form h4 { margin: 0 0 .6rem; }
.comment-field { display: flex; flex-direction: column; gap: .2rem; margin-bottom: .6rem; font-size: .88rem; }
.comment-field > span { color: var(--muted); }
.comment-field input[type="text"] { max-width: 22rem; }
.comment-preview {
  border: 1px dashed var(--border-strong);
  border-radius: var(--radius);
  padding: .6em .8em;
  margin-bottom: .6rem;
  min-height: 7.5em;
}
.comment-preview[hidden], .comment-field textarea[hidden] { display: none; }