@font-face {
  font-family: "IBM Plex Sans";
  src: url("fonts/ibm-plex-sans-latin-400-normal.woff2") format("woff2");
  font-weight: 400;
  font-style: normal;
  font-display: swap;
}
@font-face {
  font-family: "IBM Plex Sans";
  src: url("fonts/ibm-plex-sans-latin-500-normal.woff2") format("woff2");
  font-weight: 500;
  font-style: normal;
  font-display: swap;
}
@font-face {
  font-family: Inter;
  src: url("fonts/inter-latin-600-normal.woff2") format("woff2");
  font-weight: 600;
  font-style: normal;
  font-display: swap;
}
:root {
  color-scheme: light;
  --paper: #fff;
  --ink: #252b32;
  --muted: #69737d;
  --line: #e0e5e8;
  --green: #286493;
  --soft: #f4f7f9;
  --sans: "IBM Plex Sans", system-ui, sans-serif;
  --heading: Inter, var(--sans);
  --serif: var(--sans);
  --mono: ui-monospace, SFMono-Regular, Consolas, monospace;
  --measure: 660px;
  --masthead: #12303d;
  --topbar-height: 64px;
}
* { box-sizing: border-box; }
html { scroll-behavior: smooth; scroll-padding-top: 86px; }
body { margin: 0; background: var(--paper); color: var(--ink); font: 17px/1.7 var(--sans); -webkit-font-smoothing: antialiased; }
a { color: var(--green); text-underline-offset: 3px; text-decoration-thickness: 1px; }
a:hover { color: #153c5b; }
:focus-visible { outline: 2px solid #286493; outline-offset: 4px; }
img { display: block; max-width: 100%; height: auto; }
figure { margin: 32px 0; }
p { margin: 0 0 20px; }
h1, h2, h3 { font-family: var(--heading); font-weight: 600; letter-spacing: -.025em; line-height: 1.3; color: #1c242d; }
h1 { font-size: 34px; margin: 0 0 16px; }
h2 { font-size: 25px; margin: 50px 0 20px; }
h3 { font-size: 20px; margin: 34px 0 15px; }
pre, code { font-family: var(--mono); }
code { font-size: .82em; }
pre { white-space: pre; overflow: auto; max-width: 100%; font-size: 12px; line-height: 1.7; tab-size: 2; }
figcaption, .caption { font: 13px/1.6 var(--sans); color: var(--muted); margin-top: 12px; }
.skip { position: absolute; top: -100px; left: 16px; padding: 12px; background: white; z-index: 100; }
.skip:focus { top: 10px; }
.site-header { min-height: var(--topbar-height); display: flex; align-items: center; justify-content: space-between; gap: 20px; padding: 16px max(24px, calc((100vw - 1100px) / 2)); background: var(--masthead); color: #eaf0f2; }
.wordmark { font: 500 15px/1.5 var(--sans); text-decoration: none; color: inherit; white-space: nowrap; }
.wordmark span { font-weight: 400; color: #b4c5cc; padding-left: 10px; }
.site-header a { color: #eaf0f2; }
.site-header a:hover { color: #fff; }
.site-header nav { display: flex; gap: 24px; font-size: 13px; }
.site-header nav a { text-decoration: none; }
.topbar-actions { display: flex; align-items: center; justify-content: flex-end; gap: 20px; font-size: 13px; }
.topbar-actions a { text-decoration: none; }
.topbar-actions .reader-button { padding: 7px 10px; color: #eaf0f2; border: 1px solid #52707c; border-radius: 3px; background: transparent; cursor: pointer; font: 12px/1.4 var(--sans); }
.topbar-actions .reader-button:hover { background: #264653; }
.topbar-actions .reader-button[aria-pressed="true"] { background: #264653; border-color: #88a6bc; }
.home { max-width: 708px; padding: 0 24px; margin: auto; }
.intro { max-width: var(--measure); padding: 56px 0 28px; }
.intro h1 { font-size: 33px; }
.byline, .article-meta { font: 13px/1.6 var(--sans); color: var(--muted); margin: 10px 0 25px; }
.intro p { font-size: 18px; line-height: 1.7; }
.intro .byline { font-size: 13px; }
.intro .writing-note { font-size: 13px; line-height: 1.6; color: var(--muted); }
.essay-index { margin: 10px 0 30px; }
.essay-entry { position: relative; padding: 32px 0; border-top: 1px solid var(--line); }
.essay-entry .entry-kind { position: absolute; right: calc(100% + 32px); width: 145px; color: var(--muted); font: 13px/1.5 var(--sans); padding-top: 5px; }
.essay-entry h2 { margin: 0 0 12px; font-size: 23px; }
.essay-entry h2 a { color: var(--ink); text-decoration: none; }
.essay-entry h2 a:hover { color: var(--green); }
.essay-entry p { margin-bottom: 14px; }
.entry-copy { min-width: 0; }
.entry-result { font: 14px/1.65 var(--sans); padding: 12px 16px; margin: 18px 0; background: #f5f7f8; color: #41505d; }
.text-link { font-size: 13px; text-decoration: none; }
.home-source { max-width: 660px; padding: 5px 0 42px; }
.home-source h2 { font-size: 20px; }
.home-source pre { padding: 15px 18px; background: var(--soft); }
.site-footer { display: flex; flex-wrap: wrap; justify-content: space-between; gap: 20px; margin: auto; max-width: var(--measure); border-top: 1px solid var(--line); padding: 23px 0 35px; font-size: 12px; color: var(--muted); }
body > .site-footer { width: calc(100% - 48px); }
.article-shell { max-width: 1148px; margin: auto; padding: 56px 24px 70px; display: grid; grid-template-columns: 160px minmax(0,660px) 160px; column-gap: 40px; justify-content: center; }
.article-sidebar { align-self: start; position: sticky; top: 32px; max-height: calc(100vh - 64px); overflow: auto; font-size: 12px; }
.eyebrow { color: var(--muted); font: 12px/1.5 var(--sans); margin: 0 0 18px; }
.article-sidebar .toc ul { list-style: none; padding: 0; margin: 0; }
.article-sidebar .toc > ul > li > a { display: none; }
.article-sidebar .toc li { margin: 0 0 12px; }
.article-sidebar .toc a { color: var(--muted); text-decoration: none; }
.article-sidebar .toc a:hover { color: var(--green); }
.article-content { min-width: 0; font: 17.5px/1.7 var(--sans); }
.article-content h1 { font-size: 34px; }
.article-content h1 + .article-meta { padding: 16px 0; margin: 20px 0 32px; border-top: 1px solid var(--line); border-bottom: 1px solid var(--line); }
.article-content h1, .article-content h2, .article-content h3 { scroll-margin-top: 35px; }
.article-content li { margin-bottom: 8px; }
.article-content pre { padding: 18px; background: #f5f7f8; border: 1px solid var(--line); margin: 26px 0; }
.article-content :not(pre) > code { background: #f3f5f6; border-radius: 2px; padding: 1px 3px; overflow-wrap: anywhere; }
.article-content blockquote { margin: 24px 0; border-left: 2px solid #88a6bc; padding-left: 20px; color: #485c6a; }
.source-quote { margin: 24px 0; border-left: 2px solid #88a6bc; padding: 0 0 0 20px; color: #485c6a; }
.source-quote p { margin: 0; }
.article-content table { display: block; overflow: auto; max-width: 100%; border-collapse: collapse; margin: 26px 0; font: 14px/1.6 var(--sans); }
.article-content th, .article-content td { padding: 10px 13px; border-bottom: 1px solid var(--line); text-align: left; min-width: 120px; vertical-align: top; }
.article-content th { background: var(--soft); }
.article-content figure img { width: 100%; }
.figure-wide { width: 100%; max-width: 100%; }
.lean-example { min-width: 0; margin: 26px 0; }
.lean-example .lean-code { margin-bottom: 0; }
.lean-example pre code { font: inherit; background: transparent; padding: 0; }
.lean-token { color: #245d91; cursor: help; text-decoration: underline dotted #8ca6b7; text-underline-offset: 4px; }
.lean-code { font: 16px/1.75 var(--mono); white-space: pre-wrap; overflow-wrap: anywhere; }
.lean-code code { font: inherit; }
.lean-syntax.keyword { color: #7b3693; }
.lean-syntax.comment { color: #64717b; }
.lean-syntax.string { color: #21734b; }
.lean-syntax.number { color: #905117; }
.lean-syntax.builtin { color: #245d91; }
.lean-syntax.operator { color: #49596a; }
@media (max-width: 600px) {
  .lean-code { font-size: 14px; }
}
.lean-token, .lean-step { scroll-margin-top: calc(var(--reader-offset, 86px) + 12px); scroll-margin-bottom: 60px; }
.lean-token:hover, .lean-token:focus-visible { background: #e1edf4; }
.lean-step { cursor: help; border-bottom: 1px dotted #aac0cf; }
.lean-step:focus-visible { background: #e1edf4; }
.lean-context { border: 1px solid var(--line); border-top: 0; padding: 10px 16px; }
.lean-context summary { cursor: pointer; color: var(--muted); font: 12px/1.5 var(--sans); }
.lean-example .lean-code { max-height: none; }
.lean-context .lean-code { max-height: 540px; overflow: auto; }
.lean-proof { border: 1px solid var(--line); border-top: 0; padding: 10px 16px; }
.lean-proof > summary { cursor: pointer; color: var(--green); font: 13px/1.5 var(--sans); }
.lean-proof .lean-code { padding: 14px 0 0; border: 0; margin: 0; background: transparent; }
.lean-result { margin: 26px 0; padding: 14px 0; border-top: 1px solid var(--line); }
.lean-result > summary { cursor: pointer; color: var(--green); font: 14px/1.6 var(--sans); }
.lean-result .lean-example { margin-bottom: 0; }
.chapter-report { display: flex; align-items: center; gap: 6px; flex-shrink: 0; }
.chapter-report .reader-button { font: 13px/1.4 var(--sans); white-space: nowrap; }
body #chapterBar { padding: 8px max(20px, calc((100vw - 1100px) / 2)); gap: 10px; }
body #chapterBar > label { flex: 1; min-width: 0; }
.chapter-bar .chapter-report .reader-button { padding: 7px 10px; }
body .pdf-pane-heading {
  display: flex; flex-direction: column; align-items: flex-start; gap: 8px;
  padding: 10px 12px; border: 1px solid var(--line); background: var(--soft);
}
body .pdf-pane-heading > span { font: 13px/1.5 var(--sans); color: var(--ink); }
body .pdf-pane-actions { display: flex; flex-wrap: wrap; gap: 8px; }
body .pdf-pane-actions .reader-button { font: 13px/1.4 var(--sans); }
body .report-reader .report-controls { display: block; padding: 0; }
body .report-controls #reportPageForm {
  display: flex; flex-wrap: wrap; align-items: center; gap: 8px;
  margin: 0; padding: 10px 12px; border: 1px solid var(--line); border-top: 0;
}
body .report-controls #reportPageForm[hidden] { display: none; }
main .chapter-paper-jump, main > .report-page-link[data-dock="true"] {
  display: block; width: fit-content; margin: 12px 0 24px; padding: 0;
  border: 0; background: transparent; color: var(--green); text-align: left;
  font: 13px/1.5 var(--sans); text-decoration: underline; text-underline-offset: 3px;
}
@media (max-width: 600px) {
  .chapter-bar .chapter-report { flex-basis: 100%; }
  .chapter-bar .chapter-select-label, .chapter-bar label { flex: 1; width: auto; }
}
.lean-output { border: 1px solid var(--line); border-top: 0; padding: 10px 16px; background: #fbfcfd; }
.lean-output summary { cursor: pointer; color: var(--muted); font: 12px/1.5 var(--sans); }
.lean-output pre { margin: 12px 0 0; padding: 0; border: 0; background: transparent; white-space: pre-wrap; overflow-wrap: anywhere; font: 14px/1.65 var(--mono); }
.lean-hover { position: fixed; z-index: 130; width: max-content; max-width: min(560px, calc(100vw - 24px)); max-height: min(400px, 50vh); margin: 0; padding: 14px; overflow: auto; border: 1px solid #a7bbc9; border-radius: 4px; background: #f6f9fc; color: var(--ink); box-shadow: 0 4px 18px #142f3c26; white-space: pre-wrap; overflow-wrap: anywhere; font: 14px/1.65 var(--mono); }
.lean-hover[hidden] { display: none; }
.data-chart { margin: 34px 0; }
.data-chart img { width: 100%; }
.math-display { overflow-x: auto; margin: 24px 0; padding: 10px 0; text-align: center; font-size: 18px; }
.article-citation { margin-top: 36px; padding-top: 20px; border-top: 1px solid var(--line); }
main > .article-citation { max-width: var(--measure); margin-left: auto; margin-right: auto; }
.article-citation summary { cursor: pointer; color: var(--green); font: 15px/1.6 var(--sans); }
.article-citation p { font: 15px/1.7 var(--sans); }
.article-citation pre { white-space: pre-wrap; overflow-wrap: anywhere; font: 14px/1.7 var(--mono); }
.article-citation pre code { font-size: inherit; }
.article-citation > a { font: 14px/1.6 var(--sans); }
.article-references li { margin-bottom: 12px; }
.katex-display { max-width: 100%; overflow-x: auto; overflow-y: hidden; padding: 3px 0; }
.interactive { margin: 34px 0; border-top: 1px solid #ccd9e2; border-bottom: 1px solid #ccd9e2; padding: 20px 0; font: 14px/1.6 var(--sans); }
.interactive label { display: grid; gap: 5px; color: var(--muted); font-size: 12px; }
.interactive select { padding: 7px 10px; max-width: 100%; color: var(--ink); font: 14px var(--sans); background: white; border: 1px solid #ccd9e2; border-radius: 3px; }
.interactive output { display: block; }
.margin-controls { display: flex; align-items: center; flex-wrap: wrap; gap: 24px; margin-bottom: 18px; }
.margin-controls input { width: 220px; accent-color: var(--green); }
.margin-demo svg { width: 100%; max-width: 600px; }
.margin-demo .margin-verdict { margin: 12px 0 0; font-size: 14px; }
.sum-trees { display: grid !important; grid-template-columns: 1fr 1fr; gap: 20px; margin: 22px 0 12px; }
.sum-tree h3 { font: 500 15px/1.5 var(--sans); margin: 0 0 5px; letter-spacing: 0; }
.sum-tree svg { width: 100%; height: auto; }
.sum-tree p { margin: 4px 0 0; font-size: 13px; color: var(--muted); }
.prompt-controls { display: flex; flex-wrap: wrap; gap: 12px; margin-bottom: 24px; }
.prompt-line { display: flex; align-items: center; flex-wrap: wrap; gap: 8px; padding: 14px 0; }
.prompt-token { display: grid; gap: 5px; min-width: 49px; padding: 9px 10px; background: #edf3f7; border: 1px solid #d5e2eb; text-align: center; font: 500 19px/1.2 var(--sans); }
.prompt-token small { font: 10px/1.3 var(--sans); color: var(--muted); }
.prompt-token.delimiter { background: #e8f2ec; border-color: #a8c8b5; }
.prompt-choice { color: #2d7150; font-size: 15px; margin-bottom: 15px; }
.evidence-figure { display: grid; grid-template-columns: 1fr 1fr 1fr; gap: 14px; font: 13px/1.5 var(--sans); }
.evidence-figure div { padding: 15px 10px 12px; border-top: 2px solid #7399b4; }
.evidence-figure strong, .evidence-figure span { display: block; }
.evidence-figure span { margin-top: 7px; color: var(--muted); }
.evidence-figure figcaption { grid-column: 1/-1; }
.recurrence-lane { display: grid; grid-template-columns: 70px minmax(0,1fr); align-items: center; gap: 12px; margin: 12px 0; }
.recurrence-label { color: var(--muted); font-size: 12px; }
.recurrence-trace { display: flex; align-items: center; flex-wrap: wrap; gap: 8px; }
.recurrence-value { min-width: 40px; padding: 8px 10px; border: 1px solid #b9ccd9; background: #edf3f7; text-align: center; font: 500 18px/1.3 var(--sans); }
.recurrence-arrow { color: var(--muted); }
.recurrence-result { margin: 20px 0 0; color: var(--ink); }
.token-figure { font: 14px/1.5 var(--sans); }
.token-figure > div:not(.causal-mask) { display: grid; grid-template-columns: 62px repeat(4,1fr); gap: 8px; margin-bottom: 10px; }
.token-figure span { padding: 8px 3px; background: #edf3f7; text-align: center; }
.token-figure .row-label { text-align: left; background: none; color: var(--muted); }
.mask-controls { display: flex; gap: 8px; flex-wrap: wrap; align-items: center; margin-top: 22px; }
.mask-controls button { font: 14px var(--sans); cursor: pointer; padding: 6px 12px; border: 1px solid #d3dde4; background: white; border-radius: 3px; color: #445665; }
.mask-controls button[aria-pressed="true"] { color: #165180; border-color: #5589b0; background: #edf4f9; }
.causal-mask { max-width: 440px; margin: 15px auto; }
.causal-mask svg { width: 100%; height: auto; }
.causal-mask p { font: 13px/1.5 var(--sans); color: var(--muted); }
.project-links, .page-nav { display: flex; flex-wrap: wrap; gap: 20px; margin-top: 35px; padding-top: 18px; border-top: 1px solid var(--line); font: 12px/1.6 var(--sans); }
.page-nav { justify-content: space-between; }
details.proof-note { padding: 14px 0; border-top: 1px solid var(--line); font-size: 14px; color: #50616e; margin: 25px 0; }
details.proof-note summary { cursor: pointer; color: #286493; }
details.proof-note p { margin: 14px 0 0; }
@media(min-width:851px) { .article-sidebar summary { display: none; } }
@media(max-width:1100px) { .article-shell { grid-template-columns: minmax(0,660px); } .article-sidebar { display: none; } .figure-wide { width: 100%; } .essay-entry .entry-kind { position: static; width: auto; margin-bottom: 12px; } }
@media(max-width:850px) {
  .article-shell { grid-template-columns: minmax(0,660px); padding-top: 28px; gap: 24px; }
  .article-sidebar { position: static; max-height: none; }
  .article-sidebar .eyebrow { display: none; }
  .article-sidebar details { padding-bottom: 10px; border-bottom: 1px solid var(--line); }
  .article-sidebar .toc { margin-top: 12px; }
  .wordmark span { display: block; padding: 0; font-size: 11px; }
}
@media(max-width:600px) {
  .site-header { padding: 13px 18px; gap: 10px; }
  .site-header nav { gap: 13px; font-size: 11px; }
  .topbar-actions { gap: 10px; font-size: 11px; }
  .topbar-actions .reader-button { font-size: 11px; padding: 6px; }
  .home { padding: 0 20px; }
  .intro { padding-top: 30px; }
  .intro h1, .article-content h1 { font-size: 28px; }
  .intro p { font-size: 17px; }
  .article-shell { padding: 24px 20px 50px; }
  .article-content { font-size: 17px; }
  h2 { font-size: 23px; }
  .essay-entry { display: block; padding: 25px 0; }
  .essay-entry .entry-kind { font-size: 12px; margin-bottom: 10px; }
  .sum-trees { grid-template-columns: 1fr; gap: 24px; }
  .evidence-figure { grid-template-columns: 1fr; }
  .evidence-figure div { padding-left: 0; }
  .figure-wide { overflow-x: auto; }
  .figure-wide img { min-width: 810px; width: 810px; max-width: none; }
  .figure-wide::before { content: "Scroll across the plot →"; display: block; margin-bottom: 8px; color: var(--muted); font-size: 12px; }
  .token-figure > div:not(.causal-mask) { grid-template-columns: 50px repeat(4,1fr); gap: 5px; font-size: 12px; }
  .site-footer { padding: 22px 0 30px; }
  body > .site-footer { width: calc(100% - 40px); }
}
@media(prefers-reduced-motion:reduce) { html { scroll-behavior: auto; } }