/* Shared only by the two Lean formalization pages. */
:root {
  --paper: #faf9f7;
  --ink: #242927;
  --body: #414844;
  --muted: #646c65;
  --line: #dddeda;
  --accent: #2f5575;
  --note: #edf2f1;
  --serif: "Newsreader", Georgia, serif;
  --sans: -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
}

* { box-sizing: border-box; }
html { scroll-padding-top: 24px; }
body { margin: 0; background: var(--paper); }
x-dc { display: block; }
::selection { background: #d9e6e6; }
a { color: var(--accent); text-underline-offset: 4px; text-decoration-thickness: 1px; }
a:hover { text-decoration-thickness: 2px; }
a:focus-visible { outline: 2px solid var(--accent); outline-offset: 5px; border-radius: 1px; }
[tabindex="-1"]:focus { outline: none; }

.lean-page {
  min-height: 100vh;
  display: flex;
  flex-direction: column;
  color: var(--ink);
  font-family: var(--sans);
  -webkit-font-smoothing: antialiased;
}

.skip-link {
  position: absolute;
  z-index: 10;
  top: 12px;
  left: 16px;
  padding: 10px 16px;
  background: var(--paper);
  transform: translateY(-160%);
}
.skip-link:focus { transform: translateY(0); }

.site-header { border-bottom: 1px solid var(--line); }
.site-nav {
  max-width: 1080px;
  margin: 0 auto;
  padding: 23px 32px;
  display: flex;
  justify-content: space-between;
  align-items: center;
  gap: 20px;
}
.site-identity {
  flex-shrink: 0;
  color: var(--ink);
  font-family: var(--serif);
  font-size: 24px;
  font-weight: 500;
  text-decoration: none;
}
.site-links { display: flex; flex-wrap: wrap; gap: 8px 24px; }
.site-links a {
  padding: 5px 0;
  color: var(--body);
  font-size: 13px;
  line-height: 1.5;
  text-decoration: none;
}
.site-links a:hover,
.site-links a[aria-current] {
  color: var(--accent);
  text-decoration: underline;
  text-underline-offset: 7px;
}

.reading-column {
  width: min(100% - 48px, 720px);
  flex: 1;
  margin: 0 auto;
  padding: 48px 0 68px;
}
.note-header { margin-bottom: 32px; }
.back-link {
  display: inline-block;
  padding: 6px 0;
  margin-bottom: 29px;
  color: var(--muted);
  font-size: 13px;
  text-decoration: none;
}
.back-link:hover { color: var(--accent); text-decoration: underline; }
h1, h2 { color: var(--ink); font-family: var(--serif); font-weight: 400; }
h1 {
  margin: 0;
  font-size: clamp(38px, 5.5vw, 58px);
  line-height: 1.08;
  letter-spacing: -0.025em;
  text-wrap: balance;
}
.lede {
  max-width: 36em;
  margin: 20px 0 0;
  color: var(--muted);
  font-size: 17px;
  line-height: 1.65;
}
.note-meta {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 0 7px;
  margin: 21px 0 0;
  color: var(--muted);
  font-size: 12px;
  line-height: 1.8;
}
.prose { color: var(--body); font-size: 17px; line-height: 1.8; }
.prose p { margin: 0 0 20px; }
.prose section { margin-top: 38px; }
.prose h2 { margin: 0 0 18px; font-size: 30px; line-height: 1.2; }

.proof-note {
  margin: 28px 0 34px;
  padding: 18px 22px;
  background: var(--note);
  border-left: 3px solid var(--accent);
  font-size: 15px;
  line-height: 1.7;
}
.proof-note strong { display: block; color: var(--ink); font-weight: 600; margin-bottom: 3px; }
.proof-note span { display: block; }

.formula-pair {
  display: grid;
  grid-template-columns: repeat(2, minmax(0, 1fr));
  gap: 18px;
  margin: 26px 0;
  padding: 20px 0;
  border-top: 1px solid var(--line);
  border-bottom: 1px solid var(--line);
}
.formula-pair p { margin: 0; color: var(--ink); font-family: var(--serif); font-size: 18px; line-height: 1.55; }
.formula-pair p > span { display: block; margin-bottom: 7px; color: var(--muted); font-family: var(--sans); font-size: 11px; font-weight: 500; letter-spacing: 0.06em; text-transform: uppercase; }
.architecture-list { margin: 24px 0 0; padding: 0; list-style: none; counter-reset: architecture; }
.architecture-list li { position: relative; margin: 0; padding: 0 0 22px 42px; counter-increment: architecture; }
.architecture-list li + li { padding-top: 22px; border-top: 1px solid var(--line); }
.architecture-list li::before { position: absolute; top: 0; left: 0; color: var(--accent); font-family: var(--serif); font-size: 25px; line-height: 1; content: counter(architecture, decimal-leading-zero); }
.architecture-list li + li::before { top: 22px; }
.architecture-list strong { color: var(--ink); font-weight: 600; }

/* Editorial figures and the source-linked proof map. */
.article-hero { margin: 0 0 34px; }
.article-hero img { display: block; width: 100%; height: auto; background: var(--note); }
.article-hero figcaption,
.proof-map figcaption,
.formalization-workflow figcaption { margin-top: 13px; color: var(--muted); font-size: 12px; line-height: 1.65; }
.proof-map {
  --checked-ink: #315f53;
  --checked-fill: #edf3ee;
  --checked-line: #aebfb3;
  --open-ink: #7b512e;
  --open-fill: #f6f1e8;
  --open-line: #cdbba6;
  margin: 25px 0 30px;
  padding: 22px 0 0;
  border-top: 1px solid var(--line);
}
.map-heading { display: flex; flex-wrap: wrap; justify-content: space-between; gap: 4px 18px; margin-bottom: 17px; color: var(--muted); font-size: 12px; }
.map-heading > span:first-child { color: var(--ink); font-weight: 500; }
.proof-step { min-width: 0; background: var(--checked-fill); border: 1px solid var(--checked-line); }
.proof-step summary { position: relative; padding: 15px 34px 14px 16px; cursor: pointer; list-style: none; }
.proof-step summary::-webkit-details-marker { display: none; }
.proof-step summary::after { position: absolute; right: 14px; top: 17px; content: "+"; color: var(--muted); font-size: 17px; line-height: 1; }
.proof-step[open] > summary::after { content: "−"; }
.proof-step summary:focus-visible { outline: 2px solid var(--accent); outline-offset: 3px; }
.proof-step summary:hover .step-title { text-decoration: underline; text-underline-offset: 3px; }
.step-title { display: block; color: var(--ink); font-size: 15px; font-weight: 500; line-height: 1.45; }
.step-subtitle { display: block; margin-top: 4px; color: var(--body); font-size: 12px; line-height: 1.6; }
.step-state { display: block; margin-top: 9px; color: var(--checked-ink); font-size: 11px; font-weight: 600; line-height: 1.5; }
.step-state::before { content: "✓"; margin-right: 5px; }
.proof-step.is-open { background: var(--open-fill); border-color: var(--open-line); border-style: dashed; }
.is-open .step-state { color: var(--open-ink); }
.is-open .step-state::before { content: "○"; }
.proof-step.is-conditional { background: #edf2f7; border-color: #b4c2d1; }
.is-conditional .step-state { color: var(--accent); }
.is-conditional .step-state::before { content: "⇒"; }
.step-detail { padding: 0 16px 16px; color: var(--body); font-size: 13px; line-height: 1.7; }
.step-detail a { display: block; margin-top: 8px; }
.map-foundation { position: relative; text-align: center; }
.map-foundation::after { position: absolute; left: 50%; top: 100%; height: 20px; border-left: 1px solid var(--line); content: ""; }
.proof-lanes { position: relative; display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 24px; padding-top: 20px; margin-top: 20px; }
.proof-lanes::before { position: absolute; left: calc(25% - 6px); right: calc(25% - 6px); top: 0; border-top: 1px solid var(--line); content: ""; }
.proof-lane { position: relative; display: flex; flex-direction: column; min-width: 0; }
.proof-lane::before { position: absolute; left: 50%; top: -20px; height: 17px; border-left: 1px solid var(--line); content: ""; }
.proof-lane h3 { margin: 0 0 14px; color: var(--muted); font-size: 12px; line-height: 1.6; font-weight: 500; text-align: center; }
.proof-lane ol { margin: 0; padding: 0; list-style: none; }
.proof-lane li + li::before { display: block; padding: 5px 0; color: var(--muted); font-size: 17px; line-height: 1; text-align: center; content: "↓"; }
.proof-lane::after { display: block; flex: 1; min-height: 20px; margin: 0 auto; border-left: 1px solid var(--line); content: ""; }
.map-join { position: relative; padding: 10px 0 27px; color: var(--muted); font-size: 11px; line-height: 1.6; text-align: center; }
.map-join::before { position: absolute; top: 0; left: calc(25% - 6px); right: calc(25% - 6px); border-top: 1px solid var(--line); content: ""; }
.map-join::after { position: absolute; left: 0; right: 0; bottom: 4px; content: "↓"; font-size: 17px; }
.map-goal { text-align: center; }
.formalization-workflow { margin: 24px 0 28px; padding: 20px 0; border-top: 1px solid var(--line); border-bottom: 1px solid var(--line); }
.formalization-workflow ol { display: grid; grid-template-columns: repeat(4, minmax(0, 1fr)); gap: 24px; margin: 0; padding: 0; list-style: none; }
.formalization-workflow li { position: relative; min-width: 0; }
.formalization-workflow li:not(:last-child)::after { position: absolute; top: 0; right: -19px; color: var(--muted); content: "→"; font-size: 14px; }
.formalization-workflow strong { display: block; color: var(--ink); font-size: 13px; line-height: 1.5; font-weight: 500; }
.formalization-workflow li span { display: block; margin-top: 6px; color: var(--muted); font-size: 12px; line-height: 1.65; }

@media (max-width: 560px) {
  .formula-pair { grid-template-columns: 1fr; }
  .proof-lanes { grid-template-columns: 1fr; gap: 26px; padding-top: 0; margin-top: 26px; }
  .map-foundation::after, .proof-lanes::before, .proof-lane::before, .proof-lane::after, .map-join::before { display: none; }
  .proof-lane h3 { text-align: left; }
  .map-join { margin-top: 14px; }
  .formalization-workflow ol { grid-template-columns: 1fr; gap: 24px; }
  .formalization-workflow li:not(:last-child)::after { top: auto; bottom: -23px; left: 0; right: auto; content: "↓"; }
}

.resources ul { margin: 0; padding: 0; list-style: none; }
.resources li { margin: 0 0 16px; font-size: 15px; line-height: 1.6; }
.resources li a { font-weight: 500; }
.resources li > span { display: block; margin-top: 3px; color: var(--muted); font-size: 14px; }
.resources a span { margin-left: 3px; font-size: 13px; }
.prose .reference {
  padding-top: 24px;
  margin: 34px 0 0;
  border-top: 1px solid var(--line);
  color: var(--muted);
  font-size: 13px;
  line-height: 1.7;
}

.collection { padding-top: 68px; }
.eyebrow {
  margin: 0 0 18px;
  color: var(--muted);
  font-family: var(--sans);
  font-size: 11px;
  font-weight: 500;
  line-height: 1.5;
  letter-spacing: 0.08em;
  text-transform: uppercase;
}
.collection-intro { color: var(--body); font-size: 17px; line-height: 1.8; margin: 0; }
.project-list { margin-top: 42px; }
.project { padding: 24px 0 29px; border-top: 1px solid var(--line); border-bottom: 1px solid var(--line); }
.project-meta { margin: 0 0 13px; color: var(--muted); font-size: 12px; line-height: 1.6; }
.project-meta span { margin: 0 6px; }
.project h2 { margin: 0; font-size: 32px; line-height: 1.2; }
.project h2 a { color: var(--ink); text-decoration: none; }
.project h2 a:hover { color: var(--accent); text-decoration: underline; }
.project h2 span { display: inline-block; margin-left: 5px; color: var(--accent); font-size: 20px; }
.project > p:not(.project-meta) { margin: 17px 0 23px; color: var(--body); font-size: 16px; line-height: 1.8; }
.project-links { display: flex; flex-wrap: wrap; gap: 14px 28px; font-size: 14px; line-height: 1.6; }

.site-footer {
  display: flex;
  flex-wrap: wrap;
  justify-content: space-between;
  gap: 12px 24px;
  width: min(100% - 48px, 720px);
  margin: 0 auto;
  padding: 24px 0 32px;
  border-top: 1px solid var(--line);
  color: var(--muted);
  font-size: 12px;
  line-height: 1.7;
}
.site-footer > div { display: flex; flex-wrap: wrap; gap: 20px; }
.site-footer a { color: var(--muted); text-decoration: none; }
.site-footer a:hover { color: var(--accent); text-decoration: underline; }

@media (max-width: 740px) {
  .site-nav { align-items: flex-start; flex-direction: column; gap: 12px; padding: 20px 24px; }
  .site-links { gap: 6px 19px; }
  .site-links a { padding: 8px 0; }
  .reading-column { padding-top: 32px; padding-bottom: 48px; }
  .back-link { margin-bottom: 24px; }
  .collection { padding-top: 42px; }
}

@media (max-width: 440px) {
  .reading-column, .site-footer { width: calc(100% - 36px); }
  .site-nav { padding-right: 18px; padding-left: 18px; }
  .site-links { gap: 4px 16px; }
  .proof-note { padding: 16px 18px; }
  .prose { font-size: 16px; }
  .prose h2 { font-size: 28px; }
  .project h2 { font-size: 29px; }
}

@media print {
  .site-header, .skip-link, .back-link, .site-footer { display: none; }
  body, .lean-page { background: white; color: black; }
  .reading-column { width: 100%; max-width: none; padding: 0; }
  h1 { font-size: 32px; }
  .prose { font-size: 11pt; }
  .proof-note { background: none; border: 1px solid #777; }
  h2 { break-after: avoid; }
  .proof-step, .resources li { break-inside: avoid; }
  .proof-step summary::after { display: none; }
}