/* Layout: one 1120px column like the RRSI page. Solved problems lead; each opens a dossier with problem, informal proof, Lean proof and proof DAG. */
:root{
  color-scheme:light;
  --bg:#f8f8f6;--surface:#ffffff;--surface-2:#f1f1ed;--ink:#141619;--ink-2:#3b4148;--muted:#6b7178;
  --line:#e3e2dc;--line-2:#cfcec6;--accent:#2a78d6;--accent-ink:#1c5cab;--accent-soft:#e3eefb;--accent-2:#86b6ef;
  --pos:#008300;--pos-soft:#e6f4e6;--warn:#c98500;--warn-soft:#fff3d6;--del-bg:#fdecec;--del:#cf222e;
  --c1:#2a78d6;--c2:#14907c;--c3:#7c4fd0;--c4:#c8761f;--c5:#c23f69;--c6:#4f8a22;--c7:#2b8fb8;--c8:#a8841c;
  --sans:"Inter",system-ui,-apple-system,"Segoe UI",Roboto,Helvetica,Arial,sans-serif;
  --mono:"JetBrains Mono",ui-monospace,SFMono-Regular,Menlo,Consolas,monospace;
}
@media (prefers-color-scheme:dark){:root:not([data-theme="light"]){
  color-scheme:dark;
  --bg:#0f1214;--surface:#171b1f;--surface-2:#1e2328;--ink:#e9ebee;--ink-2:#b5bcc4;--muted:#818a94;
  --line:#272d33;--line-2:#363d45;--accent:#3987e5;--accent-ink:#7db4f5;--accent-soft:#14263d;--accent-2:#2f66ad;
  --pos:#3fb950;--pos-soft:#12251a;--warn:#d9a441;--warn-soft:#2f2711;--del-bg:#2a1416;--del:#f85149;
  --c1:#5a9be8;--c2:#3cc4ab;--c3:#a989ea;--c4:#e7a053;--c5:#e0708f;--c6:#87bd52;--c7:#63bde3;--c8:#d6b54d;
}}
:root[data-theme="dark"]{
  color-scheme:dark;
  --bg:#0f1214;--surface:#171b1f;--surface-2:#1e2328;--ink:#e9ebee;--ink-2:#b5bcc4;--muted:#818a94;
  --line:#272d33;--line-2:#363d45;--accent:#3987e5;--accent-ink:#7db4f5;--accent-soft:#14263d;--accent-2:#2f66ad;
  --pos:#3fb950;--pos-soft:#12251a;--warn:#d9a441;--warn-soft:#2f2711;--del-bg:#2a1416;--del:#f85149;
  --c1:#5a9be8;--c2:#3cc4ab;--c3:#a989ea;--c4:#e7a053;--c5:#e0708f;--c6:#87bd52;--c7:#63bde3;--c8:#d6b54d;
}
*{box-sizing:border-box}
[hidden]{display:none!important}
html{scroll-behavior:smooth}
@media (prefers-reduced-motion:reduce){html{scroll-behavior:auto}}
body{background:var(--bg);color:var(--ink);font:15px/1.6 var(--sans);-webkit-font-smoothing:antialiased}
a{color:var(--accent-ink)}
code,.mono{font-family:var(--mono)}
code{font-size:.88em;background:var(--surface-2);padding:1px 5px;border-radius:4px}
button{font:inherit;color:inherit}
:focus-visible{outline:2px solid var(--accent);outline-offset:2px}
.wrap{max-width:1120px;margin:0 auto;padding-inline:20px}

/* nav */
.nav{position:sticky;top:env(safe-area-inset-top,0px);z-index:20;background:color-mix(in srgb,var(--bg) 88%,transparent);backdrop-filter:blur(8px);border-bottom:1px solid var(--line)}
.nav .wrap{display:flex;align-items:center;gap:20px;height:52px}
.brand{font-weight:800;font-size:22px;letter-spacing:.04em;line-height:1;text-decoration:none;color:var(--ink)}
.nav nav{margin-left:auto;display:flex;gap:18px;align-items:center;overflow-x:auto}
.nav nav a{color:var(--ink-2);text-decoration:none;font-size:13px;white-space:nowrap}
.nav nav a:hover{color:var(--ink)}
.theme-btn{border:1px solid var(--line-2);background:var(--surface);border-radius:999px;padding:3px 10px;font:500 10px/1.6 var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--ink-2);cursor:pointer;white-space:nowrap}
@media (max-width:640px){.nav nav a.opt{display:none}}

