/* Restrained research page with a compact section rail. */
:root {
  /* Palette from the LeanLean site. */
  --paper:#fbfcfc; --fg:#13202a; --muted:#475661; --faint:#76848e; --border:#e1e7ea; --soft:#f2f5f6;
  --accent:#1d5d74; --accent-soft:#e5eff3; --link:#1d5d74;
  --raw:#c9772e; --ours:#1d6fa5; --good:#2f7d4f;
  --role-review:#c3d6d6; --role-axiom:#e2cf9f; --role-result:#cfc3df; --role-helper:#c6d6b8;
  --code-kw:#7a3e9d; --code-decl:#1d5d74; --code-com:#526570; --code-str:#8a5a12;
  --sans:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif;
  --mono:"IBM Plex Mono",ui-monospace,Consolas,monospace;
  --small:.9rem; --code:.85rem;
  color-scheme:light;
}
*,*::before,*::after { box-sizing:border-box; }
html { -webkit-text-size-adjust:100%; scroll-behavior:smooth; }
body { margin:0; background:var(--paper); color:var(--fg); font:16px/1.6 var(--sans); }
[hidden] { display:none!important; }
a { color:var(--link); text-underline-offset:.15em; text-decoration-thickness:1px; }
:focus-visible { outline:2px solid var(--accent); outline-offset:2px; }
h1,h2,h3 { line-height:1.25; font-weight:600; }
h1 { font-size:2rem; font-weight:400; margin:0 0 .5rem; text-wrap:balance; }
h2 { font-size:1.5rem; margin:40px 0 12px; padding-bottom:4px; border-bottom:2px solid var(--accent); }
h3 { font-size:1.15rem; margin:28px 0 8px; }
h4 { font-size:1rem; margin:0; }
p { margin:0 0 12px; }
b,strong { font-weight:600; }
code,pre { font-family:var(--mono); }
:not(pre)>code { font-size:var(--code); background:var(--soft); padding:1px 4px; border-radius:4px; overflow-wrap:anywhere; }
button,input { font:inherit; color:inherit; }
table th, table td { vertical-align:middle; }
ul,ol { padding-left:24px; }
li { margin-bottom:4px; }

.skip-link { position:fixed; left:16px; top:-100px; z-index:60; background:var(--paper); padding:12px; }
.skip-link:focus { top:8px; }

