:root{--lightningcss-light:initial;--lightningcss-dark: ;color-scheme:light;--bg:#f5f7fa;--panel:#fff;--heading:#131b2b;--muted:#707888;--line:#e7e9ee;--soft:#f0f2f5;--accent:#4f46e5;--emphasis:#44546a;--shadow:0 1px 2px #1419230a, 0 10px 28px #1e223014;--mathlib:#0b5fd0;--mathlib-bg:#e3eefb;--lean:#137333;--lean-bg:#e3f3e8;--sorry:#c2410c;--sorry-bg:#fbe8e6;--empty:#6b7280;--empty-bg:#eef0f3;--serif:Georgia, "Playfair Display", "Times New Roman", serif;--sans:Inter, "Helvetica Neue", -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, sans-serif}*{box-sizing:border-box}.sr-only{clip:rect(0, 0, 0, 0);white-space:nowrap;border:0;width:1px;height:1px;margin:-1px;padding:0;position:absolute;overflow:hidden}body{background:var(--bg);color:var(--heading);font:16px/1.6 var(--sans);-webkit-font-smoothing:antialiased;margin:0}a{color:inherit;text-decoration:none}.page{max-width:1050px;margin:0 auto;padding:72px 24px 96px}.page-loading,.page-error{text-align:center;color:var(--muted);font:15px var(--sans);padding:80px 24px}.hero{text-align:center;max-width:720px;margin:0 auto 72px}.hero h1{font:700 clamp(28px, 4vw, 40px) / 1.2 var(--serif);color:var(--heading);letter-spacing:0;margin:0 0 14px}.hero .subtitle{color:var(--muted);margin:0;font-size:clamp(15px,1.6vw,18px)}.landing-tabs{justify-content:center;gap:6px;margin:0 0 56px;display:flex}.landing-tab{color:var(--muted);font:700 14px var(--sans);cursor:pointer;border:1px solid #0000;border-radius:999px;padding:8px 20px}.landing-tab:hover{color:var(--heading);background:var(--bg)}.landing-tab.on{color:var(--accent);background:color-mix(in srgb, var(--accent) 10%, #fff);border-color:color-mix(in srgb, var(--accent) 25%, transparent)}.section{margin:0 0 96px}.section-title{font:700 clamp(24px, 2.6vw, 32px) / 1.25 var(--serif);margin:0 0 12px}.section-underline{border-radius:2px;width:72px;height:3px;margin:0 0 14px;display:block}.section .subtitle{color:var(--muted);margin:0 0 28px;font-size:18px}.card-grid{grid-template-columns:repeat(auto-fill,minmax(340px,1fr));gap:32px;display:grid}.card{background:var(--panel);border:1px solid var(--line);box-shadow:var(--shadow);border-radius:16px;padding:28px;transition:transform .15s,box-shadow .15s;display:block}.card:hover{transform:translateY(-3px);box-shadow:0 4px 8px #1419230f,0 20px 40px #1e22301f}.card-illo{border-radius:10px;justify-content:center;align-items:center;height:180px;margin-bottom:24px;display:flex;position:relative;overflow:hidden}.card-illo>img{object-fit:cover;object-position:center 0%;width:100%;height:100%;display:block}.card-illo>img.fit-contain{object-fit:contain;object-position:center;filter:drop-shadow(0 2px 6px #1419232e);padding:10px}.card-pct{font:700 12px var(--sans);-webkit-backdrop-filter:blur(2px);backdrop-filter:blur(2px);border-radius:999px;padding:3px 9px;position:absolute;top:10px;right:10px}.card-author{font:700 19px var(--serif);color:var(--heading);margin-bottom:4px}.card-title{font:16px var(--sans);color:var(--muted);margin-bottom:12px}.card-blurb{color:var(--muted);margin:0 0 18px;font-size:13.5px;line-height:1.55}.card-row{align-items:center;gap:12px;margin-top:8px;display:flex}.card-pill{font:700 12.5px/1.35 var(--sans);white-space:nowrap;border-radius:999px;flex-direction:column;justify-content:center;padding:7px 16px;display:inline-flex}.card-links{font:600 12.5px/1.35 var(--sans);flex-direction:column;flex:1;display:inline-flex}.card-arrow{margin-left:auto;font-size:16px;font-weight:700}.overview{border-top:1px solid var(--line);margin:0 0 64px;padding-top:8px}.overview h1,.overview h2,.overview h3{font-family:var(--serif);color:var(--heading)}.overview p{color:var(--muted);line-height:1.7}.overview a{color:var(--heading);text-decoration:underline;-webkit-text-decoration-color:var(--line);text-decoration-color:var(--line)}.overview code{background:var(--line);border-radius:4px;padding:1px 5px;font-size:.92em}.footer{color:var(--muted);border-top:1px solid var(--line);padding-top:20px;font-size:13px}.footer a{color:var(--muted);text-decoration:underline}.site-header,.project-header{z-index:20;-webkit-backdrop-filter:saturate(1.4)blur(8px);backdrop-filter:saturate(1.4)blur(8px);border-bottom:1px solid var(--line);background:#ffffffe6;margin:0 0 24px;padding:11px 24px;position:sticky;top:0}.site-header{padding:11px 0}.site-htop{flex-wrap:wrap;align-items:baseline;gap:12px;max-width:1050px;margin:0 auto;padding:0 24px;display:flex}.site-brand{font:700 17px var(--serif);color:var(--heading);letter-spacing:.01em}.site-header+.page{padding-top:40px}.project-htop{flex-wrap:wrap;align-items:baseline;gap:12px;max-width:1660px;margin:0 auto;display:flex}.project-htop h1{letter-spacing:0;color:var(--heading);margin:0;font-size:17px;font-weight:700}.project-htop .sub{color:var(--muted);font-size:13px}.panel-toggle{width:28px;height:28px;color:var(--muted);cursor:pointer;background:0 0;border:1px solid #0000;border-radius:6px;justify-content:center;align-items:center;padding:0;transition:color .15s,background-color .15s,border-color .15s;display:inline-flex}.panel-toggle svg{width:16px;height:16px}.panel-toggle:hover{color:var(--accent);background:color-mix(in srgb, var(--accent) 7%, #fff);border-color:var(--line)}.panel-toggle:focus-visible{outline:2px solid var(--accent);outline-offset:2px}.panel-rails{z-index:25;pointer-events:none;position:fixed;inset:0}.panel-rail{border-color:var(--line);background:var(--panel);width:30px;height:34px;box-shadow:var(--shadow);pointer-events:auto;position:absolute;top:56px}.panel-rail-left{left:max(6px, calc(max(0px, (100vw - 1560px) / 2) + var(--doc-left-width) - 34px))}.panel-rail-right{right:max(6px, calc(max(0px, (100vw - 1560px) / 2) + var(--doc-right-width) - 34px))}.project-home{color:var(--muted);border:1px solid var(--line);background:var(--panel);white-space:nowrap;border-radius:8px;padding:4px 10px;font-size:12.5px;font-weight:600}.project-home:hover{border-color:var(--accent);color:var(--accent)}.project-stats{flex-wrap:wrap;align-items:center;gap:15px;margin-left:auto;display:flex}.pstat{color:var(--muted);white-space:nowrap;font-size:12.5px}.pstat b{color:var(--heading);font-size:14px}.pbar{background:var(--soft);vertical-align:middle;border-radius:5px;width:120px;height:6px;margin-left:6px;display:inline-block;overflow:hidden}.pbar>i{background:linear-gradient(90deg, var(--mathlib), var(--lean));height:100%;display:block}.chapter-title{font-size:20px}.stmt-list{flex-direction:column;gap:18px;display:flex}.stmt-card{background:var(--panel);border:1px solid var(--line);border-left:3px solid var(--empty);box-shadow:var(--shadow);border-radius:11px;padding:16px;scroll-margin-top:24px}.stmt-head{flex-wrap:wrap;align-items:baseline;gap:10px;margin-bottom:10px;display:flex}.stmt-kind{font:700 11px var(--sans);text-transform:uppercase;letter-spacing:.04em;color:var(--muted);background:var(--bg);border-radius:6px;padding:2px 7px}.stmt-title{font:600 16px var(--sans);color:var(--heading)}.stmt-badges{flex-wrap:wrap;justify-content:flex-end;align-items:center;gap:6px;margin-left:auto;display:flex}.stmt-blueprint-btn{border:1px solid var(--line);background:var(--bg);color:var(--muted);font:600 11.5px var(--sans);cursor:pointer;border-radius:7px;align-items:center;gap:5px;padding:3px 8px;display:inline-flex}.stmt-blueprint-btn:hover{border-color:var(--accent);color:var(--accent)}.stmt-body{color:var(--heading);margin:0 0 12px;font-size:14.5px;line-height:1.7}.stmt-mathlib{color:var(--muted);overflow-wrap:anywhere;margin-bottom:10px;font-size:12.5px}.stmt-lean{flex-direction:column;gap:8px;margin-bottom:12px;display:flex}.lean-block{background:var(--bg);border-radius:8px;padding:10px 12px}.lean-head{flex-wrap:wrap;align-items:center;gap:8px;margin-bottom:6px;font-size:13px;display:flex}.lean-head code{word-break:break-all;min-width:0}.lean-code{color:var(--heading);white-space:pre;margin:0;font:12.5px/1.5 ui-monospace,Consolas,monospace;overflow-x:auto}.deps-row{flex-wrap:wrap;align-items:center;gap:6px;margin-bottom:6px;font-size:12.5px;display:flex}.deps-label{color:var(--muted);margin-right:2px;font-weight:600}.dep-chip{background:var(--bg);color:var(--heading);border-radius:999px;padding:2px 10px}.dep-chip:hover{text-decoration:underline}.stmt-reviews{border-top:1px solid var(--line);margin-top:14px;padding-top:10px}.stmt-reviews summary{cursor:pointer;color:var(--muted);font-size:12.5px;font-weight:600}.ritem{border-bottom:1px solid var(--line);padding:9px 2px;font-size:13px}.ritem .k{color:var(--muted);margin-left:6px;font-size:12px}.rmeta{color:var(--muted);flex-wrap:wrap;gap:7px;margin-top:3px;font-size:12.5px;display:flex}.rmeta .p{background:var(--bg);border-radius:6px;padding:1px 7px}.rmeta .p b{color:var(--heading)}.rv-form{background:var(--bg);border-radius:10px;flex-direction:column;gap:7px;margin:12px 0 0;padding:12px 14px;display:flex}.rv-row{align-items:center;gap:8px;font-size:13px;font-weight:600;display:flex}.rv-form select,.rv-form input,.rv-form textarea{font:inherit;border:1px solid var(--line);background:var(--panel);color:var(--heading);border-radius:7px;padding:6px 9px;font-size:13px}.rv-form textarea{resize:vertical;min-height:44px}.rv-err{color:#c2410c;margin:0;font-size:12.5px}.rv-note{color:var(--muted);margin:0;font-size:12.5px;line-height:1.5}.rv-note code,.rv-err code{background:var(--line);border-radius:4px;padding:0 4px;font-size:.92em}.rv-actions{flex-wrap:wrap;gap:8px;margin-top:2px;display:flex}.rv-actions .gm-btn{align-self:auto}.rv-actions .rv-primary{background:var(--accent);border-color:var(--accent);color:#fff}.rv-actions .rv-primary:hover{filter:brightness(1.06)}.gm-btn{font:600 12.5px var(--sans);border:1px solid var(--line);background:var(--panel);color:var(--heading);cursor:pointer;border-radius:8px;align-self:flex-start;padding:7px 14px}.gm-btn:hover{border-color:var(--muted)}.gm-btn:disabled{opacity:.6;cursor:default}.graph-modal{z-index:50;background:var(--bg);flex-direction:column;display:flex;position:fixed;inset:0}.gm-bar{border-bottom:1px solid var(--line);background:var(--panel);flex-wrap:wrap;align-items:center;gap:8px;padding:9px 16px;display:flex}.gm-bar h2{letter-spacing:0;color:var(--heading);margin:0 6px 0 0;font-size:15px;font-weight:700}.gm-bar .sp{margin-left:auto}.gm-body{flex:1;min-height:0;display:flex}.gm-wrap{flex:1;min-width:0;position:relative;overflow:hidden}.gm-wrap .gvwrap{border:none;border-radius:0;flex-direction:column;height:100%;display:flex}.gm-wrap .gv-canvas{flex:1;height:auto}#gm-side{border-left:1px solid var(--line);background:var(--bg);overflow-wrap:break-word;flex-direction:column;flex:none;width:min(470px,40vw);padding:16px;display:flex;overflow:hidden auto}#gm-side .dep-chip{overflow-wrap:anywhere;max-width:100%}#gm-side.empty{border-left:none;width:0;padding:0}#gm-side.empty .gp-close{display:none}@media (width<=860px){.gm-body{position:relative}#gm-side{z-index:6;border-top:1px solid var(--line);border-left:0;width:100%;max-height:min(58vh,520px);padding:12px;display:flex;position:absolute;inset:auto 0 0;box-shadow:0 -10px 30px #14192324}#gm-side.empty{display:none}}.gp-empty{color:var(--muted);padding:20px 16px;font-size:13px}.gp-close{float:right;z-index:2;align-self:auto;width:28px;height:28px;margin:0 0 8px 8px;padding:0;position:sticky;top:0}.gm-chip{border:1px solid var(--line);background:var(--panel);cursor:pointer;-webkit-user-select:none;user-select:none;border-radius:8px;padding:5px 10px;font-size:12px}.gm-chip.on{border-color:var(--accent);background:color-mix(in srgb, var(--accent) 8%, #fff);color:var(--accent);font-weight:600}.gm-chip:disabled{opacity:.5;cursor:default}.gm-float{border:1px solid var(--line);box-shadow:var(--shadow);background:#ffffffed;border-radius:10px;font-size:12px;position:absolute}.gm-legend{z-index:3;flex-direction:column;gap:4px;max-height:calc(100vh - 160px);padding:11px 13px;display:flex;bottom:14px;left:14px;overflow:auto}.gm-legend .lg{color:var(--heading);align-items:center;gap:8px;font-size:11.5px;display:flex}.gm-legend .lgttl{width:100%;color:var(--heading);font:700 12px/1.3 var(--sans);text-align:left;cursor:pointer;-webkit-user-select:none;user-select:none;background:0 0;border:0;grid-template-columns:1fr auto;align-items:center;padding:0;display:grid}.gm-legend .lgcar{color:var(--muted);transition:transform .15s}.gm-legend .lgsub{color:var(--muted);grid-column:1/-1;font-size:11px;font-weight:400}.gm-legend.collapsed{max-height:none}.gm-legend.collapsed>:not(.lgttl),.gm-legend.collapsed .lgsub{display:none}.gm-legend.collapsed .lgcar{transform:rotate(-90deg)}.gm-legend .lgsec{text-transform:uppercase;letter-spacing:.05em;color:var(--muted);margin:7px 0 2px;font-size:10px;font-weight:700}.gm-legend .lgshape{background:#fff;border:2px solid #607d8b;flex:none;width:15px;height:12px}.gm-legend .lgshape.rect{border-radius:3px}.gm-legend .lgshape.ell{border-radius:50%}.gm-legend .lgb{background:#fff;border:2.5px solid;border-radius:3px;flex:none;width:13px;height:11px}.gm-legend .lgf{border:1px solid var(--line);border-radius:3px;flex:none;width:13px;height:11px}.gm-legend .lge{border-top:2px solid #6e7887;flex:none;width:20px;height:0}.gm-legend .lge.dash{border-top-style:dashed}.ro{color:var(--muted);background:var(--bg);border-radius:8px;margin:12px 0 0;padding:9px 12px;font-size:12.5px}.doc-wrap{--doc-left-width:264px;--doc-right-width:250px;--doc-main-width:860px;grid-template-columns:var(--doc-left-width) minmax(0, 1fr) var(--doc-right-width);align-items:start;gap:0;max-width:1560px;margin:0 auto;transition:grid-template-columns .2s;display:grid}.doc-wrap.nav-collapsed{--doc-left-width:0px;--doc-main-width:1020px}.doc-wrap.outline-collapsed{--doc-right-width:0px;--doc-main-width:1020px}.doc-wrap.nav-collapsed.outline-collapsed{--doc-main-width:1180px}.doc-wrap.nav-collapsed .doc-nav,.doc-wrap.outline-collapsed .doc-outline{visibility:hidden;opacity:0;pointer-events:none;border:0;padding-left:0;padding-right:0;overflow:hidden}@media (width<=1240px){.doc-wrap{grid-template-columns:var(--doc-left-width) minmax(0, 1fr)}.doc-outline,.panel-rail-right{display:none}}@media (width<=900px){.doc-wrap{grid-template-columns:1fr}.doc-nav,.panel-rail-left{display:none}}.doc-nav,.doc-outline{scrollbar-gutter:stable;align-self:start;min-width:0;max-height:calc(100vh - 68px);padding:14px 10px 40px;transition:opacity .15s;position:sticky;top:58px;overflow:auto}.doc-nav{border-right:1px solid var(--line)}.doc-outline{border-left:1px solid var(--line);padding:14px 6px 40px}.doc-main{width:100%;min-width:0;max-width:var(--doc-main-width);justify-self:center;padding:10px 32px 90px;transition:max-width .2s}.navq{border:1px solid var(--line);background:var(--panel);width:100%;font:inherit;border-radius:9px;margin-bottom:10px;padding:7px 12px;font-size:13.5px}.navchips{flex-wrap:wrap;gap:5px;margin:0 0 12px;display:flex}.navchip{border:1px solid var(--line);background:var(--panel);cursor:pointer;-webkit-user-select:none;user-select:none;border-radius:8px;padding:3px 8px;font-size:11px}.navchip.on{border-color:var(--accent);background:color-mix(in srgb, var(--accent) 8%, #fff);color:var(--accent);font-weight:600}.navlinks{border-top:1px solid var(--line);flex-direction:column;gap:1px;margin:10px 0 6px;padding-top:10px;display:flex}.navlink{color:var(--heading);cursor:pointer;border-radius:8px;align-items:center;gap:9px;padding:7px 9px;font-size:13.5px;font-weight:550;display:flex}.navlink:hover{background:var(--bg)}.navlink.on{background:color-mix(in srgb, var(--accent) 10%, #fff);color:var(--accent)}.navlink .ni{color:var(--muted);text-align:center;width:16px}.navlink.on .ni{color:var(--accent)}.navsec{text-transform:uppercase;letter-spacing:.05em;color:var(--muted);border-top:1px solid var(--line);margin-top:6px;padding:12px 9px 5px;font-size:11px;font-weight:700}.tch{color:var(--heading);cursor:pointer;border-radius:7px;align-items:center;gap:6px;padding:6px 9px;font-size:13px;line-height:1.4;display:flex}.tch:hover{background:var(--bg)}.tch.sel{background:color-mix(in srgb, var(--accent) 10%, #fff);color:var(--accent);font-weight:600}.tch .n,.tsec .n{color:var(--muted);font-variant-numeric:tabular-nums;min-width:20px}.tch .c{color:var(--muted);margin-left:auto}.tsec{color:var(--muted);cursor:pointer;border-radius:7px;align-items:center;gap:6px;padding:3px 9px 3px 12px;font-size:12px;line-height:1.35;display:flex}.tsec.l3{padding-left:24px;font-size:11.5px}.tsec:hover{background:var(--bg);color:var(--accent)}.tchev,.tchev-sp{width:12px;color:var(--muted);font-size:10px;display:inline-block}main.doc-main h2.ch{letter-spacing:0;color:var(--heading);margin:16px 0 6px;font-size:25px;font-weight:750}main.doc-main h3{color:var(--heading);margin:30px 0 8px;font-size:19px;font-weight:660}main.doc-main h4{color:#374151;margin:22px 0 6px;font-size:15.5px;font-weight:680}.hn{color:var(--muted);font-variant-numeric:tabular-nums;margin-right:.4em;font-weight:600}.prose{text-align:justify;color:var(--heading);margin:12px 0}.prose p{margin:.6em 0}.prose ul,.prose ol{margin:.5em 0;padding-left:1.5em}.prose li{margin:.2em 0}li.li-lbl{margin-left:-1.15em;list-style:none}.li-mark{margin-right:.4em;font-weight:600}.env-lbl{color:var(--muted);margin-right:.3em;font-style:italic;font-weight:600}blockquote{border-left:3px solid var(--line);color:var(--heading);margin:.6em 0;padding-left:.9em}.choverview{background:var(--bg);border:1px solid var(--line);border-radius:11px;margin:12px 0 22px;padding:10px 14px}.choverview>summary{cursor:pointer;color:var(--muted);font-size:13px}.co-sec{color:var(--heading);min-width:140px;font-size:12px}.co-sec .n{color:var(--muted);margin-right:4px}.co-intro{color:var(--muted)}.co-link{font:inherit;text-align:left;cursor:pointer;background:0 0;border:0;padding:0}.co-link:hover{color:var(--accent);text-decoration:underline}.co-link:focus-visible,.ov-link:focus-visible,.mm:focus-visible{outline:2px solid var(--accent);outline-offset:2px}.mm{cursor:pointer;border:0;border-radius:3px;flex:none;width:12px;height:12px;padding:0;display:block}.mm[data-id]:hover{outline:2px solid var(--heading);outline-offset:1px}.maketitle{text-align:center;border-bottom:1px solid var(--line);margin-bottom:20px;padding:22px 0 20px}.maketitle h1{letter-spacing:0;color:var(--heading);margin:0 0 9px;font-size:30px;font-weight:750;line-height:1.22}.mkauthor{color:var(--muted);font-size:15px}.ovleg-wrap{margin-bottom:6px}.ovleg{flex-wrap:wrap;align-items:center;gap:16px;margin:14px 0 18px;font-size:12.5px;display:flex}.ovleg span{align-items:center;gap:6px;display:inline-flex}.sw{vertical-align:middle;border-radius:3px;width:11px;height:11px;margin-right:3px;display:inline-block}.ovleg .sw{border-radius:3px;width:12px;height:12px;margin-right:0}.mmcells{flex-wrap:wrap;gap:3px;display:flex}.mmcells.ov-statements{padding:0}.ov-chapter{border:1px solid var(--line);border-radius:10px;margin:0 0 8px;transition:border-color .12s}.ov-chapter:hover{border-color:color-mix(in srgb, var(--accent) 25%, var(--line))}.ov-chapter>summary{cursor:pointer;-webkit-user-select:none;user-select:none;flex-wrap:wrap;align-items:center;gap:4px 12px;padding:11px 16px;list-style:none;display:flex}.ov-chapter>summary::-webkit-details-marker{display:none}.ov-chapter>summary:before{content:"▸";color:var(--muted);width:10px;font-size:12px}.ov-chapter[open]>summary:before{content:"▾"}.ov-chapter>summary:hover .ov-chh{color:var(--accent)}.ov-sections{flex-direction:column;gap:1px;padding:2px 16px 12px 34px;display:flex}.ov-chh{color:var(--heading);cursor:pointer;letter-spacing:0;flex:none;max-width:100%;font-size:15.5px;font-weight:650}.ov-link{text-align:left;background:0 0;border:0;align-items:baseline;padding:0;font-family:inherit;display:inline-flex}.ov-chapter>summary .ov-flat,.ov-section>summary .ov-flat{width:100%;margin-top:2px}.ov-chapter[open]>summary .ov-flat,.ov-section[open]>summary .ov-flat{display:none}.ov-section{margin:0}.ov-section>summary{cursor:pointer;-webkit-user-select:none;user-select:none;border-radius:6px;flex-wrap:wrap;align-items:center;gap:4px 10px;padding:5px 8px;list-style:none;display:flex}.ov-section>summary::-webkit-details-marker{display:none}.ov-section>summary:before{content:"▸";color:var(--muted);width:9px;font-size:10px}.ov-section[open]>summary:before{content:"▾"}.ov-section>summary:hover,.ov-section-h:hover{background:var(--soft)}.ov-section-h{border-radius:6px;flex-wrap:wrap;align-items:center;gap:4px 10px;padding:5px 8px 5px 17px;display:flex}.ov-subsections{flex-direction:column;gap:1px;padding:2px 0 4px 24px;display:flex}.ov-subsection{border-radius:6px;flex-wrap:wrap;align-items:center;gap:4px 10px;padding:4px 8px 4px 17px;display:flex}.ov-subsection:hover{background:var(--soft)}.ov-section>summary .co-sec,.ov-section-h .co-sec,.ov-subsection .co-sec{flex:0 auto;min-width:0}.stmt{background:var(--panel);border:1px solid var(--line);border-left:3px solid var(--empty);box-shadow:var(--shadow);border-radius:11px;margin:15px 0;padding:13px 16px;scroll-margin-top:16px}.stmt.k-definition,.stmt-card.k-definition{border-left-color:#0b5fd0}.stmt.k-theorem,.stmt-card.k-theorem{border-left-color:#7c3aed}.stmt.k-lemma,.stmt-card.k-lemma{border-left-color:#0d9488}.stmt.k-proposition,.stmt-card.k-proposition{border-left-color:#b45309}.stmt.k-corollary,.stmt-card.k-corollary{border-left-color:#db2777}.stmt.k-remark,.stmt-card.k-remark{border-left-color:#6b7280}.stmt.k-example,.stmt-card.k-example{border-left-color:#0891b2}.stmt.k-conjecture,.stmt-card.k-conjecture{border-left-color:#9333ea}.stmt.sel{box-shadow:0 0 0 2px var(--accent), var(--shadow)}.blk-pending{opacity:.55;min-height:96px;animation:1.4s ease-in-out infinite blk-pulse}.blk-pending-prose{background:var(--soft);border:none;border-radius:8px;min-height:40px;margin:12px 0}@keyframes blk-pulse{0%,to{opacity:.55}50%{opacity:.3}}.sh{flex-wrap:wrap;align-items:baseline;gap:8px;display:flex}.tag{background:var(--bg);color:#111827;cursor:pointer;white-space:nowrap;border-radius:6px;padding:1px 8px;font-size:12.5px;font-weight:700}.tag.k-definition{color:#0b5fd0;background:#e2f0ff}.tag.k-theorem{color:#7c3aed;background:#f1e9ff}.tag.k-lemma{color:#0d9488;background:#d5f3ee}.tag.k-proposition{color:#b45309;background:#fdeede}.tag.k-corollary{color:#db2777;background:#fde7f1}.tag.k-remark{color:#6b7280;background:#eef0f3}.tag.k-example{color:#0891b2;background:#dcf5fb}.tag.k-conjecture{color:#9333ea;background:#f3e8ff}.stmt-card .stmt-kind{cursor:default;text-transform:none;letter-spacing:0}.st{color:#374151;font-style:italic}.badges{flex-wrap:wrap;gap:5px;margin-left:auto;display:flex}.b{white-space:nowrap;border-radius:7px;padding:2px 8px;font-size:11px;font-weight:600}.b-lean_ok{background:var(--lean-bg);color:var(--lean)}.b-mathlib_ok{background:var(--mathlib-bg);color:var(--mathlib)}.b-sorry{background:var(--sorry-bg);color:var(--sorry)}.b-empty{background:var(--empty-bg);color:var(--empty)}.reftag{background:var(--bg);color:var(--muted);white-space:nowrap;border-radius:7px;padding:2px 8px;font-size:11px;font-weight:600}.sketchtag{color:#92400e;white-space:nowrap;background:#fdf0d5;border-radius:7px;padding:2px 8px;font-size:11px;font-style:normal;font-weight:600}details.proof>summary .sketchtag{margin-left:7px}.sbody{text-align:justify;color:var(--heading);margin:9px 0 2px}.smeta{color:var(--muted);flex-wrap:wrap;align-items:center;gap:6px;margin-top:10px;font-size:12.5px;display:flex}.mtag{background:var(--bg);color:var(--muted);white-space:nowrap;font-variant-numeric:tabular-nums;border:1px solid #0000;border-radius:7px;padding:2px 9px;font-size:11.5px}.mtag.lean{background:var(--lean-bg);color:var(--lean)}.mtag.mathlib{background:var(--mathlib-bg);color:var(--mathlib)}details.stmt-detail{white-space:normal;background:0 0;border:0;margin:0;padding:0}details.stmt-detail[open]{flex-basis:100%}details.stmt-detail>summary{cursor:pointer;list-style:none;transition:border-color .15s,color .15s;display:inline-block}details.stmt-detail>summary::-webkit-details-marker{display:none}details.stmt-detail>summary::marker{content:""}details.stmt-detail>summary:after{content:"▸";margin-left:5px;font-size:10px}details.stmt-detail[open]>summary:after{content:"▾"}details.stmt-detail>summary:hover{border-color:var(--accent);color:var(--heading)}.stmt-detail-body{background:var(--panel);border:1px solid var(--line);color:var(--heading);border-radius:8px;margin-top:8px;padding:10px 11px}.stmt-deps-body{grid-template-columns:repeat(2,minmax(0,1fr));gap:14px;display:grid}.stmt-detail-label{color:var(--muted);letter-spacing:.05em;text-transform:uppercase;margin-bottom:6px;font-size:10.5px;font-weight:700}.stmt-detail-links{flex-direction:column;gap:4px;display:flex}.stmt-detail-link{background:var(--bg);width:100%;color:var(--heading);font:inherit;text-align:left;cursor:pointer;border:1px solid #0000;border-radius:6px;padding:5px 7px;font-size:12.5px;line-height:1.4;display:block}.stmt-detail-link:hover{border-color:var(--accent);color:var(--accent)}.stmt-detail-link:focus-visible{outline:2px solid var(--accent);outline-offset:1px}.stmt-detail-empty{color:var(--muted);font-size:12px}.stmt-lean-body{flex-direction:column;gap:8px;display:flex}.stmt-lean-body .lean-block{border:1px solid var(--line)}.stmt-mathlib-body code{overflow-wrap:anywhere}.mtag.graph-open{border-color:var(--line);cursor:pointer;align-items:center;gap:5px;font-family:inherit;display:inline-flex}.mtag.graph-open:hover{border-color:var(--accent);color:var(--accent);background:color-mix(in srgb, var(--accent) 7%, var(--panel))}.entry-graph-btn{border:1px solid var(--line);background:var(--panel);width:24px;height:24px;color:var(--muted);cursor:pointer;border-radius:6px;justify-content:center;align-items:center;padding:0;display:inline-flex}.entry-graph-btn:hover{border-color:var(--accent);color:var(--accent)}.mtag.rv{white-space:normal;background:0 0;border:none;padding:0}.mtag.rv>summary{background:var(--bg);color:var(--muted);cursor:pointer;white-space:nowrap;font-variant-numeric:tabular-nums;border:1px solid #0000;border-radius:7px;padding:2px 9px;font-size:11.5px;font-weight:500;list-style:none;display:inline-block}.mtag.rv>summary::-webkit-details-marker{display:none}.mtag.rv>summary::marker{content:""}.mtag.rv>summary:hover{border-color:var(--accent);color:var(--heading)}.mtag.rv[open]{flex-basis:100%}.mtag.rv[open]>summary{color:var(--heading);border-color:var(--line);margin-bottom:8px}.tex-bold{color:var(--emphasis)}.tex-link{color:var(--accent);text-decoration:underline;-webkit-text-decoration-color:color-mix(in srgb, var(--accent) 42%, transparent);text-decoration-color:color-mix(in srgb, var(--accent) 42%, transparent);text-underline-offset:.16em;text-decoration-thickness:1px;transition:color .15s,text-decoration-color .15s}.tex-url{overflow-wrap:anywhere}.tex-link:hover{color:color-mix(in srgb, var(--accent) 78%, #111827);text-decoration-color:currentColor}.tex-link:focus-visible{outline:2px solid var(--accent);outline-offset:2px;border-radius:2px}.ref{color:var(--accent);cursor:pointer;white-space:nowrap;font-weight:550}.ref:hover{text-decoration:underline}.leanref{cursor:help}.cite{color:var(--accent);cursor:pointer;white-space:nowrap}.cite:hover{text-decoration:underline}.xref{color:var(--muted)}.extref{color:var(--accent);font-weight:550;text-decoration:none}.extref:after{content:"↗";opacity:.7;margin-left:1px;font-size:.82em}.extref:hover{text-decoration:underline}.extref-dead{color:var(--muted)}.extref-dead:after{content:none}.prose code,.sbody code,.stmt-body code{background:var(--bg);border-radius:5px;padding:1px 5px;font-family:ui-monospace,SFMono-Regular,Menlo,monospace;font-size:.86em}details.proof{margin:6px 0 16px}details.proof>summary{cursor:pointer;color:var(--muted);-webkit-user-select:none;user-select:none;font-size:14px;font-style:italic;list-style:none}details.proof>summary:before{content:"▸ ";font-style:normal}details.proof[open]>summary:before{content:"▾ "}details.proof .pbody{border-left:2px solid var(--line);text-align:justify;margin:9px 0;padding:2px 0 2px 15px}.olh{text-transform:uppercase;letter-spacing:.05em;color:var(--muted);padding:2px 8px 9px;font-size:11px;font-weight:700}.olc{color:var(--heading)}.olist{flex-direction:column;gap:7px;display:flex}.olsec{color:var(--muted);padding:11px 8px 3px;font-size:11px;font-weight:600}.oempty{color:var(--muted);padding:8px;font-size:12.5px}.omini{border:1px solid var(--line);border-left:3px solid var(--empty);cursor:pointer;background:var(--panel);border-radius:8px;margin:0 2px;padding:6px 9px 7px;display:block}.omini:hover{border-color:var(--accent)}.omini.cur{box-shadow:0 0 0 2px color-mix(in srgb, var(--accent) 30%, #fff)}.omini.k-definition{border-left-color:#0b5fd0}.omini.k-theorem{border-left-color:#7c3aed}.omini.k-lemma{border-left-color:#0d9488}.omini.k-proposition{border-left-color:#b45309}.omini.k-corollary{border-left-color:#db2777}.omini.k-remark{border-left-color:#6b7280}.omini.k-example{border-left-color:#0891b2}.omini.k-conjecture{border-left-color:#9333ea}.omini-h{align-items:center;gap:5px;display:flex}.omini .tag{padding:0 6px;font-size:10px}.omini-b{align-items:center;gap:3px;margin-left:auto;display:flex}.omini-b .b{padding:1px 5px;font-size:9px}.otitle2{color:#374151;-webkit-line-clamp:2;-webkit-box-orient:vertical;margin-top:4px;font-size:11.5px;line-height:1.35;display:-webkit-box;overflow:hidden}pre.lean{border:1px solid var(--line);background:#f8f9fb;border-radius:8px;margin:4px 0;padding:10px 12px;font-family:ui-monospace,SFMono-Regular,Menlo,monospace;font-size:12.5px;line-height:1.55;overflow-x:auto}.c-kw{color:#8250df;font-weight:600}.c-cm{color:#6b7280;font-style:italic}.side-panel{background:var(--panel);border:1px solid var(--line);box-shadow:var(--shadow);border-radius:14px;max-height:calc(100vh - 24px);padding:20px;position:sticky;top:12px;overflow:auto}.pv{background:var(--panel);border:1px solid var(--line);pointer-events:auto;max-width:480px;max-height:72vh;color:var(--heading);border-radius:11px;padding:12px 14px;font-size:13.5px;overflow:auto;box-shadow:0 10px 34px #14192333}.pv pre.lean{white-space:pre-wrap;word-break:break-word}.pv .pk{text-transform:uppercase;letter-spacing:.05em;color:var(--muted);font-size:10px;font-weight:700}.pv .pt{margin:2px 0 5px;font-style:italic;font-weight:640}.gwrap{border:1px solid var(--line);background:var(--bg);border-radius:9px;overflow-x:auto}.graph{display:block}.gn{cursor:pointer}.gn text{font-size:11px}.gvwrap{border:1px solid var(--line);background:var(--bg);border-radius:11px;overflow:hidden}.gv-toolbar{border-bottom:1px solid var(--line);background:var(--panel);align-items:center;gap:10px;padding:9px 14px;display:flex}.gv-hint{color:var(--muted);font-size:12px}.gv-canvas{cursor:grab;touch-action:none;justify-content:center;align-items:center;height:70vh;display:flex;position:relative;overflow:hidden}.gv-canvas:active{cursor:grabbing}.gv-inner{transform-origin:50%;will-change:transform;flex:none}.gv-inner svg{display:block;overflow:visible}.gv-inner .node{cursor:pointer}.gv-inner .node,.gv-inner .edge{transition:opacity .12s}.gv-inner .node:hover path,.gv-inner .node:hover ellipse{stroke-width:3px}.gv-inner .cluster{cursor:pointer}.gv-inner g.node.gm-node-dependency polygon,.gv-inner g.node.gm-node-dependency ellipse,.gv-inner g.node.gm-node-dependency path{stroke:#2563eb!important;stroke-width:3px!important}.gv-inner g.node.gm-node-dependent polygon,.gv-inner g.node.gm-node-dependent ellipse,.gv-inner g.node.gm-node-dependent path{stroke:#f59e0b!important;stroke-width:3px!important}.gv-inner g.node.gm-node-selected polygon,.gv-inner g.node.gm-node-selected ellipse,.gv-inner g.node.gm-node-selected path{stroke:#111827!important;stroke-width:3.2px!important}.gv-inner g.edge.gm-edge-incoming path{stroke:#2563eb!important;stroke-width:2.8px!important}.gv-inner g.edge.gm-edge-incoming polygon{stroke:#2563eb!important;fill:#2563eb!important}.gv-inner g.edge.gm-edge-outgoing path{stroke:#f59e0b!important;stroke-width:2.8px!important}.gv-inner g.edge.gm-edge-outgoing polygon{stroke:#f59e0b!important;fill:#f59e0b!important}.gm-sel{border:1px solid var(--line);background:var(--panel);font:inherit;color:var(--heading);border-radius:8px;padding:6px 10px;font-size:13px}.gm-q{border:1px solid var(--line);background:var(--panel);font:inherit;border-radius:8px;min-width:150px;padding:6px 10px;font-size:13px}.gm-count{color:var(--muted);pointer-events:none;z-index:3;padding:6px 11px;top:14px;right:14px}.gm-count b{color:var(--heading)}.gm-hint{color:var(--muted);pointer-events:none;z-index:3;max-width:60%;padding:7px 11px;font-size:12px;bottom:14px;right:14px}.gm-gvload{color:var(--heading);background:color-mix(in srgb, var(--bg) 55%, transparent);pointer-events:none;justify-content:center;align-items:center;font-size:13px;display:flex;position:absolute;inset:0}.gm-gvload>div{background:var(--panel);border:1px solid var(--line);box-shadow:var(--shadow);border-radius:9px;padding:8px 14px}.sumgrid{flex-wrap:wrap;gap:12px;margin:16px 0 24px;display:flex}.sumcard{background:var(--panel);border:1px solid var(--line);min-width:104px;box-shadow:var(--shadow);border-radius:11px;flex:1;padding:12px 14px}.sumcard .v{letter-spacing:0;font-size:24px;font-weight:750}.sumcard .l{margin-top:2px;font-size:12.5px;font-weight:600}.sumcard .s{color:var(--muted);margin-top:4px;font-size:11px;line-height:1.4}.sumsec{letter-spacing:0;margin:28px 0 6px;font-size:15px;font-weight:700}.stmt.sum{cursor:pointer;box-shadow:none;margin:8px 0;padding:10px 14px}.stmt.sum:hover{border-color:var(--accent)}.stmt.sum .rmeta{margin-top:7px}.morebtn{color:var(--accent);cursor:pointer;margin:12px 0;font-size:12.5px;font-weight:600}.morebtn:hover{text-decoration:underline}.sumtable{border-collapse:collapse;width:100%;font-size:13px}.sumtable th{text-align:left;text-transform:uppercase;letter-spacing:.05em;color:var(--muted);border-bottom:1px solid var(--line);padding:7px 8px;font-size:11px;font-weight:700}.sumtable td{border-bottom:1px solid var(--line);vertical-align:middle;padding:9px 8px}.sumtable td a{color:var(--heading);cursor:pointer}.sumtable td a:hover{color:var(--accent)}.segbar{background:var(--bg);border-radius:5px;flex:none;width:150px;height:9px;display:flex;overflow:hidden}.segbar>i{height:100%;display:block}.bibitem{border-bottom:1px solid var(--line);padding:13px 2px}.bibitem .bi-t{line-height:1.55}.bibitem .bi-n{color:var(--muted);font-variant-numeric:tabular-nums;margin-right:2px;font-weight:700}.bibitem .bi-c{color:var(--muted);margin-top:5px;font-size:12.5px}.bibitem .bi-c .citeloc{font-variant-numeric:tabular-nums}.stmt.flash,.bibitem.flash,.prose.flash,details.proof.flash,.katex-display.flash{border-radius:6px;animation:1.7s flash}.eqa{height:0;scroll-margin-top:80px;display:block}@keyframes flash{0%,20%{background:#fff6d6}to{background:var(--panel)}}@media (prefers-reduced-motion:reduce){.doc-wrap,.doc-main,.doc-nav,.doc-outline,.panel-toggle,.tex-link,details.stmt-detail>summary{transition:none}}@media (width<=620px){.stmt-deps-body{grid-template-columns:1fr}}