/* hero */
.hero{padding-block:56px 40px}
.kicker{font:500 11px/1.4 var(--mono);letter-spacing:.16em;text-transform:uppercase;color:var(--muted)}
.hero .kicker{color:var(--accent-ink)}
h1{font-size:clamp(30px,5vw,48px);line-height:1.08;font-weight:800;letter-spacing:-.025em;margin:14px 0 16px;text-wrap:balance;max-width:18em}
.lede{font-size:clamp(16px,2vw,19px);color:var(--ink-2);max-width:42em;margin:0 0 20px}
.authors{font-size:13.5px;color:var(--ink-2);max-width:60em;margin:0}
.affil{font-size:12px;color:var(--muted);margin:6px 0 0}
.btns{display:flex;flex-wrap:wrap;gap:10px;margin:24px 0 34px}
.btn{display:inline-flex;align-items:center;gap:8px;padding:8px 14px;border:1px solid var(--line-2);border-radius:8px;background:var(--surface);color:var(--ink);text-decoration:none;font-size:13px;font-weight:500;cursor:pointer}
.btn:hover{border-color:var(--muted)}
.btn.primary{background:var(--accent);border-color:var(--accent);color:#fff}
.btn svg{width:14px;height:14px;flex:none}
.tiles{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:12px}
@media (max-width:860px){.tiles{grid-template-columns:repeat(2,minmax(0,1fr))}}
.tile{border:1px solid var(--line);background:var(--surface);border-radius:10px;padding:16px}
.tile .v{font:600 26px/1.1 var(--mono);color:var(--accent-ink);font-variant-numeric:tabular-nums}
.tile .v small{font-size:12px;color:var(--muted);font-weight:500;margin-left:4px}
.tile p{margin:8px 0 0;font-size:13px;color:var(--ink-2);line-height:1.45}

/* sections */
section.sec{padding-block:56px;border-top:1px solid var(--line)}
h2{font-size:clamp(22px,3vw,30px);line-height:1.2;font-weight:700;letter-spacing:-.015em;margin:10px 0 12px;text-wrap:balance;max-width:26em}
p.intro{color:var(--ink-2);max-width:46em;margin:0 0 26px}
h3.sub{font:500 11px var(--mono);letter-spacing:.14em;text-transform:uppercase;color:var(--muted);margin:36px 0 12px}

/* featured */
.feat{display:grid;grid-template-columns:repeat(3,minmax(0,1fr));gap:14px}
@media (max-width:900px){.feat{grid-template-columns:1fr}}
.fcard{position:relative;display:flex;flex-direction:column;border:1px solid var(--line);background:var(--surface);border-radius:14px;overflow:hidden;text-align:left;cursor:pointer;padding:0;min-width:0;transition:border-color .15s,transform .15s}
.fcard:hover{border-color:var(--accent);transform:translateY(-2px)}
@media (prefers-reduced-motion:reduce){.fcard,.fcard:hover{transition:none;transform:none}}
.fcard canvas{display:block;width:100%;height:112px;background:var(--surface-2);border-bottom:1px solid var(--line)}
.fcard .fb{padding:16px 18px 18px;display:flex;flex-direction:column;gap:6px;flex:1}
.fcard .fa{font:500 10.5px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--muted)}
.fcard .ft{font-size:20px;font-weight:700;letter-spacing:-.01em;line-height:1.2;text-wrap:balance}
.fcard .fs{font-size:13px;color:var(--muted)}
.fcard .fsum{font-size:13.5px;color:var(--ink-2);line-height:1.5;margin:4px 0 0}
.fcard .ff{margin-top:auto;padding-top:12px;display:flex;align-items:baseline;justify-content:space-between;gap:10px}
.fcard .loc{font:600 22px var(--mono);color:var(--accent-ink);font-variant-numeric:tabular-nums}
.fcard .loc small{font-size:11px;color:var(--muted);font-weight:500;margin-left:4px}
.fcard .go{font-size:13px;font-weight:600;color:var(--accent-ink);white-space:nowrap}
.fcard .cr{font:11px var(--mono);color:var(--muted)}

/* problems table */
.ptools{display:flex;flex-wrap:wrap;gap:10px;align-items:center;margin:0 0 12px}
.chips{display:flex;flex-wrap:wrap;gap:6px}
.chip{border:1px solid var(--line-2);background:var(--surface);border-radius:999px;padding:4px 11px;font-size:12px;cursor:pointer;color:var(--ink-2)}
.chip[aria-pressed="true"]{background:var(--ink);border-color:var(--ink);color:var(--bg)}
.inp{border:1px solid var(--line-2);background:var(--surface);border-radius:8px;padding:6px 10px;font:13px var(--sans);color:var(--ink);min-width:0}
.ptools .inp{margin-left:auto;width:220px}
@media (max-width:640px){.ptools .inp{margin-left:0;width:100%}}
.ptable{border:1px solid var(--line);border-radius:10px;background:var(--surface);overflow:hidden}
.tscroll{overflow-x:auto}
.ptable table{width:100%;border-collapse:collapse}
.ptable th{font:500 10.5px var(--mono);letter-spacing:.1em;text-transform:uppercase;color:var(--muted);text-align:left;padding:10px 14px;border-bottom:1px solid var(--line-2);background:var(--surface-2);white-space:nowrap}
.prow{cursor:pointer}
.prow td{padding:13px 14px;border-top:1px solid var(--line);vertical-align:top;font-size:13.5px}
.prow:first-child td{border-top:0}
.prow:hover td{background:var(--surface-2)}
.prow .pt{font-weight:600;color:var(--ink)}
.pv{font:500 11.5px var(--mono);color:var(--muted);margin-left:8px;letter-spacing:0}
.mk{color:var(--warn);font-weight:700;margin-left:2px}
.prow .ps{color:var(--muted);font-size:12.5px;margin-top:2px;max-width:60ch}
.prow .num{font:500 12.5px var(--mono);white-space:nowrap;font-variant-numeric:tabular-nums}
.prow .car{width:28px;color:var(--muted)}
.car svg{width:14px;height:14px;transition:transform .15s}
.prow[aria-expanded="true"] .car svg{transform:rotate(90deg)}
.avail{display:flex;gap:4px}
.av{font:600 10px/1.7 var(--mono);padding:0 6px;border-radius:4px;border:1px solid var(--line-2);color:var(--muted)}
.av.on{color:var(--pos);border-color:color-mix(in srgb,var(--pos) 45%,transparent);background:var(--pos-soft)}
.star{color:var(--warn);font-size:12px;margin-right:4px}
.pdet td{padding:0 14px 16px 56px;background:var(--surface)}
.pdet p{margin:0 0 10px;font-size:14px;color:var(--ink-2);max-width:68ch}
.pdet .btns{margin:8px 0 0}
.tfoot{font-size:12px;color:var(--muted);margin:10px 0 0}
@media (max-width:640px){.hide-sm{display:none}.pdet td{padding-left:14px}}
pre.lean{margin:0;background:var(--surface-2);border:1px solid var(--line);border-radius:8px;padding:12px;overflow-x:auto;font:12.5px/1.55 var(--mono);color:var(--ink)}
.todo{display:inline-block;font:600 10px/1.6 var(--mono);letter-spacing:.08em;color:var(--warn);background:var(--warn-soft);border-radius:4px;padding:0 6px;margin-right:6px;vertical-align:1px}
.err{border:1px solid var(--del);background:var(--del-bg);color:var(--del);border-radius:10px;padding:14px;font-size:13.5px}

