body,h1,h2,h3,h4,h5,h6,p,blockquote,pre,hr,dl,dd,ol,ul,figure{margin:0;padding:0}body{font:400 16px/1.5 -apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";color:#111;background-color:#fdfdfd;-webkit-text-size-adjust:100%;-webkit-font-feature-settings:"kern" 1;-moz-font-feature-settings:"kern" 1;-o-font-feature-settings:"kern" 1;font-feature-settings:"kern" 1;font-kerning:normal;display:flex;min-height:100vh;flex-direction:column}h1,h2,h3,h4,h5,h6,p,blockquote,pre,ul,ol,dl,figure,.highlight{margin-bottom:15px}main{display:block}img{max-width:100%;vertical-align:middle}figure>img{display:block}figcaption{font-size:14px}ul,ol{margin-left:30px}li>ul,li>ol{margin-bottom:0}h1,h2,h3,h4,h5,h6{font-weight:400}a{color:#2a7ae2;text-decoration:none}a:visited{color:#1756a9}a:hover{color:#111;text-decoration:underline}.social-media-list a:hover{text-decoration:none}.social-media-list a:hover .username{text-decoration:underline}blockquote{color:#828282;border-left:4px solid #e8e8e8;padding-left:15px;font-size:18px;letter-spacing:-1px;font-style:italic}blockquote>:last-child{margin-bottom:0}pre,code{font-size:15px;border:1px solid #e8e8e8;border-radius:3px;background-color:#eef}code{padding:1px 5px}pre{padding:8px 12px;overflow-x:auto}pre>code{border:0;padding-right:0;padding-left:0}.wrapper{max-width:-webkit-calc(800px - (30px * 2));max-width:calc(800px - (30px * 2));margin-right:auto;margin-left:auto;padding-right:30px;padding-left:30px}@media screen and (max-width: 800px){.wrapper{max-width:-webkit-calc(800px - (30px));max-width:calc(800px - (30px));padding-right:15px;padding-left:15px}}.wrapper:after,.footer-col-wrapper:after{content:"";display:table;clear:both}.svg-icon{width:16px;height:16px;display:inline-block;fill:#828282;padding-right:5px;vertical-align:text-top}.social-media-list li+li{padding-top:5px}table{margin-bottom:30px;width:100%;text-align:left;color:#3f3f3f;border-collapse:collapse;border:1px solid #e8e8e8}table tr:nth-child(even){background-color:#f7f7f7}table th,table td{padding:10px 15px}table th{background-color:#f0f0f0;border:1px solid #dedede;border-bottom-color:#c9c9c9}table td{border:1px solid #e8e8e8}.site-header{border-top:5px solid #424242;border-bottom:1px solid #e8e8e8;min-height:55.95px;position:relative}.site-title{font-size:26px;font-weight:300;line-height:54px;letter-spacing:-1px;margin-bottom:0;float:left}.site-title,.site-title:visited{color:#424242}.site-nav{float:right;line-height:54px}.site-nav .nav-trigger{display:none}.site-nav .menu-icon{display:none}.site-nav .page-link{color:#111;line-height:1.5}.site-nav .page-link:not(:last-child){margin-right:20px}@media screen and (max-width: 600px){.site-nav{position:absolute;top:9px;right:15px;background-color:#fdfdfd;border:1px solid #e8e8e8;border-radius:5px;text-align:right}.site-nav label[for="nav-trigger"]{display:block;float:right;width:36px;height:36px;z-index:2;cursor:pointer}.site-nav .menu-icon{display:block;float:right;width:36px;height:26px;line-height:0;padding-top:10px;text-align:center}.site-nav .menu-icon>svg{fill:#424242}.site-nav input ~ .trigger{clear:both;display:none}.site-nav input:checked ~ .trigger{display:block;padding-bottom:5px}.site-nav .page-link{display:block;padding:5px 10px;margin-left:20px}.site-nav .page-link:not(:last-child){margin-right:0}}.site-footer{border-top:1px solid #e8e8e8;padding:30px 0}.footer-heading{font-size:18px;margin-bottom:15px}.contact-list,.social-media-list{list-style:none;margin-left:0}.footer-col-wrapper{font-size:15px;color:#828282;margin-left:-15px}.footer-col{float:left;margin-bottom:15px;padding-left:15px}.footer-col-1{width:-webkit-calc(35% - (30px / 2));width:calc(35% - (30px / 2))}.footer-col-2{width:-webkit-calc(20% - (30px / 2));width:calc(20% - (30px / 2))}.footer-col-3{width:-webkit-calc(45% - (30px / 2));width:calc(45% - (30px / 2))}@media screen and (max-width: 800px){.footer-col-1,.footer-col-2{width:-webkit-calc(50% - (30px / 2));width:calc(50% - (30px / 2))}.footer-col-3{width:-webkit-calc(100% - (30px / 2));width:calc(100% - (30px / 2))}}@media screen and (max-width: 600px){.footer-col{float:none;width:-webkit-calc(100% - (30px / 2));width:calc(100% - (30px / 2))}}.page-content{padding:30px 0;flex:1}.page-heading{font-size:32px}.post-list-heading{font-size:28px}.post-list{margin-left:0;list-style:none}.post-list>li{margin-bottom:30px}.post-meta{font-size:14px;color:#828282}.post-link{display:block;font-size:24px}.post-header{margin-bottom:30px}.post-title{font-size:42px;letter-spacing:-1px;line-height:1}@media screen and (max-width: 800px){.post-title{font-size:36px}}.post-content{margin-bottom:30px}.post-content h2{font-size:32px}@media screen and (max-width: 800px){.post-content h2{font-size:28px}}.post-content h3{font-size:26px}@media screen and (max-width: 800px){.post-content h3{font-size:22px}}.post-content h4{font-size:20px}@media screen and (max-width: 800px){.post-content h4{font-size:18px}}.highlight{background:#fff}.highlighter-rouge .highlight{background:#eef}.highlight .c{color:#998;font-style:italic}.highlight .err{color:#a61717;background-color:#e3d2d2}.highlight .k{font-weight:bold}.highlight .o{font-weight:bold}.highlight .cm{color:#998;font-style:italic}.highlight .cp{color:#999;font-weight:bold}.highlight .c1{color:#998;font-style:italic}.highlight .cs{color:#999;font-weight:bold;font-style:italic}.highlight .gd{color:#000;background-color:#fdd}.highlight .gd .x{color:#000;background-color:#faa}.highlight .ge{font-style:italic}.highlight .gr{color:#a00}.highlight .gh{color:#999}.highlight .gi{color:#000;background-color:#dfd}.highlight .gi .x{color:#000;background-color:#afa}.highlight .go{color:#888}.highlight .gp{color:#555}.highlight .gs{font-weight:bold}.highlight .gu{color:#aaa}.highlight .gt{color:#a00}.highlight .kc{font-weight:bold}.highlight .kd{font-weight:bold}.highlight .kp{font-weight:bold}.highlight .kr{font-weight:bold}.highlight .kt{color:#458;font-weight:bold}.highlight .m{color:#099}.highlight .s{color:#d14}.highlight .na{color:teal}.highlight .nb{color:#0086B3}.highlight .nc{color:#458;font-weight:bold}.highlight .no{color:teal}.highlight .ni{color:purple}.highlight .ne{color:#900;font-weight:bold}.highlight .nf{color:#900;font-weight:bold}.highlight .nn{color:#555}.highlight .nt{color:navy}.highlight .nv{color:teal}.highlight .ow{font-weight:bold}.highlight .w{color:#bbb}.highlight .mf{color:#099}.highlight .mh{color:#099}.highlight .mi{color:#099}.highlight .mo{color:#099}.highlight .sb{color:#d14}.highlight .sc{color:#d14}.highlight .sd{color:#d14}.highlight .s2{color:#d14}.highlight .se{color:#d14}.highlight .sh{color:#d14}.highlight .si{color:#d14}.highlight .sx{color:#d14}.highlight .sr{color:#009926}.highlight .s1{color:#d14}.highlight .ss{color:#990073}.highlight .bp{color:#999}.highlight .vc{color:teal}.highlight .vg{color:teal}.highlight .vi{color:teal}.highlight .il{color:#099}.wrapper{max-width:1180px}.site-header{border-top:6px solid #1f5f8b;border-bottom:1px solid #d7dee5}.site-footer{border-top:1px solid #d7dee5;padding:22px 0 26px 0}.site-title,.site-title:visited{color:#17324d;font-weight:700}.page-content{padding-top:32px}h1,h2,h3{color:#17324d}h1{margin-bottom:0.5rem}p,li{line-height:1.6}.intro-card{background:#f6f9fc;border:1px solid #d7e3ef;border-radius:10px;padding:1rem 1.1rem;margin:1rem 0 1.5rem 0}.intro-card--tight{margin-top:0.8rem;margin-bottom:0}.landing-hero{display:grid;grid-template-columns:minmax(0, 1.7fr) minmax(18rem, 0.95fr);gap:1.25rem;margin:0.25rem 0 1.75rem 0;padding:1.25rem;border-radius:22px;background:radial-gradient(circle at top right, rgba(91,166,132,0.2), transparent 28%),linear-gradient(135deg, #12304a 0%, #17324d 62%, #1e4858 100%);box-shadow:0 20px 44px rgba(23,50,77,0.14)}.landing-hero--clean{color:#f6fbff}.landing-hero__main{min-width:0}.landing-hero__eyebrow{text-transform:uppercase;letter-spacing:0.08em;font-size:0.78rem;font-weight:700;color:#9fd7c0;margin-bottom:0.65rem}.landing-hero__lede{color:rgba(247,251,255,0.92);max-width:42rem;margin:0;font-size:1.02rem}.landing-summary{align-self:stretch;display:flex;flex-direction:column;gap:0.85rem;padding:1rem;border-radius:18px;background:rgba(255,255,255,0.08);border:1px solid rgba(255,255,255,0.12);backdrop-filter:blur(4px)}.landing-summary__metric{padding-bottom:0.75rem;border-bottom:1px solid rgba(255,255,255,0.12)}.landing-summary__value{display:block;font-size:1.55rem;line-height:1.1;font-weight:800;color:#fff}.landing-summary__label{display:block;margin-top:0.28rem;color:rgba(247,251,255,0.82);font-size:0.9rem}.landing-summary__note{color:rgba(247,251,255,0.92);font-size:0.95rem;line-height:1.5}.landing-summary__note strong{color:#fff}.quick-links{display:flex;flex-wrap:wrap;gap:0.65rem;margin:1rem 0 1.5rem 0}.quick-links--hero{margin-bottom:0;margin-top:1.15rem}.quick-links a{background:#17324d;color:#fff;text-decoration:none;padding:0.45rem 0.8rem;border-radius:999px;font-size:0.95rem}.quick-links--hero a{background:rgba(255,255,255,0.12);border:1px solid rgba(255,255,255,0.14)}.quick-links--hero a:hover{background:rgba(255,255,255,0.2)}.quick-links a:hover{background:#1f5f8b}.section-grid{display:grid;grid-template-columns:repeat(2, minmax(0, 1fr));gap:1rem;margin:1.2rem 0 1.8rem 0}.section-card{display:block;text-decoration:none;color:#17324d;background:linear-gradient(180deg, #fff 0%, #f7fbfd 100%);border:1px solid #d7e3ef;border-radius:16px;padding:1rem 1.05rem;box-shadow:0 10px 24px rgba(23,50,77,0.06);transition:transform 0.15s ease, box-shadow 0.15s ease, border-color 0.15s ease}.section-card:hover{transform:translateY(-2px);box-shadow:0 16px 30px rgba(23,50,77,0.1);border-color:#a9c6dc}.section-card strong,.section-card__kicker,.section-card__meta{display:block}.section-card__kicker{color:#1f5f8b;text-transform:uppercase;letter-spacing:0.06em;font-size:0.76rem;font-weight:700;margin-bottom:0.35rem}.section-card__meta{margin-top:0.65rem;color:#53708b;font-size:0.92rem}.result-board{display:grid;grid-template-columns:repeat(2, minmax(0, 1fr));gap:0.9rem;margin:1rem 0 1.8rem 0}.result-item{display:grid;grid-template-columns:2.25rem 1fr;gap:0.9rem;align-items:start;border-radius:16px;padding:1rem 1rem 0.95rem 1rem;border:1px solid #d7e3ef;background:#ffffff;box-shadow:0 10px 24px rgba(23,50,77,0.05)}.result-item strong,.result-item span{display:block}.result-item span:last-child{color:#4d647a;margin-top:0.18rem}.result-item__icon{width:2.25rem;height:2.25rem;border-radius:999px;position:relative;place-self:start;flex-shrink:0}.result-item__icon::before{content:attr(data-icon);position:absolute;top:50%;left:50%;font-size:1rem;font-weight:800;line-height:1;text-align:center;transform:translate(-50%, -50%)}.featured-theorems{display:grid;grid-template-columns:repeat(2, minmax(0, 1fr));gap:1rem;margin:1rem 0 2rem 0}.theorem-highlight{border:1px solid #d7e3ef;border-radius:18px;background:linear-gradient(180deg, #fff 0%, #f7fbfd 100%);box-shadow:0 12px 28px rgba(23,50,77,0.06);overflow:hidden}.theorem-highlight__header{display:flex;justify-content:space-between;gap:1rem;align-items:start;padding:1rem 1rem 0.9rem 1rem;border-bottom:1px solid #d7e3ef;background:#f4f9fc}.theorem-highlight__section,.theorem-highlight__label,.theorem-highlight__title{display:block}.theorem-highlight__section{color:#1f5f8b;text-transform:uppercase;letter-spacing:0.07em;font-size:0.73rem;font-weight:700;margin-bottom:0.35rem}.theorem-highlight__label{color:#17324d;font-size:0.95rem;font-weight:700}.theorem-highlight__title{margin-top:0.18rem;color:#486176;font-size:0.95rem}.theorem-highlight__badges{display:flex;flex-wrap:wrap;gap:0.45rem}.theorem-highlight .fidelity-badge{background:#e8f1f8;color:#17324d;border-color:#c9dbe8}.theorem-highlight__body{display:grid;grid-template-columns:repeat(2, minmax(0, 1fr))}.theorem-highlight__paper,.theorem-highlight__lean{padding:0.95rem 1rem 1rem 1rem}.theorem-highlight__paper{border-right:1px solid #e3ecf3}.theorem-highlight__heading{color:#5b748c;text-transform:uppercase;letter-spacing:0.06em;font-size:0.72rem;font-weight:700;margin-bottom:0.45rem}.theorem-highlight__math{color:#17324d;line-height:1.55}.theorem-highlight__name{margin-bottom:0.55rem}.theorem-highlight__code{margin:0 0 0.8rem 0;padding:0.85rem 0.95rem;border-radius:12px;background:#0f2233;color:#f4fbff;overflow-x:auto;font-size:0.86rem;line-height:1.45}.theorem-highlight__code code,.theorem-highlight__code .w{color:#f4fbff !important;background:transparent}.theorem-highlight__code .k,.theorem-highlight__code .kd,.theorem-highlight__code .kt{color:#8fd3ff !important}.theorem-highlight__code .n,.theorem-highlight__code .nf,.theorem-highlight__code .nc,.theorem-highlight__code .nn{color:#f4fbff !important}.theorem-highlight__code .s,.theorem-highlight__code .s1,.theorem-highlight__code .s2{color:#b6f0c1 !important}.theorem-highlight__code .mi,.theorem-highlight__code .mf,.theorem-highlight__code .m{color:#ffd280 !important}.theorem-highlight__code .c,.theorem-highlight__code .c1,.theorem-highlight__code .cm{color:#93aabd !important}.blocker-grid{display:grid;grid-template-columns:repeat(3, minmax(0, 1fr));gap:1rem;margin:1rem 0 1.9rem 0}.blocker-card{border:1px solid #d7e3ef;border-radius:16px;padding:1rem 1rem 0.95rem 1rem;background:#ffffff;box-shadow:0 10px 24px rgba(23,50,77,0.05)}.blocker-card__kicker{display:block;margin-bottom:0.4rem;color:#8b5a1f;text-transform:uppercase;letter-spacing:0.06em;font-size:0.72rem;font-weight:700}.blocker-card strong{display:block;color:#17324d;margin-bottom:0.35rem}.blocker-card p{margin:0 0 0.8rem 0;color:#4d647a}.blocker-card a{color:#1f5f8b;font-weight:600;text-decoration:none}.blocker-card a:hover{text-decoration:underline}.theorem-compare{margin:1.2rem 0 1.8rem 0;border:1px solid #cbdbe8;border-radius:20px;background:linear-gradient(180deg, #fff 0%, #f7fbfd 100%);box-shadow:0 18px 40px rgba(23,50,77,0.08);overflow:hidden}.theorem-compare__header{display:flex;justify-content:space-between;gap:1rem;align-items:start;padding:1.15rem 1.2rem 1.05rem 1.2rem;border-bottom:1px solid #d7e3ef;background:radial-gradient(circle at top right, rgba(91,166,132,0.14), transparent 28%),linear-gradient(135deg, #17324d 0%, #1d4861 100%)}.theorem-compare__identity{min-width:0}.theorem-compare__label,.theorem-compare__title{display:block}.theorem-compare__eyebrow{display:inline-block;margin-bottom:0.45rem;color:#9fd7c0;text-transform:uppercase;letter-spacing:0.08em;font-size:0.74rem;font-weight:700}.theorem-compare__label{color:rgba(255,255,255,0.8);text-transform:uppercase;letter-spacing:0.06em;font-size:0.8rem;font-weight:700;margin-bottom:0.22rem}.theorem-compare__title{color:#ffffff;font-size:1.2rem;line-height:1.25}.theorem-compare__badges{display:flex;gap:0.5rem;flex-wrap:wrap}.status-badge,.fidelity-badge{display:inline-block;padding:0.28rem 0.62rem;border-radius:999px;font-size:0.82rem;font-weight:700;white-space:nowrap;border:1px solid transparent}.status-badge--proved{background:#dff3e8;color:#1f6a46;border-color:#b9dec8}.status-badge--partial{background:#fdebc2;color:#8c5a00;border-color:#efcf8f}.fidelity-badge{background:rgba(255,255,255,0.12);color:#ffffff;border-color:rgba(255,255,255,0.14)}.theorem-compare__grid{display:grid;grid-template-columns:repeat(2, minmax(0, 1fr));gap:0;background:#ffffff}.theorem-pane{padding:1.15rem 1.2rem 1.2rem 1.2rem}.theorem-pane--paper{border-right:1px solid #d7e3ef;background:linear-gradient(180deg, #fffdfa 0%, #fff9ef 100%)}.theorem-pane--lean{background:linear-gradient(180deg, #fcfeff 0%, #f4f9fd 100%)}.theorem-pane__heading{margin-top:0;margin-bottom:0.75rem;font-size:0.82rem;text-transform:uppercase;letter-spacing:0.08em;color:#53708b;font-weight:800}.theorem-pane__lede{margin-bottom:0.8rem}.theorem-pane__lede code{display:inline-block;padding:0.25rem 0.55rem;border-radius:999px;background:#eaf2f8;color:#17324d;font-size:0.92rem;font-weight:700}.theorem-pane__body{color:#20364d}.theorem-pane__body--math{font-size:1.03rem;line-height:1.7}.theorem-pane__body--secondary{margin-top:0.85rem;font-size:0.97rem;color:#466078}.theorem-pane__body p:last-child{margin-bottom:0}.theorem-code{margin:0;padding:0.95rem 1rem;border-radius:14px;background:#132534;color:#eef6fb;overflow-x:auto;box-shadow:inset 0 1px 0 rgba(255,255,255,0.04)}.theorem-code code{display:block;background:transparent;color:inherit;font-size:0.92rem;line-height:1.55;white-space:pre}.theorem-pane__link{display:inline-block;margin-top:1rem;color:#1f5f8b;font-weight:700;text-decoration:none}.theorem-pane__link:hover{text-decoration:underline}.theorem-link-list{display:flex;flex-wrap:wrap;gap:0.65rem 1rem;margin-top:1rem}.theorem-link-list .theorem-pane__link{margin-top:0}.theorem-compare__footer{display:grid;gap:0.25rem;padding:0.95rem 1.2rem 1.05rem 1.2rem;border-top:1px solid #d7e3ef;background:#fcfdff}.theorem-compare__footer strong{color:#17324d}.theorem-compare__notes{color:#4d647a;font-size:0.93rem}@media (max-width: 760px){.theorem-compare__header,.theorem-compare__footer{flex-direction:column}.theorem-compare__grid{grid-template-columns:1fr}.theorem-pane--paper{border-right:0;border-bottom:1px solid #d7e3ef}}.result-item--done{background:linear-gradient(180deg, #fbfffd 0%, #f3fbf7 100%);border-color:#c9e5d7}.result-item--done .result-item__icon{color:#146b45;background:#dff3e9}.result-item--open{background:linear-gradient(180deg, #fffdf8 0%, #fff7e8 100%);border-color:#f0d8a3}.result-item--open .result-item__icon{color:#9a5b00;background:#fdebc2}.theorem-stack{display:grid;gap:1rem;margin:1rem 0 1.8rem 0}.theorem-stack .theorem-compare{margin:0}.reference-strip{display:flex;flex-wrap:wrap;gap:0.75rem;margin:0.9rem 0 0.5rem 0}.reference-strip a{text-decoration:none;color:#17324d;background:#f3f7fb;border:1px solid #d7e3ef;padding:0.5rem 0.8rem;border-radius:999px}.reference-strip a:hover{border-color:#a9c6dc;background:#ecf4fb}table{width:100%;display:table;font-size:0.96rem}th,td{vertical-align:top;padding:0.65rem 0.75rem}th{background:#f3f6f9}tr:nth-child(even) td{background:#fbfcfd}code{font-size:0.92em}blockquote{color:#4a5968;border-left:4px solid #d1dce8;background:#fafcff;padding:0.55rem 1rem}.footer-minimal{display:flex;flex-wrap:wrap;align-items:center;gap:0.8rem 1.25rem;color:#4d647a;font-size:0.95rem}.footer-brand{color:#17324d;font-weight:700}.footer-links{display:flex;flex-wrap:wrap;gap:0.75rem}.footer-links a{color:#1f5f8b;text-decoration:none}.footer-links a:hover{text-decoration:underline}@media (max-width: 820px){.landing-hero,.result-board,.section-grid,.featured-theorems,.blocker-grid{grid-template-columns:1fr}.landing-hero{padding:1rem}.theorem-highlight__body{grid-template-columns:1fr}.theorem-highlight__paper{border-right:0;border-bottom:1px solid #e3ecf3}}