/* frc-ledger — shared styles. No framework, no build step. */

:root {
  --bg:        #fbfaf8;
  --panel:     #ffffff;
  --ink:       #1a1a1a;
  --ink-soft:  #5a5a5a;
  --ink-faint: #8a8a86;
  --rule:      #e3e0da;
  --rule-soft: #efece7;
  --accent:    #2f5d7c;

  --pub:   #1f6b45;  --pub-bg:   #e6f2ea;
  --sub:   #2f5d7c;  --sub-bg:   #e5eef4;
  --rev:   #8a5a10;  --rev-bg:   #f8efdc;
  --rej:   #8c3a3a;  --rej-bg:   #f6e7e7;
  --pre:   #4a4f63;  --pre-bg:   #eceef4;
  --dra:   #6d6a63;  --dra-bg:   #efedea;
  --ess:   #5c4478;  --ess-bg:   #eee9f4;

  --mono: ui-monospace, SFMono-Regular, "SF Mono", Menlo, Consolas, monospace;
  --serif: "Iowan Old Style", "Palatino Linotype", Palatino, Georgia, serif;
}

@media (prefers-color-scheme: dark) {
  :root {
    --bg:        #16171a;
    --panel:     #1d1f23;
    --ink:       #e8e6e1;
    --ink-soft:  #a8a49c;
    --ink-faint: #7d7a76;
    --rule:      #33363c;
    --rule-soft: #26282d;
    --accent:    #8fc0e0;

    --pub: #7fc7a0; --pub-bg: #1b2f24;
    --sub: #8fc0e0; --sub-bg: #1a2833;
    --rev: #dcb268; --rev-bg: #302716;
    --rej: #dd9a9a; --rej-bg: #2f1f1f;
    --pre: #a9b0c8; --pre-bg: #23262e;
    --dra: #a8a49c; --dra-bg: #26262a;
    --ess: #bfa8dd; --ess-bg: #272031;
  }
}

* { box-sizing: border-box; }

body {
  margin: 0;
  padding: 2.5rem 1.5rem 5rem;
  background: var(--bg);
  color: var(--ink);
  font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Helvetica, Arial, sans-serif;
  font-size: 15px;
  line-height: 1.55;
  -webkit-font-smoothing: antialiased;
}

.wrap { max-width: 1080px; margin: 0 auto; }

/* ---- masthead ---- */
header { border-bottom: 1px solid var(--rule); padding-bottom: 1rem; margin-bottom: 1.75rem; }
h1 { font-family: var(--serif); font-size: 1.9rem; font-weight: 600; margin: 0 0 .3rem; letter-spacing: -.01em; }
.sub { color: var(--ink-soft); font-size: .92rem; margin: 0; }
.sub a { color: var(--accent); }
nav { margin-top: .9rem; display: flex; gap: 1.1rem; font-size: .88rem; }
nav a { color: var(--ink-soft); text-decoration: none; border-bottom: 1px solid transparent; padding-bottom: 2px; }
nav a:hover { color: var(--ink); border-bottom-color: var(--ink); }
nav a[aria-current="page"] { color: var(--ink); border-bottom-color: var(--ink); font-weight: 600; }

/* ---- summary strip ---- */
.tally { display: flex; flex-wrap: wrap; gap: .5rem; margin-bottom: 1.5rem; }
.tally button {
  font: inherit; font-size: .84rem; cursor: pointer;
  border: 1px solid var(--rule); border-radius: 999px;
  background: var(--panel); color: var(--ink-soft);
  padding: .3rem .85rem; display: inline-flex; align-items: center; gap: .45rem;
  transition: border-color .12s, color .12s;
}
.tally button:hover { border-color: var(--ink-faint); color: var(--ink); }
.tally button[aria-pressed="true"] { border-color: var(--ink); color: var(--ink); font-weight: 600; }
.tally .n { font-family: var(--mono); font-size: .8rem; opacity: .75; }
.tally .dot { width: 8px; height: 8px; border-radius: 50%; display: inline-block; }

/* ---- search ---- */
.tools { display: flex; gap: .75rem; align-items: center; margin-bottom: 1rem; flex-wrap: wrap; }
input[type="search"] {
  font: inherit; font-size: .9rem; padding: .4rem .7rem; flex: 1; min-width: 220px;
  border: 1px solid var(--rule); border-radius: 5px;
  background: var(--panel); color: var(--ink);
}
input[type="search"]:focus { outline: 2px solid var(--accent); outline-offset: -1px; border-color: transparent; }
.count { color: var(--ink-faint); font-size: .85rem; font-family: var(--mono); }

/* ---- table ---- */
table { width: 100%; border-collapse: collapse; background: var(--panel); }
thead th {
  text-align: left; font-size: .75rem; text-transform: uppercase; letter-spacing: .07em;
  color: var(--ink-faint); font-weight: 600;
  padding: .55rem .7rem; border-bottom: 1px solid var(--rule);
  cursor: pointer; user-select: none; white-space: nowrap;
}
thead th:hover { color: var(--ink); }
thead th .car { opacity: .45; font-size: .7rem; }
tbody tr { border-bottom: 1px solid var(--rule-soft); }
tbody tr:hover { background: color-mix(in srgb, var(--accent) 5%, transparent); }
td { padding: .6rem .7rem; vertical-align: top; }