/* dossier */
.dpick{display:flex;flex-wrap:wrap;gap:8px;align-items:center;margin-bottom:22px}
.dpick select{border:1px solid var(--line-2);background:var(--surface);color:var(--ink);border-radius:8px;padding:7px 10px;font:13.5px var(--sans);max-width:100%}
.dpick .btn{padding:6px 10px}
.dhead{display:grid;grid-template-columns:minmax(0,1fr) auto;gap:20px;align-items:start}
@media (max-width:760px){.dhead{grid-template-columns:1fr}}
.dhead h2{margin:0;font-size:clamp(26px,3.6vw,36px);max-width:none}
.dhead .dsub{color:var(--muted);font-size:15px;margin:4px 0 0}
.dbadges{display:flex;flex-wrap:wrap;gap:6px;margin-top:12px}
.dstat{text-align:right}
@media (max-width:760px){.dstat{text-align:left}}
.dstat .loc{font:600 34px/1 var(--mono);color:var(--accent-ink);font-variant-numeric:tabular-nums}
.dstat .lbl{font-size:12px;color:var(--muted);margin-top:4px}
.dbody{display:grid;grid-template-columns:minmax(0,1fr) 300px;gap:28px;margin-top:22px}
@media (max-width:860px){.dbody{grid-template-columns:1fr}}
.dbody .prob{min-width:0}
.dbody .prob p{font-size:15.5px;color:var(--ink);max-width:66ch;margin:0 0 12px;line-height:1.65}
.stmt{border:1px solid var(--line);background:var(--surface);border-radius:10px;padding:16px 18px;font:500 15px/1.6 var(--mono);color:var(--ink);overflow-x:auto;margin:4px 0 14px;white-space:pre-wrap}
.note{border:1px solid var(--line);border-radius:10px;background:var(--surface);padding:12px 14px;margin:0 0 10px}
.note h4{font:600 10.5px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--muted);margin:0 0 6px}
.note.todo-n h4{color:var(--warn)}
.note p{margin:0;font-size:13.5px;color:var(--ink-2)}
.dside{border:1px solid var(--line);border-radius:12px;background:var(--surface);padding:16px;align-self:start;min-width:0}
.dside h4{font:500 10.5px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--muted);margin:0 0 10px}
.dside .kv{margin-bottom:14px}
.dside .btn{width:100%;justify-content:center;margin-top:6px}
.kv{display:grid;grid-template-columns:auto 1fr;gap:6px 14px;font-size:13px;margin:0}
.kv dt{color:var(--muted)}
.kv dd{margin:0;font-family:var(--mono);font-size:12.5px;color:var(--ink);overflow-wrap:anywhere}
.stabs{display:flex;gap:2px;border-bottom:1px solid var(--line);margin:36px 0 18px;overflow-x:auto}
.stab{all:unset;cursor:pointer;padding:10px 14px;font-size:14px;font-weight:600;color:var(--muted);border-bottom:2px solid transparent;margin-bottom:-1px;white-space:nowrap}
.stab:hover{color:var(--ink)}
.stab[aria-selected="true"]{color:var(--ink);border-color:var(--accent)}
.stab:focus-visible{outline:2px solid var(--accent)}
.stab .n{font:500 11px var(--mono);color:var(--muted);margin-left:6px}
.empty{border:1px dashed var(--line-2);border-radius:12px;padding:28px;text-align:center;color:var(--muted);font-size:14px}
.empty b{display:block;color:var(--ink);font-size:15px;margin-bottom:4px}
.empty code{font-size:12px}
.isec h4{font-size:16px;margin:18px 0 6px}
.isec p{max-width:68ch;color:var(--ink-2);margin:0 0 10px}

/* explorer */
.vtabs{display:flex;gap:6px}
.parts{display:flex;align-items:center;gap:10px;flex-wrap:wrap;margin:0 0 14px;font-size:12.5px;color:var(--muted)}
.parts[hidden]{display:none}
.vtab{border:1px solid var(--line-2);background:var(--surface);border-radius:8px;padding:5px 12px;font-size:12.5px;font-weight:600;color:var(--ink-2);cursor:pointer}
.vtab[aria-selected="true"]{background:var(--ink);border-color:var(--ink);color:var(--bg)}
.xbox{border:1px solid var(--line);border-radius:12px;background:var(--surface);overflow:hidden}
.xbar{display:flex;flex-wrap:wrap;gap:10px;align-items:center;padding:10px 12px;border-bottom:1px solid var(--line);background:var(--surface-2)}
.xbar label{font-size:12px;color:var(--muted);display:flex;align-items:center;gap:6px}
.xbar .inp{padding:4px 8px;font-size:12.5px;width:200px}
.xbar .sp{flex:1}
.xstats{font:500 11.5px var(--mono);color:var(--muted);padding:8px 12px;border-bottom:1px solid var(--line);display:flex;flex-wrap:wrap;gap:4px 16px;font-variant-numeric:tabular-nums}
.xstats b{color:var(--ink);font-weight:600}
.sample{color:var(--warn)}
.xmain{display:grid;grid-template-columns:minmax(0,1fr) 340px}
@media (max-width:900px){.xmain{grid-template-columns:1fr}}
.stage{position:relative;height:620px;min-width:0;border-right:1px solid var(--line);overflow:hidden}
@media (max-width:900px){.stage{height:500px;border-right:0;border-bottom:1px solid var(--line)}}
.stage canvas#cv{position:absolute;inset:0;touch-action:none;background-image:radial-gradient(var(--line) 1px,transparent 1px);background-size:22px 22px}
.stage .pane{position:absolute;inset:0;overflow:auto;background:var(--surface)}
.zoomctl{position:absolute;right:10px;top:10px;display:flex;flex-direction:column;gap:4px;z-index:3}
.zoomctl button,.dtools button{border:1px solid var(--line-2);background:var(--surface);border-radius:6px;cursor:pointer;color:var(--ink-2)}
.zoomctl button{width:30px;height:30px;font:600 14px var(--mono)}
.dtools{position:absolute;left:10px;top:10px;z-index:3;display:flex;gap:6px;flex-wrap:wrap}
.dtools button{padding:4px 9px;font:12px var(--sans)}
.dtools button:hover,.zoomctl button:hover{border-color:var(--muted)}
#mini{position:absolute;right:10px;bottom:10px;width:200px;height:100px;border:1px solid var(--line-2);border-radius:8px;background:var(--surface);z-index:3;cursor:pointer;touch-action:none}
@media (max-width:640px){#mini{display:none}}
.hint{position:absolute;left:12px;bottom:10px;font:11px var(--mono);color:var(--muted);z-index:3;pointer-events:none;background:color-mix(in srgb,var(--surface) 85%,transparent);padding:2px 6px;border-radius:4px}
.legend{display:flex;flex-wrap:wrap;gap:6px 16px;padding:8px 12px;border-top:1px solid var(--line);font-size:12px;color:var(--ink-2)}
.legend i{display:inline-block;width:10px;height:10px;border-radius:50%;margin-right:6px;vertical-align:-1px}
.legend i.sq{border-radius:3px}

/* side panel */
.side{padding:14px 16px;overflow:auto;max-height:620px;min-width:0}
@media (max-width:900px){.side{max-height:none}}
.side .nm{font:600 13.5px/1.4 var(--mono);word-break:break-all;margin:6px 0 8px}
.side h5{font:500 10.5px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--muted);margin:16px 0 6px}
.side pre.lean{font-size:11.5px;padding:10px}
.badges{display:flex;flex-wrap:wrap;gap:6px}
.bdg{font:500 11px/1.6 var(--mono);padding:0 7px;border-radius:4px;background:var(--surface-2);color:var(--ink-2);border:1px solid var(--line);white-space:nowrap}
.bdg.leaf{color:var(--pos);background:var(--pos-soft);border-color:transparent}
.bdg.ab{color:var(--del);background:var(--del-bg);border-color:transparent}
.bdg.sh{color:var(--warn);background:var(--warn-soft);border-color:transparent}
.bdg.acc{color:var(--accent-ink);background:var(--accent-soft);border-color:transparent}
.nlist{list-style:none;margin:0;padding:0;display:grid;gap:2px}
.nlist button{all:unset;box-sizing:border-box;display:block;width:100%;font:12px/1.5 var(--mono);color:var(--accent-ink);cursor:pointer;padding:2px 4px;border-radius:4px;word-break:break-all}
.nlist button:hover{background:var(--surface-2)}
.nlist button:focus-visible{outline:2px solid var(--accent)}
.nlist .ab{color:var(--muted);text-decoration:line-through}