/* Layout and section navigation */
.site-shell { max-width:1140px; margin:0 auto; padding:0 24px; display:grid; grid-template-columns:184px minmax(0,1fr); gap:32px; align-items:start; }
.page { max-width:880px; width:100%; min-width:0; margin:0 auto; padding:0 16px 64px; }
.sidebar { position:sticky; top:32px; margin-top:40px; height:calc(100vh - 72px); height:calc(100dvh - 72px); display:flex; flex-direction:column; overflow-y:auto; font-size:var(--small); line-height:1.5; }
.sidebar-toggle { display:none; }
.sidebar-content { display:flex; flex-direction:column; flex:1; min-height:0; }
.section-nav { display:grid; gap:4px; flex-shrink:0; }
.section-nav a { text-decoration:none; color:var(--muted); border-left:2px solid var(--border); padding:10px 12px; min-height:44px; }
.section-nav a:hover { color:var(--accent); background:var(--soft); }
.section-nav a[aria-current="location"] { color:var(--accent); background:var(--accent-soft); border-color:var(--accent); font-weight:600; }
.manuscript-link { display:block; margin-top:20px; padding:16px 0; border-top:1px solid var(--border); color:var(--link); }
.manuscript-link span { display:block; font-size:.85rem; }
.hero { text-align:center; padding:32px 0 0; }
.hero h1 { display:flex; align-items:center; justify-content:center; gap:.35em; font-size:2.5rem; margin-bottom:1rem; }
.hero .title-logo { width:1.2em; height:1.2em; flex:none; }
.hero p { margin:0; }
.hero p:not(.byline) { text-align:left; }
.hero p.tagline { font-size:1rem; color:var(--muted); text-align:center; }
.hero .byline { margin:12px auto 16px; font-size:var(--small); color:var(--muted); }
.byline a { white-space:nowrap; }
main>.section+.section>h2 { margin-top:48px; }
#good>h3 { margin-top:24px; }
#unit-distance h2 { margin-top:28px; }
.affil-logos { display:flex; flex-wrap:wrap; justify-content:center; align-items:center; gap:12px 40px; margin:12px 0; }
.affil-logos img { height:22px; width:auto; }
.sidebar .affil-logos { flex-direction:column; align-items:flex-start; gap:16px; flex-shrink:0; margin:auto 0 0; padding-top:20px; border-top:1px solid var(--border); }
.section, details[id] { scroll-margin-top:24px; }
.figure-note, .muted, figcaption { font-size:var(--small); color:var(--muted); }
.organization { font-size:var(--small); color:var(--muted); }
.corrections { display:grid; grid-template-columns:repeat(auto-fit,minmax(150px,1fr)); gap:12px; margin:16px 0; padding:0; text-align:center; }
.corrections>div { background:var(--accent-soft); border-radius:8px; padding:12px; display:grid; gap:2px; }
.corrections dd { color:var(--muted); font-size:var(--small); margin:0; }
.corrections dt { font-size:1.5rem; font-weight:600; }
.closing { margin:32px 0 0; }
@media (max-width:1119px) {
  .site-shell { grid-template-columns:140px minmax(0,1fr); gap:20px; padding:0 16px; }
}
@media (max-width:767px) {
  .site-shell { display:block; padding:0 20px; }
  .page { padding:0 0 48px; }
  .sidebar { position:relative; top:16px; margin:0; height:0; overflow:visible; z-index:40; }
  .sidebar-toggle { display:block; position:absolute; top:0; left:0; width:44px; min-height:44px; padding:4px; border:1px solid var(--border); border-radius:4px; background:var(--paper); color:var(--accent); font-size:1.25rem; cursor:pointer; }
  .sidebar-content { display:none; position:fixed; left:20px; top:68px; max-height:calc(100dvh - 84px); width:min(280px,calc(100vw - 40px)); padding:12px; background:var(--paper); border:1px solid var(--border); border-radius:6px; box-shadow:0 6px 18px #13202a14; overflow-y:auto; }
  .sidebar-toggle[aria-expanded="true"] + .sidebar-content { display:flex; }
  .sidebar .affil-logos { margin-top:16px; padding-top:12px; gap:12px; }
  .hero { padding-top:20px; }
  .hero h1 { margin-left:56px; font-size:2rem; }
  .hero .byline { margin-top:16px; }
}

/* Figures and code */
.figure { margin:16px 0; display:grid; gap:8px; }
.figure-frame { overflow:auto; }
.figure-frame img { display:block; width:100%; min-width:40rem; height:auto; }
.scroll-cue { display:none; color:var(--muted); font-size:var(--small); }
@media (max-width:671px) { .scroll-cue { display:block; } }
.tok-kw { color:var(--code-kw); } .tok-decl { color:var(--code-decl); }
.tok-com { color:var(--code-com); font-style:italic; } .tok-str { color:var(--code-str); } .tok-marker { color:var(--code-com); }

/* Disclosures */
details.more { margin:12px 0; }
details.more>summary { cursor:pointer; font-weight:600; color:var(--link); padding:9px 0; border-bottom:1px solid var(--border); }
details.more>summary:hover { color:var(--fg); }
details.more[open]>summary { border-bottom-color:var(--accent); }
.disclosure-body { padding:8px 0 0; min-width:0; }

/* Proof correspondence is assessed separately from code size. */
.faithfulness-summary { margin:16px 0; }
.faithfulness-table { min-width:620px; width:100%; border-collapse:collapse; font-size:var(--small); }
.faithfulness-table th, .faithfulness-table td { padding:10px 8px; border-bottom:1px solid var(--border); text-align:left; vertical-align:middle; }
.faithfulness-table thead th, .source-size-counts thead th { background:var(--soft); }
.faithfulness-table th:first-child { text-align:left; font-weight:400; }
.faithfulness-pass { color:var(--good); }
.faithfulness-fail { color:#b42332; }
.faithfulness-fail a { color:inherit; }
.faithfulness-table .finding-context { display:block; margin-top:3px; color:var(--muted); }
#ns-findings .faithfulness-fail .finding-context,
#qr-findings .faithfulness-fail .finding-context { color:inherit; }

/* Charts */
#chart-complexity, .minimality-legend { --raw:#D95F68; --ours:#3E8FC4; }
.chart-direction { text-align:center; font-weight:600; }
.legend { display:flex; flex-wrap:wrap; justify-content:center; gap:6px 18px; font-size:var(--small); color:var(--muted); margin:12px 0; }
.legend span { display:inline-flex; align-items:center; gap:6px; }
.swatch { width:12px; height:12px; border-radius:3px; display:inline-block; flex:none; }
.chart-row { display:grid; grid-template-columns:repeat(auto-fit,minmax(min(100%,16rem),1fr)); gap:24px 32px; margin:0 0 12px; }
/* Plots sit at the bottom of each panel so baselines line up across a row. */
.chart-panel { display:flex; flex-direction:column; gap:10px; min-width:0; text-align:center; }
.chart-panel .cols { margin:auto auto 0; width:100%; }
/* Column charts: labels need headroom above the tallest column (top padding). */
.cols { display:grid; grid-template-columns:repeat(2,minmax(0,1fr)); gap:16px; max-width:22rem; }
.col-group { display:grid; gap:6px; }
.col-group>.g { font-size:var(--small); color:var(--muted); text-align:center; }
.plot { display:flex; justify-content:center; align-items:stretch; gap:6px; height:200px; padding-top:3.4rem; border-bottom:1px solid var(--border); }
.col { position:relative; width:3.25rem; }
.col .fill { position:absolute; left:0; right:0; bottom:0; min-height:2px; border-radius:4px 4px 0 0; }
.col.raw .fill { background:var(--raw); }
.col.ours .fill { background:var(--ours); }
.col.other .fill { background:var(--faint); }
.col .val { position:absolute; left:50%; transform:translateX(-50%); padding-bottom:4px; display:grid; text-align:center; font-size:var(--small); line-height:1.3; font-variant-numeric:tabular-nums; white-space:nowrap; }
.delta { color:var(--good); }
/* Extra annotation headroom preserves the existing bars and zero baseline. */
#chart-complexity .plot { height:224px; padding-top:calc(3.4rem + 24px); }
#chart-complexity .reduction { position:absolute; right:50%; width:calc(100% + 6px); border-top:1.5px solid; border-right:1.5px solid; color:var(--accent); pointer-events:none; }
#chart-complexity .reduction strong { position:absolute; bottom:calc(100% + 6px); left:50%; transform:translateX(-50%); font-size:var(--small); line-height:1.3; white-space:nowrap; }
#chart-complexity .reduction::before { content:""; position:absolute; top:0; left:0; height:8px; border-left:1.5px solid; }
#chart-complexity .reduction::after { content:""; position:absolute; right:-4px; bottom:1px; width:7px; height:7px; border-right:1.5px solid; border-bottom:1.5px solid; transform:rotate(45deg); }




/* All unbroken segments share a scale; oversized outside segments are capped. */
.source-size-chart { margin:16px 0; display:grid; gap:4px; min-width:0; }
.source-size-chart > .source-size-notes { margin-top:6px; }
.source-size-label { display:flex; flex-wrap:wrap; justify-content:space-between; gap:4px 16px; margin:0 0 6px; font-size:var(--small); font-variant-numeric:tabular-nums; }
.source-size-plot { display:grid; grid-template-columns:minmax(0,4fr) auto minmax(0,1fr); gap:8px; align-items:center; }
.source-size-track { display:flex; height:16px; width:100%; }
.source-size-segment { flex:none; height:100%; }
.source-size-break { color:var(--muted); line-height:1; }
.source-size-table { overflow-x:auto; min-width:0; max-width:100%; overscroll-behavior-x:contain; }
#audit-findings .source-size-table { max-height:60vh; overflow-y:auto; scrollbar-gutter:stable; }
#audit-findings thead th { position:sticky; top:0; z-index:1; background:var(--paper); }
@media print {
  #audit-findings .source-size-table { max-height:none; overflow:visible; }
  #audit-findings thead th { position:static; }
}
.source-size-counts { min-width:620px; width:100%; border-collapse:collapse; font-size:var(--small); font-variant-numeric:tabular-nums; }
/* Shared column widths align the faithfulness and LoC comparisons. */
.faithfulness-table, .source-size-counts { table-layout:fixed; }
.faithfulness-table th:first-child, .source-size-counts th:first-child { width:32%; }
.faithfulness-table thead th, .source-size-counts thead th { overflow-wrap:anywhere; }
.source-size-counts caption { text-align:left; color:var(--muted); }
.source-size-counts th, .source-size-counts td { padding:7px 8px; border-bottom:1px solid var(--border); text-align:right; }
.source-size-counts th:first-child { text-align:left; font-weight:400; }
.faithfulness-table:not(.audit-table) thead th:nth-child(4), .source-size-counts thead th:nth-child(4) { width:9.5rem; white-space:nowrap; }
/* Table 1 reserves width for explanations rather than sparse verdicts. */
.faithfulness-summary .faithfulness-table { min-width:720px; }
.faithfulness-summary .faithfulness-table th:first-child { width:16%; }
.faithfulness-summary .faithfulness-table thead th:nth-child(2) { width:12%; }
.faithfulness-summary .faithfulness-table thead th:nth-child(3) { width:22%; }
.faithfulness-summary .faithfulness-table thead th:nth-child(4) { width:30%; }
.faithfulness-summary .faithfulness-table thead th:nth-child(5) { width:20%; }
.faithfulness-summary .finding-context + br { display:none; }
.faithfulness-summary .finding-context + br + a { display:inline-block; margin-top:6px; }
.source-size-counts tbody tr:last-child { border-top:2px solid var(--border); font-weight:600; }
.source-size-counts tbody tr:last-child th { font-weight:600; }
.source-size-counts .source-size-subtotal > * { font-weight:600; }
.source-size-counts .swatch { vertical-align:middle; }
.source-size-footnote { margin:0; font-size:var(--small); line-height:1.5; color:var(--muted); }
.source-size-chart .figure-note { margin:0; }
.source-size-counts a { position:relative; }
.source-size-counts a::after { content:""; position:absolute; inset:-5px -10px; }
.source-size-counts tr > :last-child a::after { right:-3px; }
.source-size-chart sup a { text-decoration:none; }
.source-size-notes { margin:0; padding-left:1.5em; font-size:var(--small); line-height:1.5; color:var(--muted); }
.source-size-notes li { margin:0 0 6px; }
.source-size-chart details.more { margin:0; font-size:var(--small); }
.source-size-chart details p { margin:8px 0; }

.scope-note { color:var(--muted); font-size:var(--small); }

/* File explorer */
.file-search { display:flex; flex-wrap:wrap; align-items:center; gap:8px; margin:0 0 8px; }
.file-search input { padding:6px 10px; border:1px solid var(--border); border-radius:6px; flex:1 1 12rem; min-width:0; max-width:20rem; }
.explorer { display:grid; grid-template-columns:minmax(0,1fr); gap:12px; }
.explorer-reference { display:flex; flex-direction:column; gap:16px; min-width:0; min-height:0; }
@media (min-width:800px) {
  .explorer { grid-template-columns:minmax(16rem,.9fr) minmax(0,1.5fr); height:400px; }
  .explorer.has-statement { height:560px; }
  .explorer-reference .tree { flex:1; }
  .has-statement .explorer-reference .tree { flex:0 0 160px; }
}
.tree { background:var(--soft); border-radius:6px; padding:8px 4px; overflow:auto; max-height:160px; }
@media (min-width:800px) { .tree { max-height:none; } }
.tree ul { list-style:none; padding-left:12px; margin:0; }
.tree>ul { padding-left:0; }
.tree li { margin:0; }
.tree .dir { font:var(--code)/1.9 var(--mono); color:var(--muted); padding-left:8px; }
.tree button { all:unset; box-sizing:border-box; display:flex; align-items:center; gap:8px; width:100%; cursor:pointer; padding:2px 8px; border-radius:4px; font:var(--code)/1.6 var(--mono); }
.tree button:hover { background:var(--border); }
.tree button:focus-visible { outline:2px solid var(--accent); outline-offset:-2px; }
.tree button[aria-current="true"] { background:var(--accent-soft); color:var(--accent); }
.tree button i { width:8px; height:8px; border-radius:2px; flex:none; }
.tree button .file-name { flex:1; min-width:0; overflow-wrap:anywhere; }
.tree button .n { margin-left:auto; color:var(--muted); font: .8rem/1.7 var(--sans); white-space:nowrap; align-self:flex-start; }
.paper-statement { min-height:0; max-height:360px; overflow:auto; padding:12px 4px 0 0; border-top:1px solid var(--border); font-size:var(--small); }
.paper-statement h4 { margin-bottom:8px; }
.paper-statement p { margin:0 0 10px; overflow-wrap:anywhere; }
.paper-statement .paper-formula { white-space:pre-wrap; }
.paper-statement .paper-source { color:var(--muted); }
.paper-statement .katex { font-size:1.05em; }
.paper-statement .katex-display { margin:10px 0; max-width:100%; overflow-x:auto; overflow-y:hidden; padding:2px 0; }

.viewer { display:grid; grid-template-rows:auto minmax(0,1fr); min-width:0; min-height:0; background:var(--soft); border-radius:6px; }
.viewer-bar { border-bottom:1px solid var(--border); display:flex; flex-wrap:wrap; align-items:center; justify-content:space-between; gap:4px 16px; padding:8px 12px; font-size:var(--small); }
.viewer-bar .path { font-family:var(--mono); font-size:var(--code); overflow-wrap:anywhere; }
.viewer-bar .role { color:var(--muted); }
.toggle { display:inline-flex; align-items:center; gap:6px; color:var(--muted); cursor:pointer; user-select:none; }
.toggle input { accent-color:var(--accent); }
.viewer pre { margin:0; padding:4px 0 12px; overflow:auto; font-size:var(--code); line-height:1.6; height:320px; min-height:0; max-height:320px; }
@media (min-width:800px) { .viewer pre { height:auto; max-height:none; } }
@media (max-width:600px) { .viewer pre { height:288px; max-height:288px; } }
.viewer .ln { display:block; padding-right:16px; white-space:pre; }
.viewer .ln::before { content:attr(data-n); display:inline-block; width:3.2em; padding-right:1em; text-align:right; color:var(--muted); user-select:none; }
.viewer .ln.folded { color:var(--muted); font-style:italic; background:var(--border); }


@media (prefers-reduced-motion:reduce) { html { scroll-behavior:auto; } }