:root{--green:#2F7D55;--green-d:#1E5C3C;--card:#E6F2EA;--card-b:#6FA287;--ink:#1F3B2C;--sub:#5C7466;--edge:#8A9AA5;--violet:#8C7FD9;--bg:#FAFBF9;--rule:#DDE5DF;--warn:#9A5B00;--mono:"DejaVu Sans Mono","SFMono-Regular",Menlo,Consolas,monospace;--sans:Helvetica,Arial,"Liberation Sans",sans-serif;--serif:Georgia,"Times New Roman",serif}
*{box-sizing:border-box}
html{font-size:16px}
body{margin:0;font-family:var(--sans);color:#22313A;background:var(--bg);line-height:1.5}
a{color:var(--green-d);text-decoration:none}a:hover{text-decoration:underline}
code,pre{font-family:var(--mono);font-size:.86rem}
code{background:#EEF3EF;padding:0 .25em;border-radius:3px;word-break:break-word}
a code{color:inherit}
pre{background:#fff;border:1px solid var(--rule);border-radius:6px;padding:.7rem .9rem;overflow-x:auto;line-height:1.4;white-space:pre-wrap;word-break:break-word}
pre code{background:none;padding:0}
h1{font-family:var(--serif);font-weight:normal;font-size:1.9rem;margin:.3em 0 .3em;color:#15251C}
h2{font-size:1.15rem;margin:1.6em 0 .5em;color:#15251C;border-bottom:1px solid var(--rule);padding-bottom:.2em}
h3{font-size:1rem;margin:1.2em 0 .4em;color:#2b3b33}
.small{font-size:.85em}.muted{color:var(--sub)}.warn{color:var(--warn)}
header.top{background:#fff;border-bottom:1px solid var(--rule);position:sticky;top:0;z-index:20}
header.top .inner{max-width:1180px;margin:0 auto;padding:.5rem 1rem;display:flex;align-items:center;gap:1rem;flex-wrap:wrap}
header.top .brand{font-family:var(--serif);font-size:1.1rem;color:var(--green-d);white-space:nowrap}
header.top .brand b{color:#15251C;font-weight:normal}
header.top nav a{margin-right:.9rem;color:#2b3b33;font-size:.93rem}
header.top nav a.cur{color:var(--green-d);font-weight:bold}
.search{position:relative;flex:1;min-width:240px}
.search input{width:100%;padding:.42rem .7rem;border:1px solid #C6D2C9;border-radius:6px;font-size:.95rem;font-family:var(--mono)}
.search input:focus{outline:2px solid var(--card-b)}
#q-results{display:none;position:absolute;top:105%;left:0;right:0;background:#fff;border:1px solid #C6D2C9;border-radius:6px;max-height:70vh;overflow:auto;box-shadow:0 8px 24px rgba(0,0,0,.12);z-index:30}
a.sr{display:block;padding:.4rem .7rem;border-bottom:1px solid #EEF2EF;color:#22313A}
a.sr:hover,a.sr.active{background:var(--card);text-decoration:none}
a.sr code{display:block;background:none;font-size:.8rem;color:#2b3b33}
.sr-kind{display:inline-block;font-size:.7rem;text-transform:uppercase;letter-spacing:.04em;color:#fff;background:var(--green);border-radius:3px;padding:0 .35em;margin-right:.4em}
.sr-kind.def{background:var(--violet)}
.sr-title{font-size:.9rem;margin-right:.4em}
.sr-num{font-size:.75rem;color:var(--sub)}
.sr-empty,.sr-more{padding:.5rem .7rem;color:var(--sub);font-size:.85rem}
main{max-width:1180px;margin:0 auto;padding:1rem 1rem 4rem}
main.prose{max-width:920px}
.prose p,.prose li{font-family:var(--serif);font-size:1.04rem}
.prose table{border-collapse:collapse;font-size:.9rem;margin:1em 0;display:block;overflow-x:auto}
.prose th,.prose td{border:1px solid var(--rule);padding:.35em .6em;vertical-align:top;text-align:left}
.prose th{background:#F1F5F2}
.prose blockquote{border-left:3px solid var(--card-b);margin:1em 0;padding:.2em 1em;color:#34463c;background:#F4F8F5}
.badge{display:inline-block;font-size:.72rem;border-radius:10px;padding:.05em .6em;margin-right:.35em;border:1px solid var(--card-b);background:var(--card);color:var(--ink);vertical-align:middle;white-space:nowrap}
.badge.lm{background:var(--green);border-color:var(--green-d);color:#fff}
.badge.root{background:var(--green-d);border-color:var(--green-d);color:#fff}
.badge.stage{background:#fff}
.badge.dup{background:#FFF6E5;border-color:#E0B96B;color:#6B4A00}
.badge.proved{background:#fff;border-color:var(--card-b);color:var(--green-d)}
.badge.def{background:#F4F1FA;border-color:var(--violet);color:#3b3363}
nav.path{font-size:.86rem;background:#fff;border:1px solid var(--rule);border-radius:6px;padding:.45rem .7rem;margin-bottom:.8rem;line-height:1.7}
nav.path .sep{color:var(--edge);margin:0 .15em}
nav.path .here{color:#15251C;font-weight:bold}
.thm-head h1{margin-bottom:.1em}
.thm-head .lean-name code{font-size:.95rem;background:none;padding:0;color:#2b3b33}
.badges{margin:.5rem 0 0}
pre.lean{background:#fff}
pre.lean.ctx{color:#5C7466;border-style:dashed;margin-bottom:.3rem;padding:.4rem .9rem}
pre.lean.stmt{border-color:var(--card-b);border-width:1.5px;font-size:.9rem}
pre.lean.sol{font-size:.82rem}
.en{font-family:var(--serif);font-size:1.12rem;background:#fff;border-left:4px solid var(--green);padding:.6rem 1rem;border-radius:0 6px 6px 0}
.en-context{font-family:var(--serif);margin-top:.6rem}
.strength{background:#FBFAF4;border:1px solid #E8E0C2;border-radius:6px;padding:.1rem 1rem .6rem;margin-top:.8rem}
ul.kv{list-style:none;padding:0;margin:0;display:flex;flex-wrap:wrap;gap:.4rem 1.4rem}
ul.kv li{font-size:.92rem}
.two-col{display:grid;grid-template-columns:1fr 1fr;gap:2rem}
@media(max-width:860px){.two-col{grid-template-columns:1fr}}
ul.refs{list-style:none;padding:0;margin:0}
ul.refs li{padding:.22rem 0;border-bottom:1px solid #EEF2EF;font-size:.9rem}
ul.refs li code{font-size:.78rem;background:none;padding:0;color:#2b3b33}
a.thm-ref .t{font-size:.92rem}
a.thm-ref:hover{text-decoration:none}a.thm-ref:hover code{text-decoration:underline}
.nums{font-size:.75rem;white-space:nowrap}
.graph-box{background:#fff;border:1px solid var(--rule);border-radius:6px;padding:.5rem;min-height:120px;overflow:auto;text-align:center}
.graph-box svg{max-width:100%;height:auto}
.graph-tools{margin:.2rem 0 .5rem;font-size:.85rem}
button{font:inherit;font-size:.85rem;border:1px solid #C6D2C9;background:#fff;border-radius:5px;padding:.15rem .6rem;cursor:pointer;color:#2b3b33}
button:hover{background:var(--card)}
button.small{font-size:.72rem;padding:.05rem .45rem;vertical-align:middle}
ul.src-links{list-style:none;padding:0}
ul.src-links li{margin:.3rem 0}
.hero{display:grid;grid-template-columns:1.1fr .9fr;gap:2rem;align-items:start}
@media(max-width:980px){.hero{grid-template-columns:1fr}}
.hero .stmt pre{font-size:.95rem;border-color:var(--card-b);border-width:1.5px}
.cards{display:grid;grid-template-columns:repeat(auto-fill,minmax(250px,1fr));gap:.8rem;margin:1rem 0}
.card{background:#fff;border:1px solid var(--rule);border-radius:8px;padding:.7rem .9rem}
.card h3{margin:0 0 .3em;font-size:.98rem}
.card p{margin:0;font-size:.88rem;color:#34463c;font-family:var(--serif)}
.card .num{font-size:.75rem;color:var(--sub)}
.stage-num{display:inline-block;width:1.5em;height:1.5em;line-height:1.5em;text-align:center;border-radius:50%;background:var(--green);color:#fff;font-size:.8rem;margin-right:.4em}
.figure{background:#fff;border:1px solid var(--rule);border-radius:8px;padding:.6rem;text-align:center;overflow:auto}
.figure svg{max-width:100%;height:auto}
.figure figcaption,.caption{font-size:.82rem;color:var(--sub);text-align:left;margin-top:.4rem}
.numbers-grid{display:grid;grid-template-columns:repeat(auto-fill,minmax(170px,1fr));gap:.6rem;margin:1rem 0}
.numbers-grid div{background:#fff;border:1px solid var(--rule);border-radius:8px;padding:.5rem .7rem}
.numbers-grid b{display:block;font-size:1.3rem;color:var(--green-d);font-weight:normal;font-family:var(--serif)}
.numbers-grid span{font-size:.8rem;color:var(--sub)}
.thm-card{background:#fff;border:1px solid var(--rule);border-left:4px solid var(--card-b);border-radius:0 8px 8px 0;padding:.5rem .9rem;margin:.8rem 0}
.thm-card .name{font-family:var(--mono);font-size:.82rem}
.thm-card pre{margin:.4rem 0;font-size:.8rem;max-height:22em;overflow:auto}
.thm-card .meta{font-size:.78rem;color:var(--sub)}
table.plain{border-collapse:collapse;font-size:.88rem}
table.plain td,table.plain th{border-bottom:1px solid var(--rule);padding:.3em .7em;text-align:left;vertical-align:top}
.lm-list li{margin:.2rem 0}
.src pre{font-size:.8rem;white-space:pre;word-break:normal}
.src pre{counter-reset:ln}.src .l{counter-increment:ln}.src .l::before{content:counter(ln);display:inline-block;width:3.2em;color:#A0AFA6;text-align:right;padding-right:.8em;user-select:none}.src .l:target{background:#FFF7D6}
.src a.anchor{color:#A0AFA6}
.decl-index{columns:2;font-size:.82rem;column-gap:2rem}
.decl-index li{break-inside:avoid}
.decl-index .kw{color:var(--sub);font-size:.75rem;margin-right:.3em}
footer{max-width:1180px;margin:0 auto;padding:1rem;color:var(--sub);font-size:.8rem;border-top:1px solid var(--rule)}
/* Lean highlighting (Pygments class names) */
.kn,.k,.kd,.kr{color:#7B3294;font-weight:600}
.kt{color:#1B6CA8}
.nf{color:#15251C;font-weight:700}
.nd,.na{color:#8A6D1F}
.mi,.mf,.m{color:#0F7A5B}
.s,.s2,.s1{color:#B3451F}
.c,.cm,.c1,.cs,.sd{color:#7D8F85;font-style:italic}
.o,.bp{color:#5B6B73}
.katex{font-size:1.05em}
.toc{font-size:.88rem;background:#fff;border:1px solid var(--rule);border-radius:6px;padding:.5rem 1rem;margin:1rem 0}
.toc ul{margin:.2rem 0;padding-left:1.2rem}
.legend{font-size:.8rem;color:var(--sub);display:flex;gap:1.2rem;flex-wrap:wrap;align-items:center;margin:.4rem 0}
.legend i{display:inline-block;width:1.1em;height:.8em;border-radius:3px;vertical-align:middle;margin-right:.3em;border:1.5px solid var(--card-b);background:var(--card)}
.legend i.root{background:var(--green);border-color:var(--green-d)}
.legend i.def{background:#F4F1FA;border-color:var(--violet);border-radius:0}
.legend i.lm{background:var(--card);border-color:var(--green);border-width:2.5px}

pre a.id{color:inherit;text-decoration:none;border-bottom:1px dotted #9DB5A6}
pre a.id:hover{color:var(--green-d);border-bottom:1px solid var(--green-d);background:#EEF6F0}
.provenance{background:#F6F7F3;border:1px solid #E3E6DA;border-radius:6px;padding:.4rem .7rem}
.figure.zoomable svg{cursor:zoom-in}
.figure.zoomed{overflow:auto}.figure.zoomed svg{max-width:none;cursor:zoom-out}
code.tex{background:none;color:#34463c}
span.tex{font-family:var(--mono);font-size:.9em;color:#34463c;white-space:pre-wrap}span.tex::before,span.tex::after{content:"$";color:#9aa69f}
span.tex.k{font-family:inherit;font-size:inherit;color:inherit;white-space:normal}span.tex.k::before,span.tex.k::after{content:none}
span.tex.d{display:block;text-align:center;margin:.6em 0;overflow-x:auto;overflow-y:hidden}span.tex.d.k{margin:0}span.tex.d>.katex-display{margin:.8em 0}
.refs-lit{font-family:var(--serif)}

.warnish{color:#8A6D1F}
details summary{cursor:pointer;color:var(--green-d);font-size:.9rem;margin:.3rem 0}

.en{font-size:1rem;border-left:3px solid #B9CDBF}
.en-context.lead{font-family:var(--serif);font-size:1rem;color:#34463c;margin:.6rem 0 .2rem;max-width:920px}
h2.en-title{font-family:var(--serif);font-weight:normal;border:none;font-size:1.35rem;margin:.2em 0}
.en p:first-child,.en-context p:first-child{margin-top:0}.en p:last-child,.en-context p:last-child{margin-bottom:0}

nav.path .hop{color:#8A6D1F;font-size:.8rem}

a.ext{color:#5B6B73}a.ext:hover{color:var(--green-d)}

.graph-box svg text[font-family=Courier]{font-family:var(--mono)}
.imperial{background:#fff;border:1px solid var(--rule);border-left:4px solid #8C7FD9;border-radius:0 8px 8px 0;padding:.6rem 1rem;margin:1rem 0;font-family:var(--serif)}

ol.refs-lit{padding-left:1.4rem}ol.refs-lit li{margin:.15rem 0;font-size:.9rem}