:root{--paper:#f6f4ec;--ink:#193e3b;--muted:#586a64;--line:#cdd5c9;--teal:#146b62;--light:#e4ede2;--orange:#a54829;--white:#fffcf7;--shadow:0 10px 32px #193e3b06;font-family:Arial,Helvetica,sans-serif;color:var(--ink);background:var(--paper);font-size:16px;scroll-behavior:smooth}*{box-sizing:border-box}body{margin:0}a{color:var(--teal);text-underline-offset:4px}a:hover{color:var(--orange)}button,input,select{font:inherit}button,select{cursor:pointer}button{color:var(--ink);border:1px solid var(--line);background:var(--white);border-radius:6px;padding:10px 15px;line-height:1.4}button:hover{border-color:var(--teal);background:var(--light)}button:focus-visible,a:focus-visible,input:focus-visible,select:focus-visible,summary:focus-visible{outline:3px solid var(--orange);outline-offset:4px}button:disabled{opacity:.45;cursor:default}h1,h2{font-family:Georgia,'Times New Roman',serif;font-weight:400;letter-spacing:-.045em;line-height:1.08}h1{font-size:clamp(56px,6vw,82px);margin:18px 0 24px}h1 em{color:var(--teal);font-weight:400}h2{font-size:clamp(32px,3.7vw,50px);margin:10px 0 25px}h3{font-size:21px;line-height:1.3;letter-spacing:-.03em}p{line-height:1.75;margin:0 0 18px}header,main,footer{max-width:1280px;margin:auto}header{display:flex;justify-content:space-between;align-items:center;padding:26px 40px;border-bottom:1px solid var(--line);gap:20px}.brand{font-weight:bold;font-size:24px;display:flex;align-items:center;gap:2px;text-decoration:none;color:var(--ink)}.brand>span:first-child{color:var(--orange);font-size:35px}.brand-name{font-size:13px;margin-left:12px;letter-spacing:-.015em}nav{display:flex;gap:25px;font-size:14px;flex-wrap:wrap}nav a{text-decoration:none;color:var(--ink)}main{padding:0 40px}.hero{display:grid;grid-template-columns:1.12fr 1fr;gap:70px;padding:80px 0 74px;align-items:center}.eyebrow{font-size:11px;text-transform:uppercase;letter-spacing:.15em;font-weight:700;color:var(--muted);margin-bottom:15px}.lede{font-size:19px;max-width:590px;line-height:1.65}.hero-links{display:flex;flex-direction:column;align-items:flex-start;gap:21px;margin-top:26px;font-size:13px}.button{display:inline-flex;align-items:center;justify-content:space-between;gap:28px;padding:16px 21px;border-radius:6px;text-decoration:none}.primary{background:var(--ink);color:white}.primary:hover{background:var(--teal);color:white}.theorem{border:1px solid var(--line);border-radius:18px;padding:36px 28px 25px;background:var(--light);transform:rotate(-1deg)}.theorem>*{transform:rotate(1deg)}.big-equation{font-family:Georgia,serif;white-space:nowrap;letter-spacing:-.055em;font-size:clamp(28px,3.4vw,46px);padding:20px 0 35px}.big-equation sub{font-size:.48em}.equation-labels{display:grid;grid-template-columns:1fr 1fr;gap:18px;font-size:13px;line-height:1.5}.equation-labels strong{font-size:17px}.scope{border-top:1px solid #bdcbbd;padding-top:20px;margin:12px 0 20px;display:flex;flex-wrap:wrap;gap:9px}.scope span{border:1px solid #bccaba;font-size:11px;border-radius:30px;padding:6px 9px}.small{font-size:12px;color:var(--muted);line-height:1.65}.rule{border-top:1px solid var(--line);padding:55px 0 62px;scroll-margin-top:24px}.columns{display:grid;grid-template-columns:1fr 1fr;gap:55px}.intro{padding-bottom:30px}.section-head{display:grid;grid-template-columns:1.25fr 1fr;gap:70px;align-items:start;margin-bottom:20px}.section-head>p{color:var(--muted);padding-top:25px}.lab{display:grid;grid-template-columns:250px 1fr;gap:1px;background:var(--line);border:1px solid var(--line);border-radius:12px;overflow:hidden;box-shadow:var(--shadow)}.controls{padding:25px;background:var(--white)}label{display:block;font-size:13px;font-weight:600;line-height:1.5}output{float:right;font-variant-numeric:tabular-nums;color:var(--teal)}select{display:block;width:100%;padding:10px 8px;margin:10px 0 20px;border:1px solid var(--line);border-radius:4px;color:var(--ink);background:var(--paper);font-size:13px}input[type=range]{display:block;width:100%;margin:15px 0 24px;accent-color:var(--teal);cursor:pointer}input[type=checkbox]{accent-color:var(--teal)}.legend{display:grid;grid-template-columns:1fr 1fr;gap:10px 5px;font-size:11px;margin-bottom:25px}.legend span{display:flex;gap:7px;align-items:center}.dot{display:inline-block;width:11px;height:11px;border-radius:50%;flex:none}.dot.s{background:#287ab0}.dot.t{background:#bd602e}.dot.both{background:#7e659d}.dot.neither{background:#8b9485}.set-description{font-size:12px;line-height:1.8;padding:14px 0;border-top:1px solid var(--line);margin-top:12px}.subtle{font-size:12px}.graph-panel{padding:22px 26px;background:var(--white);min-width:0}.segmented{display:flex;gap:4px;flex-wrap:wrap}.segmented button{font-size:12px;padding:9px 17px;background:transparent;border-color:transparent}.segmented button[aria-pressed=true]{background:var(--ink);color:white}svg{max-width:100%;height:auto;display:block}#graph{width:100%;margin:5px auto -10px}svg text{font-family:Arial,Helvetica,sans-serif;fill:var(--ink)}.caption{font-size:13px;line-height:1.65;min-height:45px}.graph-actions{display:flex;align-items:center;gap:9px;flex-wrap:wrap;padding-top:10px;font-size:12px}.graph-actions button{font-size:12px;padding:7px 11px}#step-label{font-variant-numeric:tabular-nums;min-width:72px;text-align:center}#remove-label{font-size:12px}.witness-summary{display:grid;grid-template-columns:.65fr .65fr 1.6fr;margin-top:15px;border:1px solid var(--line);border-radius:10px;overflow:hidden}.witness-summary>div{padding:22px 25px;display:flex;flex-direction:column;justify-content:center;gap:5px}.witness-summary>div+div{border-left:1px solid var(--line)}.witness-summary strong{font-family:Georgia,serif;font-size:38px;font-weight:400}.witness-summary span{font-size:12px}.witness-chain{background:var(--light)}.witness-chain #chain{font-family:Georgia,serif;font-size:24px;line-height:1.4}.witness-chain p{margin:5px 0 0}details{margin-top:24px;background:#ffffff50;border-top:1px solid var(--line);padding:18px 0 0}summary{font-size:13px;font-weight:600;cursor:pointer;margin-bottom:14px}details p{font-size:14px}.formula{font-family:Georgia,serif;font-size:22px;line-height:1.8;padding:22px 0;overflow-wrap:anywhere}.formula span{font:12px Arial;color:var(--muted)}details .formula{font-size:16px}.proof-layout{display:grid;grid-template-columns:1.3fr 1fr;gap:45px;align-items:start}.map-row{display:grid;grid-template-columns:1fr;max-width:85%;margin:auto}.map-row.two{grid-template-columns:1fr 1fr;gap:25px;max-width:100%}.map-node{display:flex;flex-direction:column;align-items:flex-start;text-align:left;padding:16px 18px;border-radius:7px;min-height:100px}.map-node small{font-size:9px;letter-spacing:.08em;font-weight:bold;color:var(--muted)}.map-node strong{font-size:16px;line-height:1.4;margin:5px 0}.map-node span{font-size:11px;line-height:1.5;color:var(--muted)}.map-node.selected{border:2px solid var(--teal);padding:15px 17px;background:var(--light)}.map-node.final-node{background:var(--ink);color:white;align-items:center}.map-node.final-node small,.map-node.final-node span{color:#cfdfd7}.map-arrow{text-align:center;color:var(--teal);font-size:24px;height:36px;line-height:36px}.map-join{height:45px;position:relative;display:flex;margin:0 25%}.map-join i{height:22px;width:50%;border-bottom:1.5px solid var(--teal)}.map-join i:first-child{border-left:1.5px solid var(--teal)}.map-join i:nth-child(2){border-right:1.5px solid var(--teal)}.map-join span{position:absolute;top:17px;left:calc(50% - 7px);font-size:24px;line-height:28px;color:var(--teal)}.map-split{height:36px;display:flex;justify-content:space-around;color:var(--teal);font-size:24px;line-height:36px}#proof-detail{background:var(--light);padding:30px;border-radius:12px;position:sticky;top:25px}#proof-detail h3{font-family:Georgia,serif;font-size:30px;font-weight:400;margin:0 0 16px}#proof-detail p{font-size:14px}#proof-detail .formula{font-size:25px;border-top:1px solid #bdcbbd;border-bottom:1px solid #bdcbbd;margin:22px 0;text-align:center}#proof-detail code{display:block;font-size:11px;overflow-wrap:anywhere;line-height:1.8}#proof-detail a{font-size:12px}.detail-role{border-left:3px solid var(--teal);padding-left:15px;margin:20px 0}.matching-layout,.sum-layout,.domain-layout{display:grid;grid-template-columns:1fr 1fr;gap:65px;align-items:start}.matching-layout>div:first-child,.sum-layout>div:first-child{background:var(--white);border:1px solid var(--line);border-radius:12px;padding:20px}.color-buttons{display:flex;justify-content:center;gap:7px;flex-wrap:wrap}.color-buttons button{border-width:2px;min-width:36px;padding:6px;font-size:11px}.color-buttons button[aria-pressed=true]{box-shadow:0 0 0 2px var(--ink)}.matching-controls{padding:10px 0}.math-callout{background:var(--light);border-left:3px solid var(--teal);padding:22px;font-family:Georgia,serif;font-size:24px;line-height:1.6;margin:20px 0}.matching-controls>p,.reason>p{font-size:14px}.matching-controls details{margin-top:15px}.sum-layout .caption{margin:0;padding:0 10px}.reason .formula{padding-top:0}.reason a{font-size:12px}.domain-panel{border:1px solid var(--line);border-radius:12px;background:var(--white);padding:28px}.domain-panel label{display:flex;justify-content:space-between;align-items:center;gap:15px}.domain-panel input{width:130px;padding:10px;border:1px solid var(--line);border-radius:4px;background:var(--paper);color:var(--ink)}.preset-buttons{display:flex;gap:8px;margin-top:20px;flex-wrap:wrap}.preset-buttons button{font-size:12px;padding:7px 12px}.rho-axis{margin:50px 10px 20px}.rho-track{position:relative;border-top:2px solid var(--teal);height:16px}.rho-track:after,.rho-track:before{content:'';position:absolute;height:12px;top:-7px;border-left:1px solid var(--teal)}.rho-track:after{right:0}.rho-track>span{position:absolute;top:-8px;width:14px;height:14px;border-radius:50%;background:var(--orange);transform:translateX(-50%);transition:left .3s}.axis-labels{display:flex;justify-content:space-between;font-size:12px}.domain-stats{display:flex;border-top:1px solid var(--line);padding-top:22px;gap:35px}.domain-stats strong{display:block;font-family:Georgia,serif;font-size:27px;font-weight:400}.domain-stats span{font-size:11px;color:var(--muted)}.scope-note{margin:30px 0 0;font-size:13px;border-left:3px solid var(--orange);padding-left:18px}.verify-grid{display:grid;grid-template-columns:repeat(3,1fr);gap:25px;margin:30px 0}.verify-grid article{border:1px solid var(--line);border-radius:10px;background:var(--white);padding:28px}.number{font-family:Georgia,serif;font-size:32px;color:var(--teal)}.verify-grid p{font-size:14px}.verify-grid a{font-size:13px}.verification-record{font-size:13px;background:var(--light);padding:25px;border-radius:8px}.verification-record p:last-child{margin:0}.context{display:grid;grid-template-columns:1fr 1fr;gap:65px}.context>div:nth-child(2){padding-top:30px}.context p{font-size:14px}footer{padding:30px 40px 45px;border-top:1px solid var(--line);display:flex;justify-content:space-between;gap:25px;font-size:11px;color:var(--muted)}footer p{margin:0}.skip{position:absolute;left:20px;top:-100px;padding:12px;background:white;z-index:5}.skip:focus{top:15px}[hidden]{display:none!important}@media(max-width:1000px){.hero{gap:35px}.brand-name{display:none}main{padding:0 25px}header{padding:22px 25px}.section-head{gap:40px}.proof-layout{gap:25px}.matching-layout,.sum-layout,.domain-layout{gap:35px}.lab{grid-template-columns:210px 1fr}.controls{padding:20px}.witness-chain #chain{font-size:20px}.graph-panel{padding:20px 15px}}@media(max-width:740px){header{align-items:flex-start;gap:18px;padding:20px}nav{gap:12px 18px;font-size:12px;justify-content:flex-end}.brand{font-size:20px}.brand>span:first-child{font-size:25px}main{padding:0 20px}.hero{grid-template-columns:1fr;padding:45px 0;gap:30px}h1{font-size:66px}.theorem{transform:none;padding:25px}.theorem>*{transform:none}.big-equation{font-size:40px}.hero-links{font-size:12px}.rule{padding:38px 0}.columns,.section-head,.proof-layout,.matching-layout,.sum-layout,.domain-layout,.context{grid-template-columns:1fr;gap:20px}.section-head{margin-bottom:18px}.section-head>p{padding:0;margin:0}.columns{gap:0}.lab{grid-template-columns:1fr}.controls{display:grid;grid-template-columns:1fr 1fr;gap:8px 20px;padding:20px}.controls>label:first-child,.controls select,.controls .legend,.controls .set-description,.controls .small,.controls button{grid-column:1/-1}.controls select{margin:0 0 10px}.controls .legend{display:flex;flex-wrap:wrap;gap:16px;margin:5px 0 15px}.controls label[for=p]{grid-row:4;grid-column:1}.controls #p{grid-row:5;grid-column:1}.controls label[for=q]{grid-row:4;grid-column:2}.controls #q{grid-row:5;grid-column:2}.controls input[type=range]{margin:3px 0 10px}.controls .set-description{margin:0}.controls .small{margin:0}.controls button{justify-self:start}.graph-panel{padding:18px 10px}.graph-actions{padding:10px}.caption{padding:0 10px;min-height:65px}.witness-summary{grid-template-columns:1fr 1fr}.witness-summary>div{padding:18px}.witness-summary .witness-chain{grid-column:1/-1;border-left:0;border-top:1px solid var(--line)}#proof-detail{position:static;padding:24px}.map-row{max-width:88%}.map-row.two{gap:14px}.map-node{padding:13px;min-height:108px}.map-node.selected{padding:12px}.map-node strong{font-size:14px}.map-node small{font-size:8px}.map-node span{font-size:10px}.verify-grid{grid-template-columns:1fr;gap:14px}.verify-grid article{padding:23px}.verify-grid h3{margin:12px 0}.context>div:nth-child(2){padding-top:0}footer{padding:25px 20px;flex-direction:column;gap:15px}.domain-panel{padding:22px}.domain-stats{gap:25px}}@media(prefers-reduced-motion:reduce){:root{scroll-behavior:auto}.rho-track>span{transition:none}}

.map-connector{width:100%;height:42px;display:block}.map-connector path{stroke:var(--teal);fill:none;stroke-width:1.5;vector-effect:non-scaling-stroke;stroke-linejoin:round;stroke-linecap:round}#graph{max-height:430px}.graph-actions{padding-top:12px;padding-bottom:2px;min-height:48px}@media(max-width:740px){#graph{max-height:none}.graph-actions{padding:12px 5px}.graph-actions #show-all{font-size:11px;padding:6px 8px}.graph-actions #step-label{min-width:58px}}

.matching-toggle{font-size:12px;font-weight:400;text-align:center;margin-top:20px}.matching-toggle input{vertical-align:middle}