/* outline */
.ohead{position:sticky;top:0;z-index:2;display:flex;gap:10px;padding:6px 12px;font:500 10px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--muted);background:var(--surface-2);border-bottom:1px solid var(--line)}
.ohead span:first-child{flex:1}
.orow{display:flex;align-items:stretch;gap:6px;padding:0 12px 0 4px;cursor:pointer;min-height:40px}
.orow:hover{background:var(--surface-2)}
.orow.sel{background:var(--accent-soft)}
.orow .ig{width:9px;margin-left:7px;border-left:1px solid var(--line-2);flex:none}
.orow .tg{all:unset;width:18px;text-align:center;color:var(--muted);cursor:pointer;flex:none;align-self:center;font-size:11px}
.orow .tg[disabled]{visibility:hidden}
.orow .dot{width:9px;height:9px;border-radius:50%;flex:none;align-self:center}
.orow .dot.comp{background:transparent!important;border:2.5px solid}
.oc{display:flex;flex-direction:column;justify-content:center;min-width:0;flex:1;padding:4px 0}
.oc .on{font:600 12.5px/1.35 var(--mono);color:var(--ink);overflow:hidden;text-overflow:ellipsis;white-space:nowrap}
.oc .os{font:11px/1.35 var(--mono);color:var(--muted);overflow:hidden;text-overflow:ellipsis;white-space:nowrap}
.orow.ab .on{color:var(--muted);text-decoration:line-through}
.orow.match .on{color:var(--warn)}
.orow .bdg{align-self:center}
.obar{width:64px;height:6px;background:var(--surface-2);border-radius:3px;flex:none;align-self:center;overflow:hidden}
.orow:hover .obar,.orow.sel .obar{background:var(--line)}
.obar i{display:block;height:100%;border-radius:3px}
.orow .om{width:140px;text-align:right;flex:none;align-self:center;font:11.5px var(--mono);color:var(--muted);font-variant-numeric:tabular-nums}
@media (max-width:640px){.obar,.ohead .hb{display:none}.orow .om{width:auto}}

/* lean code */
.lk{color:var(--c3)}.lt{color:var(--c2)}.ly{color:var(--c4)}.ln{color:var(--c5)}.lc{color:var(--muted);font-style:italic}.lself{font-weight:700;color:var(--ink)}
.ll{all:unset;color:var(--accent-ink);text-decoration:underline dotted;text-underline-offset:3px;cursor:pointer}
.ll:hover{background:var(--accent-soft)}
span.ll{cursor:default}

/* hover card */
.pop{position:fixed;z-index:60;width:min(470px,calc(100vw - 24px));background:var(--surface);border:1px solid var(--line-2);border-radius:12px;box-shadow:0 18px 44px rgba(0,0,0,.22);padding:12px 12px 10px;pointer-events:none}
.pop-h{display:flex;flex-wrap:wrap;align-items:center;gap:6px;margin-bottom:8px}
.pop-n{font:600 13px var(--mono);word-break:break-all;margin-right:4px}
.pop-l{font:500 10px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--muted);margin:0 0 5px}
.pop pre.lean{font-size:11.5px;padding:10px;white-space:pre;overflow:hidden}
.pop-r{font-size:12px;color:var(--del);margin-top:8px}
.pop-f{font:10.5px var(--mono);color:var(--warn);margin-top:8px}

/* how it works */
.steps{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:12px}
@media (max-width:860px){.steps{grid-template-columns:repeat(2,minmax(0,1fr))}}
@media (max-width:520px){.steps{grid-template-columns:1fr}}
.step{border:1px solid var(--line);background:var(--surface);border-radius:10px;padding:16px;min-width:0}
.step .n{font:500 11px var(--mono);color:var(--muted);letter-spacing:.1em}
.step h4{font-size:15px;margin:6px 0 6px}
.step p{margin:0;font-size:13px;color:var(--ink-2);line-height:1.5}
.tracks{display:grid;grid-template-columns:repeat(3,minmax(0,1fr));gap:12px;margin-top:14px}
@media (max-width:760px){.tracks{grid-template-columns:1fr}}
.track{border:1px solid var(--line);border-radius:10px;padding:16px;background:var(--surface);text-decoration:none;color:inherit;display:block}
.track:hover{border-color:var(--accent)}
.track .tn{font:600 11px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--accent-ink)}
.track h4{margin:6px 0 4px;font-size:15px}
.track p{margin:0;font-size:13px;color:var(--ink-2)}

