:root{font-family:IBM Plex Sans,-apple-system,BlinkMacSystemFont,Segoe UI,sans-serif;color:#13202a;background:#fbfcfc;font-synthesis:none;font-size:16px;--ink: #13202a;--muted: #5d6b75;--line: #dce3e7;--control: #85949f;--space-1: 8px;--space-2: 16px;--space-3: 24px;--space-4: 32px;--teal: #1d5d74;--display: "Newsreader", "Iowan Old Style", Georgia, serif;--mono: "IBM Plex Mono", "SFMono-Regular", Menlo, monospace;color-scheme:light;-webkit-font-smoothing:antialiased}*,*:before,*:after{box-sizing:border-box}html{-webkit-text-size-adjust:100%}body{line-height:1.55;margin:0}button,input,select{font:inherit;color:inherit}button,a,input,select{-webkit-tap-highlight-color:transparent}button{cursor:pointer;border:0;background:none}button:disabled{cursor:default}a{color:var(--teal);text-decoration:none}a:hover{text-decoration:underline;text-underline-offset:3px}button:focus-visible,a:focus-visible,input:focus-visible,select:focus-visible,[tabindex]:focus-visible{outline:2px solid #2b7fa0;outline-offset:3px}h1,h2,h3,p{margin:0}h1,h2,h3{font-family:var(--display);font-weight:500;line-height:1.2;letter-spacing:-.01em}h1{font-size:clamp(2rem,4.2vw,2.6rem)}h2{font-size:1.75rem}h3{font-size:1.25rem}p{line-height:1.6}small{font-size:.75rem}code,pre{font-family:var(--mono)}.math{font-family:var(--display)}.shell{max-width:1152px;margin:0 auto;padding:0 20px}main{min-width:0}.topbar{display:flex;align-items:center;justify-content:space-between;gap:20px;padding:24px 0;border-bottom:1px solid var(--line)}.brand{display:inline-flex;align-items:center;gap:10px;color:var(--ink);font-family:var(--display);font-size:1.35rem;font-weight:500;white-space:nowrap}.header-links{display:flex;align-items:center;gap:24px;font-size:.875rem}.header-links a,.header-links button{color:#475661;padding:0}.header-links button:hover{color:var(--teal);text-decoration:underline;text-underline-offset:3px}.header-links .github-badge{display:inline-flex;align-items:center;gap:7px;padding:6px 10px;border:1px solid #c9d2d7;border-radius:4px;background:#fff;color:var(--ink);font-weight:500}.header-links .github-badge:hover{background:#f2f5f6;text-decoration:none}.header-links .pr-button{display:inline-flex;align-items:center;gap:7px;padding:0 8px;height:36px;border-radius:4px}.header-links .pr-button:hover{background:#f2f5f6}.content{padding:var(--space-4) 0}.bound-summary{--line: #ccdbe2;display:grid;grid-template-columns:minmax(0,1fr) auto;gap:0;align-items:stretch;margin-bottom:32px;overflow:hidden;border:1px solid var(--line);border-radius:6px;background:#f2f6f8}.qrh-statement{padding:24px;min-width:0}.qrh-statement p{font-size:.875rem;color:#475661}.statement-equation-row{display:flex;align-items:center;gap:12px;margin-top:18px}.statement-equation,.statement-description,.best-bound{font-size:1.4rem}.statement-description{font-family:var(--display);font-weight:400;line-height:1.5;color:var(--ink)}.current-bound{display:flex;align-items:center;justify-content:center;padding:24px;border-left:1px solid var(--line);background:#fbfdfe}.best-bound{padding:0;color:var(--teal);text-align:left}.best-bound:hover{color:var(--ink)}.current-bound>p{font-size:.8125rem;color:var(--muted);margin-top:14px}.view-nav{display:flex;gap:26px;border-bottom:1px solid var(--line);margin-bottom:24px}.view-nav button{display:flex;align-items:center;gap:7px;padding:10px 0 12px;margin-bottom:-1px;font-size:.875rem;color:#475661;border-bottom:2px solid transparent}.view-nav button:hover{color:var(--ink)}.view-nav button[aria-current=page]{color:var(--teal);border-bottom-color:var(--teal);font-weight:500}.view-nav small{color:var(--muted);font-variant-numeric:tabular-nums}.icon{min-width:36px;min-height:36px;display:inline-grid;place-items:center;padding:6px;border-radius:4px;color:#475661;flex-shrink:0}.icon:hover{background:#f2f5f6}select{border:1px solid #c9d2d7;background:#fff;border-radius:4px;padding:8px 28px 8px 10px;font-size:.8125rem;max-width:100%;color:#475661}.research-layout{display:grid;grid-template-columns:minmax(0,1fr);gap:32px;align-items:start}.research-main,.panel{min-width:0}.panel-heading{display:flex;align-items:center;justify-content:space-between;gap:12px;padding:0 0 16px}.eyebrow{display:block;font-family:IBM Plex Sans,sans-serif;font-size:.75rem;letter-spacing:.08em;font-weight:500;color:var(--muted)}.panel-heading .eyebrow{margin-bottom:6px}.chart-panel{position:relative}.chart-toolbar{position:absolute;right:0;top:0;z-index:1;display:flex;justify-content:flex-end;align-items:center;gap:10px;margin-bottom:8px}.chart-tools{display:flex;align-items:center;gap:4px}.chart-panel .chart-toolbar{position:static;justify-content:flex-end}.chart-tools .icon{border:1px solid var(--control);background:#fff;width:36px;height:36px}.chart-tools .icon:hover{background:#f2f5f6}.chart-wrap{position:relative}.chart{display:block;width:100%;height:355px;touch-action:none;cursor:grab}.axis{font-size:12px;fill:var(--muted);font-family:var(--mono)}.axis-label,.point-label{font-size:12px;fill:#475661}.dot{cursor:pointer}.dot:hover circle:last-of-type,.dot:focus circle:last-of-type{stroke:var(--teal);stroke-width:3px}.chart-empty{position:absolute;top:47%;left:55%;transform:translate(-50%,-50%);width:80%;text-align:center;pointer-events:none}.chart-empty>*{pointer-events:auto}.empty-mark{display:block;font:2rem var(--display);color:var(--muted);margin-bottom:12px}.chart-empty h3{font-size:1.25rem;background:#fbfcfced}.chart-empty p{font-size:.8125rem;color:var(--muted);margin-top:9px;background:#fbfcfced}.chart-tooltip{position:absolute;left:24px;bottom:55px;display:flex;flex-direction:column;gap:5px;background:var(--ink);color:#fff;padding:10px 12px;border-radius:4px;font-size:.75rem;pointer-events:none;max-width:calc(100% - 48px);z-index:3}.chart-tooltip span{color:#d7e3e9}.chart-tooltip small{color:#efd9a1}.chart-bottom{display:flex;flex-wrap:wrap;align-items:center;gap:10px 20px;padding:6px 0 16px;font-size:.75rem;color:#475661}.chart-bottom>span{display:flex;align-items:center;gap:7px}.legend-line{height:2px;width:18px;background:var(--teal)}.legend-dot{height:8px;width:8px;border-radius:50%;background:#7184a2}.pending-dot{background:#fff;border:2px solid #ad761e}.pan-hint{margin-left:auto;color:var(--muted)}.chart-note{display:flex;gap:8px;align-items:flex-start;font-size:.75rem;color:var(--muted);padding:8px 0 0;line-height:1.6}.chart-note svg{flex-shrink:0;margin-top:2px}.chart-note span{min-width:0;overflow-wrap:anywhere}.contribution-list{margin-top:28px}.contribution-list:first-child{margin-top:0}.leaderboard-sort{display:flex;align-items:center;gap:20px;border-bottom:1px solid var(--line);color:var(--muted);font-size:.8125rem}.leaderboard-sort button{display:inline-flex;align-items:center;gap:6px;min-height:44px;padding:0}.leaderboard-sort button[aria-pressed=true]{color:var(--ink)}.leaderboard{list-style:none;padding:0;margin:0}.leaderboard-entry{border-bottom:1px solid var(--line);min-width:0;scroll-margin-block:16px}.entry-summary{position:relative}.entry-toggle{display:flex;flex-direction:column;gap:8px;width:100%;min-width:0;padding:16px 0;text-align:left;color:var(--ink)}.entry-toggle:hover .entry-decimal,.entry-toggle[aria-expanded=true] .entry-decimal{color:var(--teal)}.entry-heading{display:flex;align-items:center;gap:10px;width:100%;padding-right:80px}.entry-decimal{font:500 1.25rem/1.4 var(--mono);overflow:hidden;text-overflow:ellipsis;white-space:nowrap}.entry-chevron{flex-shrink:0;color:var(--muted)}.entry-toggle[aria-expanded=true] .entry-chevron{transform:rotate(180deg)}.entry-meta{display:grid;grid-template-columns:minmax(0,1fr) minmax(0,1.5fr) max-content;align-items:baseline;gap:12px;width:100%;font-size:.8125rem;color:#475661}.entry-meta>span{overflow:hidden;text-overflow:ellipsis;white-space:nowrap}.entry-exact{font-family:var(--mono);font-size:.75rem}.entry-meta time{white-space:nowrap}.entry-method{width:100%;overflow:hidden;text-overflow:ellipsis;white-space:nowrap;font-size:.8125rem;line-height:1.6;color:var(--muted)}.entry-actions{display:flex;align-items:center;position:absolute;top:10px;right:0;gap:4px}.entry-actions .tag,.entry-actions .source-link{display:inline-flex;align-items:center;justify-content:center;width:36px;height:40px;padding:0;background:transparent}.entry-actions .tag:before{display:none}.entry-actions a:hover{background:#e5eff3}.source-link{color:#475661}.off-frontier .entry-toggle,.off-frontier .entry-decimal,.off-frontier .entry-chevron,.off-frontier .entry-meta,.off-frontier .entry-method,.off-frontier .entry-actions .tag,.off-frontier .entry-actions .source-link{color:#6b7378}.entry-details{position:relative;padding:20px;margin-bottom:16px;background:#f1f6f7;border-radius:6px;overflow-wrap:anywhere}.tag{display:inline-flex;align-items:center;gap:7px;font-size:.8125rem;font-weight:500;color:#475661}.tag:before{content:"";width:6px;height:6px;flex-shrink:0;border-radius:50%;background:currentColor}.tag.teal{color:#25613c}.tag.amber{color:#80560e}.empty-table{padding:36px 20px;text-align:center;color:var(--muted)}.empty-table h3{color:#475661;margin:10px 0}.empty-table p{font-size:.8125rem;max-width:390px;margin:auto}.empty-table button{margin-top:14px;color:var(--teal)}.proof-detail{min-width:0}.proof-detail .panel-heading{position:absolute;top:12px;right:12px;padding:0}.proof-detail .eyebrow{margin:0}.detail-body{padding-top:0}.detail-body h2{padding-right:32px;font-size:1.25rem;line-height:1.3}.detail-body p{font-size:.8125rem;color:#475661;margin:10px 0 16px}.detail-body .authors{color:var(--muted)}.exact-result{padding:16px 0;margin-top:12px;border-top:1px solid var(--line);border-bottom:1px solid var(--line)}.exact-result span,.detail-label{font-size:.8125rem;letter-spacing:.08em;color:var(--muted)}.exact-result strong{font:500 1.5rem/1.3 var(--display);display:block;color:var(--teal);margin:8px 0;overflow-wrap:anywhere}.exact-result code{display:block;font-size:.8125rem;color:#475661;overflow-wrap:anywhere}.detail-body h3{font-family:IBM Plex Sans,sans-serif;font-size:.8125rem;font-weight:500;margin:24px 0 8px}pre{background:#f2f5f6;padding:14px;border:1px solid var(--line);border-radius:4px;white-space:pre-wrap;overflow-wrap:anywhere;font:.75rem/1.7 var(--mono);color:#475661;margin:14px 0 18px}.proof-detail pre{padding:10px;font-size:.8125rem}dl{display:grid;grid-template-columns:auto minmax(0,1fr);gap:10px;font-size:.75rem;margin:16px 0 24px}dt{color:var(--muted)}dd{margin:0;text-align:right;color:#475661;overflow-wrap:anywhere;line-height:1.5}.detail-label{display:block;margin:20px 0 6px}.hash{display:block;font-size:.8125rem;overflow-wrap:anywhere;color:#475661;line-height:1.6}.detail-links{display:flex;flex-direction:column;gap:10px;font-size:.8125rem;margin-top:20px}.detail-links a,.predecessor{display:flex;align-items:center;gap:7px}.predecessor{color:var(--teal);font-size:.75rem;padding:6px 0;overflow-wrap:anywhere;text-align:left}.reference{font-size:.8125rem;display:block;margin:10px 0;overflow-wrap:anywhere}.muted{color:var(--muted)}.protocol-grid{display:grid;grid-template-columns:minmax(0,1fr);max-width:76ch;gap:32px}.protocol-grid article{border-top:1px solid var(--line);padding-top:20px}.protocol-grid h2{font-size:1.5rem;margin-bottom:14px}.protocol-grid p{font-size:.9375rem;color:#475661;margin-top:10px}.protocol-grid .statement-equation{font-size:.9375rem}.protocol-grid h3{font-family:IBM Plex Sans,sans-serif;font-size:.9375rem;font-weight:500;margin:24px 0 12px}.lean-code{margin-top:16px;border:1px solid var(--line);border-radius:4px;overflow:hidden;background:#fff}.lean-code-heading{display:flex;align-items:center;justify-content:space-between;gap:12px;padding:10px 16px;border-bottom:1px solid var(--line);background:#f2f5f6;font-size:.8125rem;color:var(--muted)}.lean-code-heading a{display:inline-flex;align-items:center;gap:6px}.lean-code pre{margin:0;border:0;border-radius:0;padding:16px;font-size:.9375rem;line-height:1.7}.protocol-grid a{font-size:.875rem}dialog{width:min(680px,calc(100vw - 32px));border:1px solid #c9d2d7;border-radius:6px;padding:32px;color:var(--ink);background:#fbfcfc;max-height:90vh}dialog::backdrop{background:#13202a66}.dialog-close{position:absolute;right:14px;top:14px}dialog>h2{font-size:1.8rem;margin:8px 20px 18px 0}dialog p{font-size:.9375rem;color:#475661;margin:12px 0}dialog .protocol-grid{grid-template-columns:minmax(0,1fr);gap:24px}dialog .protocol-grid h2{font-size:1.35rem}.guide-list{padding-left:20px;font-size:.875rem;line-height:1.7;color:#475661}.guide-list li{padding:6px 0}.notice-text{font-size:.8125rem}.notice{padding:12px 16px;border:1px solid var(--line);margin-bottom:24px;font-size:.8125rem}.error{background:#fff0ed;border-color:#e9b9ae}.check{display:flex;align-items:center;gap:5px;font-size:.75rem;color:#475661}.check input{accent-color:var(--teal)}.sr-only{position:absolute;width:1px;height:1px;padding:0;margin:-1px;overflow:hidden;clip:rect(0,0,0,0);white-space:nowrap;border:0}@media(max-width:980px){.bound-summary{grid-template-columns:minmax(0,1fr)}.current-bound{border-left:0;border-top:1px solid var(--line);padding:24px}.pan-hint{display:none!important}}@media(max-width:640px){.qrh-statement,.current-bound{padding:20px 16px}.shell{padding:0 16px}.topbar{flex-wrap:wrap;padding:18px 0;gap:12px}.brand{font-size:1.2rem}.header-links{gap:14px;font-size:.75rem}.content{padding-top:28px}.view-nav{gap:22px}.view-nav button{font-size:.8125rem}h2{font-size:1.5rem}.panel-heading{flex-wrap:wrap}.panel-heading select{font-size:.75rem}.chart-bottom{gap:8px 16px}.chart-empty{left:52%;width:90%}.entry-meta{gap:8px;font-size:.75rem}.entry-exact{font-size:.6875rem}.entry-details{padding:16px}.statement-equation,.statement-description,.best-bound{font-size:clamp(1rem,4.8vw,1.4rem)}.statement-equation-row{gap:6px;flex-wrap:wrap}.chart-tools .icon{width:40px;height:40px}.protocol-grid{grid-template-columns:minmax(0,1fr);gap:28px}dialog{padding:26px 20px}}.tag.historical{color:#56677f;background:#edf1f6}