td.key { font-family: var(--mono); font-size: .82rem; color: var(--ink-soft); white-space: nowrap; }
td.title { font-family: var(--serif); font-size: 1rem; }
td.title .note { display: block; font-family: -apple-system, sans-serif; font-size: .78rem; color: var(--ink-faint); margin-top: .2rem; font-style: italic; }
td.doi { font-family: var(--mono); font-size: .78rem; white-space: nowrap; }
td.doi a { color: var(--accent); text-decoration: none; border-bottom: 1px solid color-mix(in srgb, var(--accent) 35%, transparent); }
td.doi a:hover { border-bottom-color: var(--accent); }
td.doi .none { color: var(--ink-faint); }
td.status { white-space: nowrap; }
td.hist { font-size: .78rem; color: var(--ink-faint); }
td.hist .h { font-family: var(--mono); white-space: nowrap; }

/* ---- badges ---- */
.badge {
  display: inline-block; font-size: .76rem; font-weight: 600;
  padding: .15rem .55rem; border-radius: 4px; white-space: nowrap;
  font-family: var(--mono); letter-spacing: -.01em;
}
.badge.published { color: var(--pub); background: var(--pub-bg); }
.badge.submitted { color: var(--sub); background: var(--sub-bg); }
.badge.revision  { color: var(--rev); background: var(--rev-bg); }
.badge.rejected  { color: var(--rej); background: var(--rej-bg); }
.badge.preprint  { color: var(--pre); background: var(--pre-bg); }
.badge.draft     { color: var(--dra); background: var(--dra-bg); }
.badge.essay     { color: var(--ess); background: var(--ess-bg); }

.dot.published { background: var(--pub); } .dot.submitted { background: var(--sub); }
.dot.revision  { background: var(--rev); } .dot.rejected  { background: var(--rej); }
.dot.preprint  { background: var(--pre); } .dot.draft     { background: var(--dra); }
.dot.essay     { background: var(--ess); } .dot.all       { background: var(--ink-faint); }

/* ---- legend / footer ---- */
.legend { margin-top: 1.1rem; margin-bottom: 1.75rem; font-size: .84rem; color: var(--ink-soft); }
.legend + .tally { margin-top: 1.75rem; }
section.prose.closing + .legend, footer + .legend { margin-top: 2.5rem; padding-top: 1.25rem; border-top: 1px solid var(--rule); }
.legend h2 { font-size: .78rem; text-transform: uppercase; letter-spacing: .07em; color: var(--ink-faint); margin: 0 0 .6rem; }
.legend dl { display: grid; grid-template-columns: auto 1fr; gap: .3rem 1rem; margin: 0; }
.legend dt { font-family: var(--mono); font-size: .8rem; color: var(--ink); }
.legend dd { margin: 0; }
footer { margin-top: 2rem; font-size: .8rem; color: var(--ink-faint); }
footer code { font-family: var(--mono); font-size: .95em; }

.empty { padding: 2.5rem; text-align: center; color: var(--ink-faint); font-style: italic; }

@media (max-width: 720px) {
  body { padding: 1.5rem 1rem 3rem; }
  td.hist, th.hist { display: none; }
  td.title { font-size: .95rem; }
}