/* cite */
.bib{position:relative}
.bib pre{margin:0;background:var(--surface);border:1px solid var(--line);border-radius:10px;padding:16px;overflow-x:auto;font:12.5px/1.6 var(--mono);color:var(--ink-2)}
.bib .btn{position:absolute;top:10px;right:10px;padding:4px 10px;font-size:12px}
footer{padding-block:28px 48px;border-top:1px solid var(--line);font-size:12px;color:var(--muted)}

/* pipeline figure */
.fig{border:1px solid var(--line);border-radius:14px;background:var(--surface);overflow:hidden}
.fig-scroll{overflow-x:auto}
#pipe{display:block;width:100%;min-width:820px;height:auto}
#pipe .st rect,#pipe .st polygon{fill:var(--surface);stroke:var(--line-2);stroke-width:1.3;transition:fill .3s,stroke .3s}
#pipe .st .t{font:600 13px var(--sans);fill:var(--ink)}
#pipe .st .s{font:11px var(--mono);fill:var(--muted)}
#pipe .st.on rect,#pipe .st.on polygon{fill:var(--accent-soft);stroke:var(--accent);stroke-width:2}
#pipe .st.ok rect{stroke:var(--pos)}
#pipe .st.ok .t{fill:var(--pos)}
#pipe .ed{fill:none;stroke:var(--line-2);stroke-width:1.6;marker-end:url(#arr);transition:stroke .3s}
#pipe .ed.on{stroke:var(--accent);stroke-width:2.4;marker-end:url(#arrOn)}
#pipe .el{font:500 10.5px var(--mono);fill:var(--muted)}
#pipe .panel-bg{fill:var(--surface-2);stroke:var(--line)}
#pipe .pt{font:500 10.5px var(--mono);letter-spacing:.1em;fill:var(--muted)}
#pipe .pc{font:500 11px var(--mono);fill:var(--accent-ink)}
#pipe .dn{transition:opacity .4s}
#pipe .dn.off{opacity:0}
#pipe .dn rect{fill:var(--surface);stroke:var(--line-2);stroke-width:1.3}
#pipe .dn text{font:600 11px var(--mono);fill:var(--ink)}
#pipe .dn.proc rect{stroke:var(--accent);stroke-width:2;fill:var(--accent-soft)}
#pipe .dn.ok rect{stroke:var(--pos);fill:var(--pos-soft)}
#pipe .dn.bad rect{stroke:var(--del);fill:var(--del-bg);stroke-dasharray:4 3}
#pipe .dn.bad text{fill:var(--del)}
#pipe .dn.and circle{fill:var(--surface);stroke:var(--ink-2);stroke-width:1.4}
#pipe .dn.and text{font:700 10px var(--sans);fill:var(--ink-2)}
#pipe .dn.and.bad circle{stroke:var(--del);fill:var(--del-bg)}
#pipe .dn.and.bad text{fill:var(--del)}
#pipe .de{stroke:var(--line-2);stroke-width:1.3;fill:none}
#pipe .dn.share path{stroke:var(--warn);stroke-width:1.6;stroke-dasharray:5 4;fill:none}
#pipe .lg{font:10.5px var(--mono);fill:var(--muted)}
#pipe .tok{fill:var(--accent);filter:drop-shadow(0 0 4px var(--accent))}
@media (prefers-reduced-motion:reduce){#pipe *{transition:none!important}}
.fig-bar{display:flex;flex-wrap:wrap;align-items:center;gap:12px;padding:12px 16px;border-top:1px solid var(--line);background:var(--surface-2)}
.fig-bar .btn{padding:5px 12px}
#pCap{flex:1;min-width:240px;font-size:14px;color:var(--ink-2)}
#pCap .pn{font:600 11px var(--mono);color:var(--accent-ink);margin-right:10px}
#pDots{display:flex;gap:5px}
#pDots button{width:8px;height:8px;border-radius:50%;border:0;padding:0;background:var(--line-2);cursor:pointer}
#pDots button.on{background:var(--accent);width:20px;border-radius:4px}
.pillars{display:grid;grid-template-columns:repeat(3,minmax(0,1fr));gap:12px;margin-top:16px}
@media (max-width:860px){.pillars{grid-template-columns:1fr}}
.pillar{border:1px solid var(--line);background:var(--surface);border-radius:12px;padding:18px;min-width:0}
.pillar .k{font:600 11px var(--mono);letter-spacing:.12em;text-transform:uppercase;color:var(--accent-ink)}
.pillar h4{font-size:16px;margin:6px 0 10px}
.pillar ul{margin:0;padding-left:18px;display:grid;gap:6px;font-size:13.5px;color:var(--ink-2)}
.layers{margin-top:16px}
.run{display:grid;grid-template-columns:minmax(0,1fr) minmax(0,1fr);gap:16px}
@media (max-width:860px){.run{grid-template-columns:1fr}}
.run pre{margin:0;background:var(--surface);border:1px solid var(--line);border-radius:10px;padding:14px 16px;overflow-x:auto;font:12.5px/1.7 var(--mono);color:var(--ink)}
.run pre .c{color:var(--muted)}
.otable{width:100%;border-collapse:collapse;font-size:13px;background:var(--surface);border:1px solid var(--line);border-radius:10px;overflow:hidden}
.otable td{padding:8px 12px;border-bottom:1px solid var(--line);vertical-align:top;color:var(--ink-2)}
.otable td:first-child{font:500 12px var(--mono);color:var(--ink);white-space:nowrap}
.otable tr:last-child td{border-bottom:0}

/* informal proof and Lean viewer */
.doc-head{display:flex;flex-wrap:wrap;gap:6px 18px;align-items:center;font-size:12.5px;color:var(--muted);margin:0 0 10px}
.prose{border:1px solid var(--line);border-radius:12px;background:var(--surface);padding:8px 28px 24px;max-height:820px;overflow:auto;font-size:15px;line-height:1.7;color:var(--ink)}
.prose>*{max-width:78ch}
.prose h1{font-size:24px;margin:24px 0 12px}
.prose h2{font-size:20px;margin:28px 0 10px}
.prose h3{font-size:16.5px;margin:22px 0 8px}
.prose h4{font-size:15px;margin:18px 0 6px}
.prose p,.prose li{color:var(--ink-2)}
.prose blockquote{margin:12px 0;padding:4px 16px;border-left:3px solid var(--line-2);color:var(--ink-2)}
.prose table{border-collapse:collapse;font-size:13.5px;margin:12px 0;display:block;overflow-x:auto;max-width:100%}
.prose th,.prose td{border:1px solid var(--line);padding:6px 10px;text-align:left;vertical-align:top}
.prose th{background:var(--surface-2)}
.prose pre{background:var(--surface-2);border:1px solid var(--line);border-radius:8px;padding:12px;overflow-x:auto;font-size:12.5px}
.prose pre code{background:none;padding:0}
.prose hr{border:0;border-top:1px solid var(--line);margin:24px 0}
.prose .katex-display{overflow-x:auto;overflow-y:hidden;padding:4px 0}
.lh{font-size:15px;margin:22px 0 8px}
.lh:first-child{margin-top:0}
.lh span{font:500 12px var(--mono);color:var(--muted);margin-left:8px}
.code-view{max-height:640px;overflow:auto;font-size:12px;line-height:1.5}
#pipe .ah{fill:var(--line-2)}
#pipe .ah2{fill:var(--accent)}

/* multi-page layout */
.nav nav a[aria-current="page"]{color:var(--ink);font-weight:600}
.hero .btns{margin:22px 0 22px}
.sec-head{display:flex;flex-wrap:wrap;align-items:flex-end;justify-content:space-between;gap:12px;margin-bottom:18px}
.sec-head h2{margin-bottom:0}
.page-head{padding-block:40px 28px}
.page-body{padding-block:8px 64px}
h1.ph{font-size:clamp(28px,4vw,40px);line-height:1.12;font-weight:800;letter-spacing:-.02em;margin:8px 0 10px;max-width:24em;text-wrap:balance}
.crumbrow{display:flex;flex-wrap:wrap;justify-content:space-between;align-items:center;gap:10px;margin-bottom:18px}
.crumb{display:flex;gap:8px;font-size:13px;color:var(--muted)}
.crumb a{color:var(--accent-ink);text-decoration:none}
.pager{display:flex;gap:8px}
.pager .btn{padding:5px 11px;font-size:12.5px}
.page-body .stabs{margin-top:0}
.prow a.pt{color:var(--ink);text-decoration:none}
.prow a.pt:hover{color:var(--accent-ink)}
.prow td:first-child{padding-left:16px}

/* featured carousel: three cards in view */
.car{position:relative}
.car-track{display:grid;grid-auto-flow:column;grid-auto-columns:calc((100% - 28px) / 3);gap:14px;overflow-x:auto;scroll-snap-type:x mandatory;scroll-behavior:smooth;scrollbar-width:none;padding:4px 2px 6px;overscroll-behavior-x:contain}
.car-track::-webkit-scrollbar{display:none}
@media (max-width:1000px){.car-track{grid-auto-columns:calc((100% - 14px) / 2)}}
@media (max-width:640px){.car-track{grid-auto-columns:86%}}
.car-track .fcard{scroll-snap-align:start}
@media (prefers-reduced-motion:reduce){.car-track{scroll-behavior:auto}.car-track .fcard{transition:none}}
.car-btn{position:absolute;top:50%;transform:translateY(-50%);z-index:2;width:38px;height:38px;border-radius:50%;border:1px solid var(--line-2);background:var(--surface);color:var(--ink);font-size:22px;line-height:1;cursor:pointer;box-shadow:0 4px 14px rgba(0,0,0,.08)}
.car-btn.prev{left:-18px}.car-btn.next{right:-18px}
.car-btn:hover{border-color:var(--accent);color:var(--accent-ink)}
.car-btn:disabled{opacity:0;pointer-events:none}
@media (max-width:640px){.car-btn.prev{left:-6px}.car-btn.next{right:-6px}}
.car.static .car-btn{display:none}
.car-dots{display:flex;justify-content:center;gap:6px;margin-top:14px}
.car-dots button{width:8px;height:8px;border-radius:4px;border:0;padding:0;background:var(--line-2);cursor:pointer;transition:width .2s,background .2s}
.car-dots button.on{background:var(--accent);width:20px}
.car.static + .car-dots{display:none}

/* hero headline: one short line of numbers right under the lede */
.headline{display:flex;flex-wrap:wrap;align-items:baseline;gap:6px 0;margin:-6px 0 24px;font-size:15px;color:var(--ink-2)}
.headline .hp{display:inline-flex;align-items:baseline;gap:6px;white-space:nowrap}
.headline .hp+.hp::before{content:"";align-self:center;width:4px;height:4px;border-radius:50%;background:var(--line-2);margin:0 14px}
.headline .hn{font:600 22px/1 var(--mono);color:var(--accent-ink);letter-spacing:-.01em;font-variant-numeric:tabular-nums}
@media (max-width:640px){.headline{flex-direction:column;align-items:flex-start;gap:6px}.headline .hp+.hp::before{display:none}}

/* hero: three principles, set like the page's other labelled blocks */
.values{list-style:none;margin:0 0 26px;padding:0;display:grid;grid-template-columns:repeat(3,minmax(0,1fr));gap:0;max-width:62em;border-top:1px solid var(--line);border-bottom:1px solid var(--line)}
.values li{padding:14px 18px 14px 0;font-size:13.5px;line-height:1.55;color:var(--ink-2)}
.values li+li{padding-left:18px;border-left:1px solid var(--line)}
.values .vk{display:block;font:600 11px var(--mono);letter-spacing:.14em;text-transform:uppercase;color:var(--accent-ink);margin-bottom:6px}
@media (max-width:760px){.values{grid-template-columns:1fr}.values li+li{padding-left:0;border-left:0;border-top:1px solid var(--line)}}

/* people */
.people{display:grid;gap:10px;max-width:64em;margin-top:6px}
.prow2{display:grid;grid-template-columns:130px minmax(0,1fr);gap:16px;align-items:baseline}
@media (max-width:640px){.prow2{grid-template-columns:1fr;gap:2px}}
.plabel{font:500 10.5px var(--mono);letter-spacing:.14em;text-transform:uppercase;color:var(--muted)}
.prow2 p{margin:0;font-size:13.5px;line-height:1.7;color:var(--ink-2)}
.pn{white-space:nowrap}
.people sup,.affils sup{font:500 9.5px var(--mono);color:var(--accent-ink);margin-left:1px}
.affils{list-style:none;margin:4px 0 0;padding:0 0 0 146px;display:flex;flex-wrap:wrap;gap:4px 18px;font-size:12px;color:var(--muted)}
@media (max-width:640px){.affils{padding-left:0}}
.affils sup{margin-right:3px}

/* problem drawer */
html.drawer-on{overflow:hidden}
.drawer{position:fixed;inset:0;z-index:80}
.drawer-scrim{position:absolute;inset:0;background:rgba(15,18,20,.38);opacity:0;transition:opacity .5s}
.drawer-panel{position:absolute;top:0;right:0;bottom:0;width:min(96vw,1360px);display:flex;flex-direction:column;background:var(--bg);box-shadow:-24px 0 60px rgba(0,0,0,.18);transform:translateX(100%);transition:transform .55s cubic-bezier(.22,.7,.16,1);padding-top:env(safe-area-inset-top,0px)}
.drawer.open .drawer-scrim{opacity:1}
.drawer.open .drawer-panel{transform:none}
@media (max-width:640px){.drawer-panel{width:100vw}}
@media (prefers-reduced-motion:reduce){.drawer-scrim,.drawer-panel{transition:none}}
.drawer-bar{display:flex;align-items:center;gap:14px;padding:10px 16px;border-bottom:1px solid var(--line);background:var(--surface)}
.drawer-x{width:34px;height:34px;border-radius:8px;border:1px solid var(--line-2);background:var(--surface);color:var(--ink);font-size:20px;line-height:1;cursor:pointer;flex:none}
.drawer-x:hover{border-color:var(--muted)}
.drawer-t{display:flex;flex-direction:column;min-width:0;flex:1}
.drawer-t #drawerTitle{font-weight:700;font-size:15px;white-space:nowrap;overflow:hidden;text-overflow:ellipsis}
.drawer-bar .btn{padding:6px 12px;font-size:12.5px;flex:none}
.drawer-frame{flex:1;width:100%;border:0;background:var(--bg)}
/* embedded problem page: no site chrome */
html.embed .nav,html.embed footer,html.embed .crumb{display:none}
html.embed .page-head{padding-top:22px}
html.embed .crumbrow{justify-content:flex-end}

.fcard,.fcard:hover{text-decoration:none;color:inherit}
.nav .wrap{height:58px}

/* how-it-works figure */
#pipe .st.agent rect{fill:var(--ink);stroke:var(--ink)}
#pipe .st.agent .t{fill:var(--bg);font-size:15px}
#pipe .st.agent .s{fill:var(--line-2)}
#pipe .st.agent.on rect{fill:var(--ink);stroke:var(--accent);stroke-width:3}
#pipe .dn.open rect{fill:var(--surface);stroke:var(--line-2)}
#pipe .wk{opacity:0;transition:opacity .3s}
#pipe .wk rect{fill:var(--accent);stroke:none}
#pipe .wk text{font:600 9.5px var(--mono);fill:#fff}
#pipe .dn.proc .wk{opacity:1}
#pipe .bx{font:600 10.5px var(--mono);fill:var(--del)}
.pillar p{margin:0;font-size:13.5px;line-height:1.6;color:var(--ink-2)}

/* how-it-works figure v3: orchestrator, subagents, LEAP-CLI with a compiler gate */
#pipe .ed{stroke-dasharray:none}
#pipe .ed.on{stroke-dasharray:6 6;animation:flow .9s linear infinite}
@keyframes flow{to{stroke-dashoffset:-12}}
@media (prefers-reduced-motion:reduce){#pipe .ed.on{animation:none;stroke-dasharray:none}}
#pipe .st.sub .sh1,#pipe .st.sub .sh2{opacity:0;transition:opacity .4s}
#pipe .st.sub.multi .sh1{opacity:.75}
#pipe .st.sub.multi .sh2{opacity:.45}
#pipe .par{font:600 10.5px var(--mono);fill:var(--accent-ink)}
#pipe .st.cli rect{fill:var(--surface-2);stroke:var(--line-2);stroke-width:1.4}
#pipe .st.cli.on rect{fill:var(--surface-2);stroke:var(--accent);stroke-width:2}
#pipe .clit{font:800 15px var(--sans);fill:var(--ink);letter-spacing:.04em}
#pipe .st.gate rect{fill:var(--surface);stroke:var(--line-2);stroke-width:1.4}
#pipe .st.gate.on rect{fill:var(--pos-soft);stroke:var(--pos);stroke-width:2}
#pipe .gt{font:600 10px var(--mono);letter-spacing:.16em;fill:var(--ink-2)}
#pipe .gx{fill:var(--del-bg);stroke:var(--del);stroke-width:1.5}
#pipe .gxt{font:700 12px var(--sans);fill:var(--del)}
#pipe .dn.open rect{fill:var(--surface);stroke:var(--ink-2)}
#pipe .dn.redo rect{fill:var(--warn-soft);stroke:var(--warn);stroke-dasharray:4 3;stroke-width:1.6}
#pipe .dn.redo text{fill:var(--warn)}
#pipe .dn rect,#pipe .st rect{transition:fill .4s,stroke .4s}
#pDots{margin-left:auto}

/* gate */
#pipe .gt{font:600 11px var(--sans);letter-spacing:0;fill:var(--ink)}
#pipe .gt2{font:500 10.5px var(--mono);letter-spacing:.08em;fill:var(--muted)}
#pipe .glock{fill:none;stroke:var(--ink-2);stroke-width:2.2}
#pipe .gbody{fill:var(--ink-2)}
#pipe .gok circle{fill:var(--surface);stroke:var(--line-2);stroke-width:1.4}
#pipe .gok path{fill:none;stroke:var(--line-2);stroke-width:2.2;stroke-linecap:round;stroke-linejoin:round}
#pipe .st.gate.on .gok circle{fill:var(--pos);stroke:var(--pos)}
#pipe .st.gate.on .gok path{stroke:#fff}
#pipe .st.gate.on .glock{stroke:var(--pos)}
#pipe .st.gate.on .gbody{fill:var(--pos)}

/* affiliation logos */
.affils li{display:inline-flex;align-items:center}
.affils img{width:13px;height:13px;margin-right:5px;vertical-align:-2px}

/* run it */
.run2{display:grid;grid-template-columns:minmax(0,1.1fr) minmax(0,1fr);gap:18px;align-items:start}
@media (max-width:900px){.run2{grid-template-columns:1fr}}
.rsteps{list-style:none;margin:0;padding:0;display:grid;gap:12px}
.rsteps li{display:grid;grid-template-columns:34px minmax(0,1fr);gap:14px;border:1px solid var(--line);background:var(--surface);border-radius:12px;padding:16px}
.rn{width:30px;height:30px;border-radius:50%;background:var(--accent-soft);color:var(--accent-ink);font:700 14px var(--mono);display:grid;place-items:center}
.rb h4{margin:3px 0 4px;font-size:15px}
.rb p{margin:0 0 10px;font-size:13.5px;color:var(--ink-2)}
.cmd{position:relative}
.cmd pre{margin:0;background:var(--ink);color:var(--bg);border-radius:8px;padding:12px 70px 12px 14px;font:12.5px/1.7 var(--mono);overflow-x:auto}
.cmd .copy{position:absolute;top:8px;right:8px;border:1px solid color-mix(in srgb,var(--bg) 30%,transparent);background:transparent;color:var(--bg);border-radius:6px;padding:2px 9px;font:500 11px var(--mono);cursor:pointer;opacity:.8}
.cmd .copy:hover{opacity:1}
.tree{border:1px solid var(--line);border-radius:12px;background:var(--surface);overflow:hidden}
.tree-h{display:flex;align-items:center;gap:6px;padding:10px 14px;background:var(--surface-2);border-bottom:1px solid var(--line);font:500 11px var(--mono);color:var(--muted)}
.tree-h span:last-child{margin-left:8px}
.dotr,.doty,.dotg{width:10px;height:10px;border-radius:50%;background:var(--line-2)}
.tree ul{list-style:none;margin:0;padding:12px 16px;display:grid;gap:2px}
.tree li{display:grid;grid-template-columns:minmax(150px,auto) minmax(0,1fr);gap:14px;padding:6px 0 6px 18px;border-left:1px solid var(--line);font-size:13px;margin-left:6px}
.tree li.d{display:block;border-left:0;margin-left:0;padding-left:0;font:600 12.5px var(--mono);color:var(--ink)}
.tree .f{font:500 12.5px var(--mono);color:var(--ink)}
.tree .f.hl{color:var(--accent-ink)}
.tree .f.ok{color:var(--pos)}
.tree .c{color:var(--muted)}
@media (max-width:640px){.tree li{grid-template-columns:1fr;gap:0}}
.tree-f{margin:0;padding:12px 16px;border-top:1px solid var(--line);font-size:12.5px;color:var(--muted)}
.cmd{display:flex;align-items:flex-start;background:var(--ink);border-radius:8px}
.cmd pre{flex:1;min-width:0;background:none;padding:12px 14px}
.cmd .copy{position:static;flex:none;margin:9px 9px 0 0}

/* real Lean code: statement, preview, full viewer, numbered proof */
.xbox{position:relative}
pre.lean.wrap{white-space:pre-wrap;overflow-wrap:anywhere;max-height:280px;overflow:auto}
.peek-code{position:relative;max-height:150px;overflow:hidden;border-radius:8px}
.peek-code pre.lean{margin:0;white-space:pre;overflow:hidden}
.peek-code::after{content:"";position:absolute;left:0;right:0;bottom:0;height:60px;background:linear-gradient(transparent,var(--surface))}
.side-act{display:flex;flex-wrap:wrap;gap:6px;margin-top:8px}
.side-act .btn{padding:5px 10px;font-size:12px}
details.defs{margin-top:12px;font-size:12.5px}
details.defs summary{cursor:pointer;color:var(--accent-ink)}
details.defs pre{margin-top:6px}
.pop-f2{font:11px var(--mono);color:var(--muted);margin-top:8px}
.cview{position:absolute;left:0;right:0;bottom:0;top:96px;z-index:6;display:flex;flex-direction:column;background:var(--surface);border-top:1px solid var(--line)}
.cv-head{display:flex;flex-wrap:wrap;align-items:center;gap:10px 16px;padding:10px 14px;border-bottom:1px solid var(--line);background:var(--surface-2)}
.cv-t{display:flex;flex-direction:column;min-width:0}
.cv-t .nm{font:600 14px var(--mono);word-break:break-all}
.cv-b{display:flex;gap:6px;flex-wrap:wrap}
.cv-a{margin-left:auto;display:flex;gap:6px;align-items:center}
.cv-a .btn{padding:5px 10px;font-size:12px}
.cv-body{flex:1;overflow:auto;padding:8px 0;font:12.5px/1.6 var(--mono);color:var(--ink)}
.cv-defs{border-bottom:1px dashed var(--line-2);padding-bottom:6px;margin-bottom:6px}
.cv-defs .kicker{padding:4px 14px}
.cl{display:flex;min-width:max-content}
.cl i{flex:none;width:56px;padding-right:14px;text-align:right;color:var(--muted);opacity:.6;font-style:normal;user-select:none;font-variant-numeric:tabular-nums}
.cl>span{white-space:pre;padding-right:16px}
.cl.hit{background:var(--accent-soft)}
.cl .ll[data-n]{cursor:pointer}
.proof-bar{display:flex;flex-wrap:wrap;align-items:center;gap:8px;margin:0 0 8px;font-size:12.5px;color:var(--muted)}
.proof-bar select{border:1px solid var(--line-2);background:var(--surface);color:var(--ink);border-radius:6px;padding:4px 6px;font:12px var(--mono);max-width:100%}
.proof-bar .sp{flex:1}
.code-view{max-height:72vh;overflow:auto;font:12.5px/1.6 var(--mono);background:var(--surface-2);border:1px solid var(--line);border-radius:10px;padding:8px 0;color:var(--ink)}
.code-view{position:relative}
.tracks{grid-template-columns:repeat(auto-fit,minmax(240px,1fr))}