/* ---- home page (added by tools/site_build.py) ---- */
.home { line-height: 1.6; }
.home h2 { font-family: var(--serif); font-size: 1.45rem; font-weight: 600; margin: 0.2rem 0 0.8rem; letter-spacing: -.01em; }
.home h3 { font-size: 1rem; font-weight: 600; margin: 1.8rem 0 0.4rem; }
.home p { margin: 0 0 0.9rem; }
.home figure.hero { margin: 1.4rem auto 1.8rem; max-width: 800px; }
.home figure.hero video { display: block; width: 100%; max-width: 800px; height: auto; border-radius: 6px; background: #0d0d0f; }
.home figure.hero figcaption { font-size: .84rem; color: var(--ink-soft); margin-top: .55rem; line-height: 1.45; }
.home figure.fig { margin: 1.4rem auto 1.2rem; max-width: 860px; }
.home figure.fig img { display: block; width: 100%; height: auto; border-radius: 6px; background: #fff; }
.home figure.fig figcaption { font-size: .84rem; color: var(--ink-soft); margin-top: .55rem; line-height: 1.45; }
.home ol.refs { font-size: .86rem; color: var(--ink-soft); line-height: 1.5; padding-left: 2.2rem; margin: 0 0 1rem; }
.home ol.refs li { margin-bottom: .3rem; }
.home ol.refs li:target { background: color-mix(in srgb, var(--accent) 10%, transparent); border-radius: 4px; }
.home a[href^="#ref-"] { border-bottom: none; font-size: .85em; vertical-align: 1px; }
.home sup, .home sub { line-height: 0; }   /* superscripts and subscripts leave the line height alone (15 October 2026) */
/* ---- ledger pages (added by tools/site_build.py) ---- */
/* every link on every page takes the accent token (light and dark) except the tab bar and the title links of the
   publications list; the stylesheet above colours only nav, .sub and DOI links, and a page has no <main> wrapper
   in general (publications.html), so the rule is scoped to .wrap. :where() keeps the specificity at (0,1,1) so
   the witness rules below still win. */
.wrap a:where(:not(nav a):not(.ledgerlink)), .wrap a:where(:not(nav a):not(.ledgerlink)):visited { color: var(--accent); text-decoration: none; border-bottom: 1px solid color-mix(in srgb, var(--accent) 35%, transparent); }
.wrap a:where(:not(nav a):not(.ledgerlink)):hover { border-bottom-color: var(--accent); }
.wrap a.wit.ok, .wrap a.wit.ok:visited, .wrap a.wit.ok:hover { color: var(--pub); border-bottom-color: color-mix(in srgb, var(--pub) 35%, transparent); }
.wrap a.wit.fail, .wrap a.wit.fail:visited, .wrap a.wit.fail:hover { color: var(--rej); border-bottom-color: color-mix(in srgb, var(--rej) 35%, transparent); }
table.ledger td { vertical-align: top; }
table.ledger td.lab { font-family: var(--mono); font-size: 0.85rem; white-space: nowrap; }
table.ledger td.lab .key { display: block; color: var(--ink-faint); font-size: 0.72rem; }
table.ledger td.pred .name { display: block; font-weight: 600; margin-bottom: 0.15rem; }
table.ledger td.src { font-size: 0.82rem; color: var(--ink-soft); }
table.ledger td.src code, table.ledger td.src .wit { font-family: var(--mono); font-size: 0.78rem; }
table.ledger tr.blockhead td { background: var(--rule-soft); padding: 0.55rem 0.6rem; font-size: 0.9rem; }
table.ledger tr.blockhead td.bw { padding-left: .7rem; white-space: nowrap; }   /* the block head's glyphs and counts in their own cell, the Sources column (9 October 2026) */
table.ledger tr.blockhead .bglyphs { display: flex; align-items: center; gap: 0; }   /* the block head's glyphs and counts (8 October 2026): the menu totals' form, left-aligned under the Sources header (9 October 2026) */
.wrap table.ledger tr.blockhead .bglyphs a.sum:first-child { margin-left: -.14rem; }   /* the first glyph's left edge on the column's text edge (the pill's own .14rem padding taken off) */
.wrap table.ledger tr.blockhead .bglyphs a.sum, .wrap table.ledger tr.blockhead .bglyphs a.sum:visited { display: inline-flex; align-items: center; gap: .2rem; height: 22px; padding: 0 .25rem 0 .14rem; margin: 0 0 0 .2rem; border: 0; border-radius: 4px; font-family: var(--mono); font-size: .85rem; text-decoration: none; }
.wrap table.ledger tr.blockhead .bglyphs a.sum:hover { background: color-mix(in srgb, var(--ink) 8%, transparent); border: 0; }
table.ledger tr.blockhead .bglyphs .n { line-height: 1; color: #419457; font-weight: 400; } table.ledger tr.blockhead .bglyphs a.sum.py .n { color: #a27900; } table.ledger tr.blockhead .bglyphs a.sum.ml .n { color: #7974c6; } table.ledger tr.blockhead .bglyphs a.sum.fail .n { color: #c04a4a; }
table.ledger tr.blockhead .bglyphs img.leanico, table.ledger tr.blockhead .bglyphs img.runico { width: 16px; height: 16px; display: block; }
@media (prefers-color-scheme: dark) { table.ledger tr.blockhead .bglyphs img, table.ledger tr.blockhead .bglyphs .n { opacity: .85; } }
table.ledger tr.target td { background: var(--sub-bg); }
.tag { display: inline-block; min-width: 1.4em; padding: 0.05rem 0.4rem; border-radius: 0.3rem; font-family: var(--mono); font-size: 0.78rem; font-weight: 600; text-align: center; }
.tag.t { color: var(--pub); background: var(--pub-bg); }   .tag.d { color: var(--dra); background: var(--dra-bg); }
.tag.i { color: var(--sub); background: var(--sub-bg); }   .tag.r { color: var(--ess); background: var(--ess-bg); }
.tag.om { color: var(--rev); background: var(--rev-bg); }  .tag.o { color: var(--rej); background: var(--rej-bg); }
.tag.g, .tag.p { color: var(--ink); background: var(--rule-soft); } .tag.e { color: var(--pre); background: var(--pre-bg); }
.dot.t-t { background: var(--pub); } .dot.t-d { background: var(--dra); } .dot.t-i { background: var(--sub); } .dot.t-r { background: var(--ess); }
.dot.t-om { background: var(--rev); } .dot.t-o { background: var(--rej); } .dot.t-g, .dot.t-p { background: var(--ink); } .dot.t-e { background: var(--pre); } .dot.t-all { background: var(--ink-faint); }
.dot.ok { background: var(--pub); } .dot.fail { background: var(--rej); }
.wit.ok { color: var(--pub); } .wit.fail { color: var(--rej); }
/* ---- Lean witnesses (added by tools/site_build.py): the declaration name, its axioms dot, the live link ---- */
.wrap a.lean.ico, .wrap a.lean.ico:visited { display: inline-flex; align-items: center; justify-content: center; width: 20px; height: 22px; margin: 0 .075rem; border-bottom: none; border-radius: 5px; color: var(--ink-soft); vertical-align: middle; }
.wrap a.lean.ico:hover { background: var(--rule-soft); color: var(--accent); }
.wrap a.lean.ico svg { width: 15px; height: 15px; }
img.leanico { width: 16px; height: 16px; display: block; filter: invert(.78); }          /* a light glyph on transparency: darkened on the light theme */
img.leanico.ok, img.leanico.ml, img.leanico.fail { filter: none; }      /* the coloured versions, the library's colour on every page: green the core (lean-ok.png #419457), violet Mathlib (lean-ml.png #7974c6), red a proof the gate rejects (lean-fail.png #c04a4a); the tier is in the hover */
pre.lean img.leanico { width: 12px; height: 12px; display: inline-block; vertical-align: -2px; margin-right: .4em; }
@media (prefers-color-scheme: dark) { img.leanico { filter: none; opacity: .85; } }
.wrap a.lean.ico.live { width: auto; padding: 0 3px 0 2px; }
.wrap a.wit.ico, .wrap a.wit.ico:visited { display: inline-flex; align-items: center; justify-content: center; width: 20px; height: 22px; margin: 0 .075rem; border-bottom: none; border-radius: 5px; color: var(--ink-soft); vertical-align: middle; }
.wrap a.wit.ico:hover { background: var(--rule-soft); color: var(--accent); }
.wrap a.wit.ico svg { width: 15px; height: 15px; fill: none; stroke: currentColor; stroke-width: 1.6; stroke-linecap: round; stroke-linejoin: round; }
.wrap a.wit.ico.py.ok { color: var(--pub); } .wrap a.wit.ico.py.fail { color: var(--rej); }
/* syntax colours (Pygments token classes) — a quiet palette on the site's tokens, both themes */
pre.lean .k, pre.lean .kn, pre.lean .kd, pre.lean .kr, pre.lean .kc, pre.lean .kt { color: #7a3e9d; }   /* keywords */
pre.lean .s, pre.lean .s1, pre.lean .s2, pre.lean .sd, pre.lean .sa, pre.lean .si, pre.lean .se, pre.lean .sb, pre.lean .sh, pre.lean .sx { color: #2a7f62; }   /* strings, docstrings */
pre.lean .c, pre.lean .c1, pre.lean .cm, pre.lean .ch, pre.lean .cs { color: var(--ink-faint); font-style: italic; }   /* comments */
pre.lean .ln.decl .c1 { color: var(--accent); font-style: normal; font-weight: 600; }                         /* the predicate marker */
pre.lean .m, pre.lean .mi, pre.lean .mf, pre.lean .mh, pre.lean .mo, pre.lean .mb { color: #b35c00; }         /* numbers */
pre.lean .nb, pre.lean .bp { color: #2f5d7c; }                                                                 /* builtins */
pre.lean .nf, pre.lean .fm { color: #1f5fbf; }                                                                 /* function names */
pre.lean .nc, pre.lean .nn { color: #1f5fbf; font-weight: 600; }                                               /* classes, modules */
pre.lean .nd { color: #7a3e9d; }                                                                               /* decorators */
pre.lean .o, pre.lean .ow { color: var(--ink-soft); }                                                          /* operators */
@media (prefers-color-scheme: dark) {
  pre.lean .k, pre.lean .kn, pre.lean .kd, pre.lean .kr, pre.lean .kc, pre.lean .kt, pre.lean .nd { color: #c792ea; }
  pre.lean .s, pre.lean .s1, pre.lean .s2, pre.lean .sd, pre.lean .sa, pre.lean .si, pre.lean .se, pre.lean .sb, pre.lean .sh, pre.lean .sx { color: #7ec699; }
  pre.lean .m, pre.lean .mi, pre.lean .mf, pre.lean .mh, pre.lean .mo, pre.lean .mb { color: #f0a45d; }
  pre.lean .nb, pre.lean .bp { color: #82aaff; } pre.lean .nf, pre.lean .fm, pre.lean .nc, pre.lean .nn { color: #82aaff; }
}
.src .glyphs { display: flex; align-items: center; gap: .15rem; margin: 0 0 .25rem; }   /* the witnesses lead the Sources cell (13 October 2026) */
img.runico { width: 16px; height: 16px; display: block; object-fit: contain; filter: invert(.78); }   /* the run glyphs: light on transparency, darkened on the light theme like the plain Lean glyph */
img.runico.pysrc { filter: brightness(0) invert(.55); }   /* the python-source glyph, a white PNG: no verdict (a script cited whole) mid grey */
img.runico.pyok, img.runico.pyfail, .wrap a.ico:hover img.runico.pyok, .wrap a.ico:hover img.runico.pyfail { filter: none; }   /* the python glyph in its verdict colour, drawn in the PNG (media/python-ok.png gold #a27900, media/python-fail.png red #c04a4a) as the Lean glyphs are: no filter chain, so every browser shows the colour of the count beside it (12 October 2026) */
img.runico.colab { width: 19px; filter: none; }                                                        /* the Colab mark is coloured: shown as drawn in both themes */
.wrap a.ico:hover img.runico.colab { filter: none; opacity: .8; }
.wrap a.ico:hover img.runico { filter: invert(.45) sepia(.6) saturate(3) hue-rotate(170deg); }        /* the accent on hover */
.legend .ico img.runico { display: inline-block; vertical-align: -3px; }
@media (prefers-color-scheme: dark) { img.runico { filter: none; opacity: .85; } .wrap a.ico:hover img.runico { filter: none; opacity: 1; }
 }
.wrap a.lean.ico .play, .legend .ico .play { font-size: .55rem; margin-left: 2px; line-height: 1; }
.legend .ico img.leanico { display: inline-block; vertical-align: -3px; }
.legend.lean dt { white-space: nowrap; }
.ax { display: inline-block; margin: 0 .3rem 0 .15rem; font-size: .62rem; line-height: 1; vertical-align: .1em; }
.ax.ok { color: var(--pub); } .ax.bad { color: var(--rej); }
.lean.missing { color: var(--rej); font-family: var(--mono); font-size: .78rem; text-decoration: line-through; }
pre.lean { font-family: var(--mono); font-size: .8rem; line-height: 1.45; overflow-x: auto; padding: .6rem .8rem 0; margin: 1rem 0; border: 1px solid var(--rule-soft); border-radius: 6px; background: var(--pre-bg, transparent); }
pre.lean .ln { display: block; white-space: pre-wrap; overflow-wrap: anywhere; padding-left: 3.5rem; text-indent: -3.5rem; }   /* long lines wrap, continuation lines hang past the line number */ pre.lean .ln:target, pre.lean .ln:has(> a.pred:target) { background: color-mix(in srgb, var(--accent) 14%, transparent); }   /* a predicate anchor (p10015, the paper's witness link) highlights its line */
pre.lean .lno, .wrap pre.lean a.lno, .wrap pre.lean a.lno:visited { display: inline-block; width: 3rem; text-align: right; margin-right: .5rem; text-indent: 0; color: var(--ink-faint); border: 0; font-size: .72rem; user-select: none; }
.wrap pre.lean a.gh, .wrap pre.lean a.gh:visited { border: 0; margin-right: .35em; font-size: .72rem; color: var(--ink-soft); }
.checks, .master, .refs { margin-top: 0.25rem; }
.kind { color: var(--ink-faint); font-size: 0.85em; }
.sf { font-family: ui-sans-serif, system-ui, sans-serif; }
.rowref { font-family: var(--mono); font-size: 0.85em; } .rowref.off { color: var(--ink-faint); }
.cite { font-size: 0.85em; } .ref { border-bottom: 1px dotted var(--rule); cursor: help; } .ref.off { color: var(--ink-faint); }
section.prose { margin: 1rem 0; line-height: 1.55; } section.prose.closing { border-top: 1px solid var(--rule); padding-top: 1rem; }
p.hist { font-size: 0.85rem; color: var(--ink-soft); }
section.abstract { font-size: 0.95rem; line-height: 1.5; color: var(--ink-soft); margin: 0.6rem 0 0; }   /* full width of .wrap, like the table below it */
section.abstract p.meta { margin: 0.55rem 0 0; } section.abstract p.meta a.badge { margin-right: .3rem; }   /* a page built before the badges moved to the menu line keeps its header until its next build */
nav { align-items: center; flex-wrap: wrap; } nav.withmeta { flex-wrap: wrap-reverse; }   /* a menu line with the badges: one line above 760 px (the widest menu, 38-s13's, needs 734 px) */
nav .meta { margin-left: auto; display: inline-flex; align-items: center; gap: .45rem; }   /* the paper's badges at the right end of the menu line */
@media (max-width: 760px) {   /* a narrow screen (12 October 2026): Home and the badges or glyph totals on the first line, the other tabs on the second */
  nav.withmeta { flex-wrap: wrap; row-gap: 0; }
  nav.withmeta > .meta { order: 1; }
  nav.withmeta::after { content: ""; order: 2; flex-basis: 100%; height: .5rem; }   /* the line break */
  nav.withmeta > a:not(:first-child) { order: 3; }
}
.wrap a.colab, .wrap a.colab:visited, .wrap a.colab:hover { border-bottom: none; text-decoration: none; display: inline-block; line-height: 0; vertical-align: middle; }
.wrap a.badge, .wrap a.badge:visited, .wrap a.badge:hover { border-bottom: none; text-decoration: none; display: inline-block; line-height: 0; vertical-align: middle; margin: 0; padding: 0; }   /* the header badges: inline SVG, each a link; the .badge padding is the text badges' */
.wrap a.badge svg { display: block; } .wrap a.badge svg text { font-weight: 400; letter-spacing: 0; } .wrap a.badge:hover svg { filter: brightness(1.08); }
.wrap img.colab { height: 20px; display: block; }
header.paper { margin-bottom: 1rem; }
header.paper + main > section.prose:first-child { margin-top: 0; }
p.note { color: var(--ink-soft); font-size: 0.9rem; margin: 0 0 1rem; }
td.links a { display: inline-block; margin-right: 0.35rem; font-size: 0.8rem; }
/* the (i) after a column header: links to the legend below the table */
.wrap thead th a.info, .wrap thead th a.info:visited { display: inline-block; vertical-align: middle; position: relative; top: -1px; margin-left: 0.15rem; border-bottom: none; color: var(--ink-faint); line-height: 0; }
.wrap thead th a.info:hover { color: var(--accent); }
thead th a.info svg { width: 12px; height: 12px; stroke: currentColor; fill: none; stroke-width: 1.7; stroke-linecap: round; display: block; }
.empty + .legend { margin-top: 2rem; padding-top: 1.25rem; border-top: 1px solid var(--rule); }
.legend + .legend { margin-top: 1.25rem; }
section.legend:target { scroll-margin-top: 1rem; }
/* the Package column's glyphs: a 26 px hit area, the ink-soft colour, the accent on hover; the legend shows each beside its word */
.wrap td.links a.ico, .wrap td.links a.ico:visited { display: inline-flex; align-items: center; justify-content: center; width: 26px; height: 26px; margin-right: 0.2rem; border-bottom: none; border-radius: 5px; color: var(--ink-soft); vertical-align: middle; }
.wrap td.links a.ico:hover { background: var(--rule-soft); color: var(--accent); }
.ico svg { width: 17px; height: 17px; stroke: currentColor; fill: none; stroke-width: 1.6; stroke-linecap: round; stroke-linejoin: round; display: block; }
.legend dt .ico { display: inline-block; vertical-align: -4px; margin-right: 0.15rem; color: var(--ink-soft); }
a.ledgerlink { color: inherit; text-decoration: none; border-bottom: 1px solid var(--rule); }
a.ledgerlink:hover { border-bottom-color: var(--ink); }
.wrap a.badgelink, .wrap a.badgelink:visited { text-decoration: none; border-bottom: none; }
.wrap a.badgelink:hover .badge { filter: brightness(0.92); }
/* ---- phones (added by tools/site_build.py): the tables stack, one row a card, so the layout viewport stays the device
   width and the type stays the Home page's 15px instead of the browser zooming out to fit a 700 px table ---- */
html { -webkit-text-size-adjust: 100%; text-size-adjust: 100%; }
mjx-container { max-width: 100%; overflow-x: auto; overflow-y: hidden; }
@media (max-width: 720px) {
  .wrap table { display: block; width: 100%; }
  .wrap table thead { display: none; }
  .wrap table tbody { display: block; width: 100%; }
  .wrap table tr { display: grid; grid-template-columns: minmax(0, 1fr) auto; column-gap: .6rem; padding: .6rem 0; }
  .wrap table td { padding: 0; min-width: 0; overflow-wrap: anywhere; }
  table.ledger tr { grid-template-areas: "lab status" "pred pred" "src src"; }
  table.ledger tr.blockhead { display: block; padding: 0; }
  table.ledger tr.blockhead td { padding: .5rem .6rem; }
  table.ledger tr.blockhead td.bw { display: block; padding: 0 .6rem .5rem; }
  table.ledger td.lab { grid-area: lab; white-space: normal; padding-bottom: .25rem; }
  table.ledger td.lab .key { display: inline; margin-left: .45rem; }
  table.ledger td.status { grid-area: status; text-align: right; }
  table.ledger td.pred { grid-area: pred; }
  table.ledger td.src { grid-area: src; padding-top: .35rem; }
  table:not(.ledger) tr { grid-template-areas: "key status" "title title" "links links"; }
  td.key { grid-area: key; white-space: normal; }
  table:not(.ledger) td.status { grid-area: status; text-align: right; }
  td.title { grid-area: title; padding: .2rem 0; }
  td.links { grid-area: links; }
  td.doi { white-space: normal; }
  .empty { padding: 1.5rem 0; }
  nav { gap: .4rem .9rem; }
}
/* the source pages' bar: the way back to the ledger (at the predicate when opened at one), the file's path and size, copy, download, the editor */
.srcbar { position: sticky; top: 0; z-index: 2; display: flex; align-items: center; flex-wrap: wrap; gap: .5rem .75rem; margin: 1rem 0 0; padding: .45rem .8rem; border: 1px solid var(--rule-soft); border-bottom: 0; border-radius: 6px 6px 0 0; background: var(--bg); font-size: .82rem; }
.srcbar + pre.lean { margin-top: 0; border-top-left-radius: 0; border-top-right-radius: 0; }
.srcbar .back { display: inline-flex; align-items: center; gap: .35rem; }
.wrap .srcbar a.back, .wrap .srcbar a.back:visited, .wrap .srcbar a.back:hover, .wrap .srcbar .also a, .wrap .srcbar .also a:visited, .wrap .srcbar .also a:hover { border-bottom: 0; }   /* the bar's links carry no underline */
.srcbar .back svg { width: 15px; height: 15px; fill: none; stroke: currentColor; stroke-width: 1.8; stroke-linecap: round; stroke-linejoin: round; }
.srcbar .also { color: var(--ink-faint); }
.srcbar .path { color: var(--ink-faint); font-family: var(--mono); font-size: .76rem; margin-left: auto; }
.srcbar .tool, .wrap .srcbar a.tool, .wrap .srcbar a.tool:visited { display: inline-flex; align-items: center; gap: .35rem; padding: .2rem .5rem; border: 1px solid var(--rule-soft); border-radius: 5px; background: transparent; color: var(--ink-soft); font: inherit; font-size: .78rem; line-height: 1.2; cursor: pointer; text-decoration: none; }
.srcbar .tool:hover, .srcbar .tool:focus-visible, .wrap .srcbar a.tool:hover { color: var(--accent); border-color: var(--accent); }
.srcbar .tool svg { width: 14px; height: 14px; fill: none; stroke: currentColor; stroke-width: 1.7; stroke-linecap: round; stroke-linejoin: round; }
.srcbar .tool.done { color: #419457; border-color: #419457; } .srcbar .tool.failed { color: #c04a4a; border-color: #c04a4a; }
.srcbar .vh { position: absolute; width: 1px; height: 1px; overflow: hidden; clip: rect(0 0 0 0); }
td.links a.sum, .wrap td.links a.sum, .wrap td.links a.sum:visited { display: inline-flex; align-items: center; gap: .2rem; width: auto; height: 22px; padding: 0 .25rem 0 .14rem; margin-right: .2rem; border: 0; border-radius: 4px; color: #419457; font-family: var(--mono); font-size: .78rem; text-decoration: none; }   /* the Publications table: a glyph and its count */
.wrap td.links a.sum .n, .wrap td.links a.sum:hover .n { color: #419457; } .wrap td.links a.sum.py .n, .wrap td.links a.sum.py:hover .n { color: #a27900; } .wrap td.links a.sum.ml .n, .wrap td.links a.sum.ml:hover .n { color: #7974c6; } .wrap td.links a.sum.fail .n, .wrap td.links a.sum.fail:hover .n { color: #c04a4a; } .wrap td.links a.ico.sum:hover { background: var(--rule-soft); }   /* the count is set on its own span in the glyph's own colour (gold the python count, green the core's, violet Mathlib's, red a failure), so neither the .ico/.lean.ico hover rules (accent) nor the python glyph's --pub reach it: hover shows the pill only, as the ledger's glyphs do */
.wrap td.links a.sum .n { line-height: 1; min-width: 1.4em; } td.links { white-space: nowrap; }
nav .meta .totals { display: inline-flex; align-items: center; }   /* a paper page: its witnesses as glyph and count beside the DOI badge (8 October 2026) */
nav .meta.totals { gap: 0; }   /* the corpus totals at the right end of the menu line of the five top-level pages (the slot of a paper page's badges): the same badges as the Publications rows, each opening Publications */
.wrap nav .totals a.sum, .wrap nav .totals a.sum:visited { display: inline-flex; width: auto; height: 22px; align-items: center; gap: .2rem; padding: 0 .25rem 0 .14rem; margin: 0 0 0 .2rem; border: 0; border-radius: 4px; font-family: var(--mono); font-size: .78rem; font-weight: 400; text-decoration: none; color: #419457; }   /* width auto: the .ico rules fix 20px */
.wrap nav .totals a.sum:hover { background: var(--rule-soft); border: 0; }
nav .totals .n { line-height: 1; min-width: 1.4em; color: #419457; } nav .totals a.sum.py .n { color: #a27900; } nav .totals a.sum.ml .n { color: #7974c6; } nav .totals a.sum.fail .n { color: #c04a4a; } nav .totals a.sum.lab .n { color: var(--ink-soft); }
nav .totals a.sum.lab svg { width: 17px; height: 17px; stroke: var(--ink-soft); fill: none; stroke-width: 1.6; stroke-linecap: round; stroke-linejoin: round; }
nav .totals img.leanico, nav .totals img.runico { width: 16px; height: 16px; display: block; }
@media (prefers-color-scheme: dark) { nav .totals img, nav .totals .n { opacity: .85; } .wrap nav .totals a.sum:hover { background: color-mix(in srgb, var(--ink) 13%, transparent); } .wrap td.links a.sum img, .wrap td.links a.sum .n, .wrap td.links a.sum:hover img, .wrap td.links a.sum:hover .n { opacity: .85; } .wrap td.links a.ico.sum:hover { background: color-mix(in srgb, var(--ink) 13%, transparent); } }   /* dark theme: the pill in ink at 13 % (rule-soft is 4 L* above the dark page, under the row's own hover tint it vanished); glyph and count stay at the theme's .85 under hover too (the run-glyph rule alone would brighten the python image): the hover highlights the badge, the pill behind glyph and count, nothing inside it */
.srcbar.solo { position: static; border: 0; padding-left: 0; padding-right: 0; margin: 1.1rem 0 .2rem; }   /* the bar on its own (a package page): no frame, flush with the text */
pre.lean .ln, pre.lean a.pred { scroll-margin-top: 2.8rem; }   /* a targeted line (or predicate anchor) lands below the sticky bar */
.corpus { margin: 1.5rem 0 0; }   /* the Ledger page: the register's hits in the papers' ledgers, under the master's table */
.corpus h2 { font-size: .78rem; text-transform: uppercase; letter-spacing: .07em; color: var(--ink-faint); margin: 0 0 .6rem; }
.corpus ol { list-style: none; margin: 0; padding: 0; font-size: .88rem; }
.corpus li { padding: .3rem 0; border-top: 1px solid var(--rule); line-height: 1.45; }
.corpus li .snip { color: var(--ink-soft); }
.corpus + .legend { margin-top: 2rem; padding-top: 1.25rem; border-top: 1px solid var(--rule); }
table:not(.ledger) td.status { padding-left: .15rem; }   /* the Publications table: the badge's text starts under the header's text (the badge's own .55rem padding taken off the cell's .7rem) */
/* the Publications table's package column (25 Sept): four equal slots headed by the glyphs, the counts alone beneath them */
th.pkg .pkgrow, td.links.pkg .pkgrow { display: grid; grid-template-columns: repeat(4, 2.1rem); align-items: center; justify-items: center; column-gap: 0; }
th.pkg .g, td.links.pkg .g { display: inline-flex; justify-content: center; align-items: center; min-height: 22px; width: 100%; }
th.pkg .g .ico, .wrap th.pkg .g .ico { display: inline-flex; width: auto; height: auto; padding: 0; margin: 0; border: 0; background: none; }
th.pkg img.runico, th.pkg img.leanico { width: 16px; height: 16px; display: block; }
th.pkg .ico svg { width: 17px; height: 17px; stroke: var(--ink-soft); fill: none; stroke-width: 1.6; stroke-linecap: round; stroke-linejoin: round; }
.wrap td.links.pkg a.n, .wrap td.links.pkg a.n:visited { font-family: var(--mono); font-size: .85rem; line-height: 1; border: 0; background: none; padding: .1rem .15rem; width: 2ch; box-sizing: content-box; text-align: right; height: auto; text-decoration: none; margin: 0; }
.wrap td.links.pkg a.n.py.ok { color: #a27900; } .wrap td.links.pkg a.n.core { color: #419457; } .wrap td.links.pkg a.n.ml { color: #7974c6; } .wrap td.links.pkg a.n.py.fail { color: #c04a4a; }
.wrap td.links.pkg a.n:hover { background: var(--rule-soft); }
.wrap td.links.pkg a.ico.lab { width: 22px; height: 22px; margin: 0; }
td.links.pkg .g.legacy { grid-column: 1 / 4; justify-content: flex-start; gap: .2rem; }
@media (prefers-color-scheme: dark) { th.pkg img, .wrap td.links.pkg a.n { opacity: .9; } }
.pillrows .tally { margin-bottom: .55rem; }   /* the register view: three pill rows, each captioned */
.pillrows .tally:last-child { margin-bottom: 1.25rem; }
.pillrows .cap { font-size: .72rem; text-transform: uppercase; letter-spacing: .07em; color: var(--ink-faint); align-self: center; min-width: 3.4rem; }
details.filters { margin-bottom: .9rem; }   /* the register view: the pill rows behind one toggle, collapsed by default */
details.filters > summary { list-style: none; cursor: pointer; display: flex; flex-wrap: wrap; align-items: center; gap: .4rem .9rem; }
details.filters > summary::-webkit-details-marker { display: none; }
details.filters .tgl { font-size: .84rem; font-weight: 600; color: var(--ink-soft); padding: .3rem 0; display: inline-flex; align-items: center; gap: .5rem; transition: color .12s; }
details.filters > summary:hover .tgl, details.filters[open] .tgl { color: var(--ink); }
details.filters > summary:focus-visible { outline: none; } details.filters > summary:focus-visible .tgl { outline: 2px solid var(--accent); outline-offset: 2px; border-radius: 3px; }
details.filters .chev { width: .38rem; height: .38rem; border-right: 1.5px solid currentColor; border-bottom: 1.5px solid currentColor; transform: rotate(-45deg); margin: 0 .05rem 0 -.1rem; transition: transform .12s; }
details.filters[open] .chev { transform: translateY(-.12rem) rotate(45deg); }
details.filters .sel { display: inline-flex; flex-wrap: wrap; align-items: center; gap: .2rem .55rem; font-size: .84rem; color: var(--ink); }
details.filters .sel .cap { font-size: .68rem; text-transform: uppercase; letter-spacing: .07em; color: var(--ink-faint); margin-right: .35rem; }
details.filters .sel .grp { display: inline-flex; align-items: baseline; white-space: nowrap; }
details.filters .sel .dot { width: 8px; height: 8px; border-radius: 50%; display: inline-block; margin-right: .35rem; align-self: center; }
details.filters .sel .sep { color: var(--ink-faint); }
details.filters[open] .sel { display: none; }
details.filters[open] .pillrows { margin-top: .8rem; }
details.filters[open] .pillrows .tally:last-child { margin-bottom: .35rem; }
@media (max-width: 640px) { details.filters .sel .sep { display: none; } details.filters .sel { column-gap: 1.1rem; } }   /* a phone: the captions part the groups, no dot left at a line end (14 October 2026) */