:root {
  color-scheme: light;
  --ink: #141414;
  --muted: #525252;
  --accent: #0036a3;
  --accent-ink: #ffffff;
  --brand: #99bbff;
  --brand-light: #ebf1ff;
  --brand-gradient: linear-gradient(327deg, #99bbff 0%, #e0ebff 100%);
  --paper: #ffffff;
  --card: #ffffff;
  --line: #c2d6ff;
  --panel: #f5f7fb;
  --focus: #005fcc;
  --polymath: #285ea8;
}

/* Full interactive blueprint. Pandoc keeps the source document's prose,
   mathematical environments, and ordering; these rules provide the visual
   hierarchy without changing that structure. */
.full-blueprint {
  max-width: 76rem;
  margin: 2rem auto 4rem;
  color: var(--ink);
  font-size: 1.08rem;
  line-height: 1.5;
}

.full-blueprint h1,
.full-blueprint h2,
.full-blueprint h3,
.full-blueprint h4 {
  max-width: none;
  text-align: left;
  line-height: 1.25;
  letter-spacing: -0.01em;
}

.full-blueprint h1 {
  margin: 2.6rem 0 0.8rem;
  padding-bottom: 0.42rem;
  border-bottom: 2px solid var(--accent);
  font-size: clamp(1.65rem, 2.5vw, 2rem);
}
.full-blueprint h2 {
  margin: 2rem 0 0.65rem;
  padding-bottom: 0.3rem;
  border-bottom: 1px solid var(--line);
  font-size: clamp(1.3rem, 2vw, 1.55rem);
}
.full-blueprint h3 { margin: 1.5rem 0 0.5rem; font-size: clamp(1.12rem, 1.7vw, 1.3rem); }
.full-blueprint h4 { margin: 1.2rem 0 0.4rem; color: var(--muted); font-size: 1.05rem; }

.full-blueprint p { margin: 0.55rem 0; }

.full-blueprint ul,
.full-blueprint ol {
  margin: 0.65rem 0 0.9rem;
  padding-left: 2rem;
}

.full-blueprint li { margin: 0.25rem 0; padding-left: 0.3rem; }
.full-blueprint li::marker { color: var(--accent); font-weight: 700; }

.full-blueprint .math.display {
  display: block;
  max-width: 100%;
  margin: 0.65rem 0;
  padding: 0.25rem 0.4rem;
  overflow-x: auto;
  overflow-y: hidden;
}

.full-blueprint :is(.definition, .notation, .lemma, .sublemma, .proposition, .theorem) {
  margin: 1.15rem 0 0;
  padding: 0.9rem 1.25rem;
  border: 1px solid var(--line);
  border-left: 0.3rem solid var(--accent);
  border-radius: 0.65rem;
  background: var(--card);
  scroll-margin-top: 7rem;
}

.full-blueprint .proof {
  margin: 0.7rem 0 1.15rem;
  padding: 0.75rem 1.25rem;
  border: 1px solid var(--line);
  border-radius: 0.65rem;
  background: var(--panel);
}

.full-blueprint .leanlinks,
.full-blueprint .uses-statement {
  margin: 0;
  padding: 0.32rem 0.25rem;
  border: 0;
  background: transparent;
  font-size: 0.9rem;
}

.full-blueprint :is(.uses-statement, .uses-proof) p { margin: 0; }
.full-blueprint :is(.uses-statement, .uses-proof) a {
  font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
  font-size: 0.86em;
}

.full-blueprint .proof .uses-proof {
  margin: 0.65rem 0 0;
  padding: 0.55rem 0 0;
  border: 0;
  border-top: 1px solid var(--line);
  background: transparent;
  font-size: 0.9rem;
}

.full-blueprint .lean-link {
  display: inline-block;
  margin: 0.2rem 0.3rem 0.2rem 0;
  padding: 0.2rem 0.5rem;
  border-radius: 0.35rem;
  background: var(--brand-light);
  font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
  font-size: 0.82rem;
  overflow-wrap: anywhere;
}

.full-blueprint [hidden] { display: none !important; }

@media (max-width: 650px) {
  .full-blueprint :is(.definition, .notation, .lemma, .sublemma, .proposition, .theorem),
  .full-blueprint .proof,
  .full-blueprint .leanlinks,
  .full-blueprint :is(.uses-statement, .uses-proof, .uses-notation) {
    padding-inline: 1rem;
  }
}

*, *::before, *::after { box-sizing: border-box; }
html { background: var(--paper); scroll-behavior: smooth; }
body {
  width: min(76rem, 100%);
  margin: 0 auto;
  padding: clamp(1rem, 3vw, 2rem) clamp(1.25rem, 4vw, 3rem) 3rem;
  color: var(--ink);
  background: var(--paper);
  font-family: Inter, ui-sans-serif, system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  font-size: 1rem;
  line-height: 1.65;
}
.skip-link {
  position: fixed;
  z-index: 100;
  top: 0.75rem;
  left: 0.75rem;
  padding: 0.7rem 1rem;
  color: #fff;
  background: var(--accent);
  border-radius: 0.35rem;
  transform: translateY(-160%);
}
.skip-link:focus { transform: translateY(0); }
:focus-visible { outline: 3px solid var(--focus); outline-offset: 3px; }

.hero {
  max-width: 70rem;
  margin: 0 auto clamp(3rem, 6vw, 4.5rem);
  padding: clamp(1.5rem, 5vw, 4rem);
  border-radius: 1.25rem;
  background: var(--brand-gradient);
  text-align: center;
}
.brand { display: block; width: 9.5rem; margin: 0 auto 1.5rem; }
.brand img { display: block; width: 100%; height: auto; }
.brand-small { width: 7.5rem; margin: 0 0 1.5rem; }
.eyebrow {
  margin: 0 0 1rem;
  color: var(--accent);
  font-size: 0.78rem;
  font-weight: 750;
  line-height: 1.2;
  letter-spacing: 0.14em;
  text-transform: uppercase;
}
h1 {
  max-width: 34ch;
  margin: 0 auto;
  font-size: clamp(2rem, 4.5vw, 3.2rem);
  line-height: 1.12;
  letter-spacing: -0.025em;
  text-wrap: balance;
}
.sub { margin: 1.1rem 0 0.9rem; color: var(--muted); font-size: 1.1rem; }
.gist { max-width: 58ch; margin: 0 auto 2rem; font-size: 1.02rem; }
.actions { display: flex; flex-wrap: wrap; justify-content: center; gap: 0.8rem; }
.actions + .actions { margin-top: 0.8rem; }
.actions :is(a, .button) {
  display: inline-flex;
  min-height: 44px;
  align-items: center;
  justify-content: center;
  padding: 0.75rem 1.25rem;
  border: 1.5px solid var(--accent);
  border-radius: 999px;
  font-size: 0.95rem;
  font-weight: 700;
  line-height: 1;
  text-decoration: none;
  transition: filter .15s ease, background .15s ease;
}
.actions .primary { color: var(--accent-ink); background: var(--accent); }
.actions .primary:hover { filter: brightness(1.12); }
.actions .disabled,
.actions .disabled:hover {
  cursor: default;
  filter: none;
  opacity: 1;
}
.actions .secondary { color: var(--accent); background: transparent; }
.actions .secondary:hover { background: color-mix(in srgb, var(--accent) 8%, transparent); }
.actions .disabled {
  border-color: #7da8f5;
  color: #17478f;
  background: #cfe0ff;
}

.two-col {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(21rem, 1fr));
  column-gap: 3rem;
  align-items: start;
}
.page-header { margin-bottom: clamp(2rem, 5vw, 3.5rem); }
.page-header .back {
  color: var(--accent);
  font: 650 0.9rem/1 system-ui, sans-serif;
  text-decoration: none;
}
.page-header .back:hover { text-decoration: underline; }
.page-header h1 {
  max-width: none;
  margin: 0.9rem 0 0;
  font-size: clamp(1.7rem, 3.5vw, 2.5rem);
  text-align: left;
}
.paper-actions { justify-content: flex-start; margin-top: 1.2rem; }
h2 {
  margin: 2.6rem 0 1rem;
  color: var(--ink);
  font-size: clamp(1.4rem, 2.2vw, 1.75rem);
  font-weight: 760;
  line-height: 1.25;
  letter-spacing: -0.018em;
}
h3 { margin: 0.75rem 0 0; font-size: clamp(1.15rem, 1.5vw, 1.3rem); line-height: 1.35; }
.prose { max-width: 66ch; }
.prose p { margin: 0 0 1rem; }
main a, footer a { color: var(--accent); text-decoration-thickness: 0.1em; text-underline-offset: 0.18em; }
main a:hover, footer a:hover { text-decoration-color: var(--accent); }
.section-intro { max-width: 66ch; color: var(--muted); }

.resource-grid {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(17rem, 1fr));
  gap: 1rem;
}
.resource-grid.grid-2col { grid-template-columns: repeat(2, minmax(0, 1fr)); }
.resource-card {
  padding: 1.3rem 1.4rem;
  border: 1px solid var(--line);
  border-radius: 0.8rem;
  background: var(--card);
  box-shadow: 0 8px 24px rgba(0, 54, 163, 0.07);
}
.source-card { border-top: 4px solid var(--accent); }
.source-card.polymath { border-top-color: var(--polymath); }
.resource-card p { margin: 0.5rem 0 0; color: var(--muted); font-size: 0.95rem; }
.resource-card .res-title { font-size: 1.12rem; font-weight: 700; text-underline-offset: 0.25em; }
.res-title-soon { color: var(--ink); text-decoration: none; }
.card-heading { display: flex; flex-wrap: wrap; align-items: baseline; justify-content: space-between; gap: 0.55rem; }
.source-kicker {
  color: var(--muted);
  font: 700 0.68rem/1.3 system-ui, sans-serif;
  letter-spacing: 0.08em;
  text-transform: uppercase;
}
.badge {
  display: inline-block;
  padding: 0.14rem 0.55rem;
  border: 1px solid var(--accent);
  border-radius: 999px;
  color: var(--accent);
  background: color-mix(in srgb, var(--accent) 8%, transparent);
  font: 700 0.64rem/1.4 system-ui, sans-serif;
  letter-spacing: 0.05em;
  text-transform: uppercase;
}
.badge-solid { color: var(--accent-ink); background: var(--accent); }
.badge-amber { color: var(--polymath); border-color: var(--polymath); background: color-mix(in srgb, var(--polymath) 9%, transparent); }
.card-links { display: flex; flex-wrap: wrap; gap: 0.9rem; padding-top: 0.3rem; }

.proof-route {
  display: grid;
  grid-template-columns: 1fr auto 1fr auto 1fr auto 1fr;
  gap: 0.7rem;
  align-items: stretch;
}
.route-stage {
  display: flex;
  gap: 0.75rem;
  padding: 1rem;
  border: 1px solid var(--line);
  border-radius: 0.7rem;
  background: var(--card);
}
.route-stage div { display: flex; flex-direction: column; gap: 0.3rem; }
.route-stage span:not(.route-number) { color: var(--muted); font-size: 0.86rem; }
.route-number {
  display: grid;
  flex: 0 0 1.7rem;
  width: 1.7rem;
  height: 1.7rem;
  place-items: center;
  border-radius: 50%;
  color: var(--accent-ink);
  background: var(--accent);
  font: 700 0.75rem/1 system-ui, sans-serif;
}
.route-arrow { align-self: center; color: var(--muted); font-size: 1.3rem; }
.result-stage { border-color: var(--accent); }

.process-section {
  margin-top: 3rem;
  padding: clamp(1.5rem, 4vw, 2.6rem);
  overflow: hidden;
  border: 1px solid var(--line);
  border-radius: 1.1rem;
  background: linear-gradient(145deg, #f7faff 0%, var(--brand-light) 100%);
}
.process-section h2 { margin-top: 0; color: var(--accent); }
.process-section .section-intro { margin-bottom: 1.7rem; }
.process-grid {
  position: relative;
  display: grid;
  grid-template-columns: repeat(3, minmax(0, 1fr));
  gap: 1.15rem;
  margin: 0;
  padding: 0;
  list-style: none;
}
.process-grid::before {
  position: absolute;
  z-index: 0;
  top: 2.65rem;
  right: 10%;
  left: 10%;
  height: 2px;
  background: var(--brand);
  content: "";
}
.process-step {
  position: relative;
  z-index: 1;
  padding: 1.45rem;
  border: 1px solid var(--line);
  border-radius: 0.9rem;
  background: var(--card);
  box-shadow: 0 10px 26px rgba(0, 54, 163, 0.08);
}
.process-step-heading { display: flex; align-items: center; gap: 0.85rem; }
.process-step h3 { margin: 0; }
.process-step p { margin: 0.9rem 0 0; color: var(--muted); }
.process-number {
  display: grid;
  flex: 0 0 2.45rem;
  width: 2.45rem;
  height: 2.45rem;
  place-items: center;
  border: 4px solid #dbe7ff;
  border-radius: 50%;
  color: var(--accent-ink);
  background: var(--accent);
  box-shadow: 0 0 0 4px var(--card);
  font-size: 0.9rem;
  font-weight: 800;
}
.people-section {
  margin-top: 3rem;
  padding: clamp(1.25rem, 3vw, 2rem);
  border: 1px solid var(--line);
  border-radius: 0.9rem;
  background: var(--brand-light);
}
.people-section h2 { margin-top: 0; color: var(--accent); }
.contributor-legend { display: flex; flex-wrap: wrap; gap: 0.35rem 1.5rem; }
.contributor-legend span { white-space: nowrap; }
.contributor-legend strong, .unified-contributors sup { color: var(--accent); }
.people-list {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(12rem, 1fr));
  gap: 0.55rem 1.5rem;
  margin: 1.25rem 0 0;
  padding: 0;
  list-style: none;
}
.people-list li { position: relative; padding-left: 1rem; }
.people-list li::before { position: absolute; left: 0; color: var(--accent); content: "•"; }
.unified-contributors { display: flex; flex-wrap: wrap; gap: 0.35rem 0; }
.unified-contributors li { padding-left: 0; }
.unified-contributors li::before { content: none; }
.unified-contributors li:not(:last-child)::after { margin-right: 0.45rem; content: ","; }
.unified-contributors sup { margin-left: 0.08em; font-weight: 800; }

.paper-page { width: min(76rem, 100%); }
.scope-note {
  max-width: 74ch;
  margin: 0 0 1.5rem;
  padding: 0.85rem 1rem;
  border-left: 4px solid var(--polymath);
  background: var(--panel);
}
.paper-tools {
  position: sticky;
  z-index: 5;
  top: 0;
  display: grid;
  grid-template-columns: minmax(15rem, 1fr) minmax(12rem, 0.45fr) auto;
  gap: 0.8rem;
  align-items: end;
  margin: 1.5rem 0 2rem;
  padding: 0.9rem;
  border: 1px solid var(--line);
  border-radius: 0.7rem;
  background: color-mix(in srgb, var(--paper) 94%, transparent);
  backdrop-filter: blur(8px);
}
.paper-tools label { display: grid; gap: 0.3rem; }
.paper-tools label span {
  color: var(--muted);
  font: 700 0.68rem/1.2 system-ui, sans-serif;
  letter-spacing: 0.06em;
  text-transform: uppercase;
}
.paper-tools input,
.paper-tools select {
  width: 100%;
  min-height: 2.45rem;
  padding: 0.5rem 0.65rem;
  border: 1px solid var(--line);
  border-radius: 0.45rem;
  color: var(--ink);
  background: var(--card);
  font: 0.92rem/1.2 system-ui, sans-serif;
}
.paper-tools input:focus,
.paper-tools select:focus { outline: 3px solid var(--focus); outline-offset: 1px; }
.paper-tools output { padding-bottom: 0.55rem; color: var(--muted); font: 0.85rem/1 system-ui, sans-serif; white-space: nowrap; }
.paper-section { scroll-margin-top: 7rem; }
.paper-section > h2 {
  margin-top: 3.2rem;
  padding-bottom: 0.55rem;
  border-bottom: 2px solid var(--ink);
}
.node-list { display: grid; gap: 0.85rem; }
.blueprint-node {
  scroll-margin-top: 7rem;
  padding: 1.1rem 1.25rem;
  border: 1px solid var(--line);
  border-radius: 0.7rem;
  background: var(--card);
}
.blueprint-node:target { outline: 3px solid var(--focus); outline-offset: 2px; }
.node-head { display: flex; justify-content: space-between; gap: 1rem; align-items: flex-start; }
.node-head h3 { margin-top: 0.25rem; overflow-wrap: anywhere; }
.node-kind {
  color: var(--muted);
  font: 700 0.64rem/1.2 system-ui, sans-serif;
  letter-spacing: 0.08em;
  text-transform: uppercase;
}
.node-label {
  display: inline-block;
  margin-top: 0.35rem;
  color: var(--muted);
  font: 0.78rem/1.3 ui-monospace, SFMono-Regular, Menlo, monospace;
  text-decoration: none;
}
.node-label:hover { color: var(--accent); }
.status-badge {
  flex: 0 0 auto;
  padding: 0.18rem 0.55rem;
  border: 1px solid var(--muted);
  border-radius: 999px;
  color: var(--muted);
  font: 700 0.62rem/1.35 system-ui, sans-serif;
  letter-spacing: 0.04em;
  text-transform: uppercase;
}
.status-formalized, .status-in-mathlib { color: var(--accent); border-color: var(--accent); }
.status-gap { color: var(--polymath); border-color: var(--polymath); }
.math-copy { white-space: pre-wrap; overflow-wrap: anywhere; }
.statement { margin-top: 0.85rem; }
.dependencies, .lean-row { margin: 0.75rem 0 0; color: var(--muted); font-size: 0.9rem; }
.dependencies a { font-family: ui-monospace, SFMono-Regular, Menlo, monospace; font-size: 0.86em; }
.lean-link {
  display: inline-block;
  padding: 0.02rem 0.5rem;
  border: 1px solid var(--accent);
  border-radius: 999px;
  color: var(--accent);
  font: 0.78rem/1.45 ui-monospace, SFMono-Regular, Menlo, monospace;
  text-decoration: none;
}
.proof { margin-top: 0.8rem; border-top: 1px solid var(--line); padding-top: 0.65rem; }
.proof summary { width: fit-content; cursor: pointer; color: var(--accent); font: 650 0.88rem/1.3 system-ui, sans-serif; }
.proof .math-copy { margin-top: 0.65rem; color: var(--muted); font-size: 0.94rem; }

footer {
  margin-top: 3.2rem;
  padding-top: 1.1rem;
  border-top: 1px solid var(--line);
  color: var(--muted);
  font-size: 0.9rem;
}
footer .version-line { margin-bottom: 0.55rem; line-height: 1.7; }
footer .vknowl { color: inherit; text-decoration: none; border-bottom: 1px dashed var(--muted); cursor: pointer; }
footer .vknowl[aria-expanded="true"] { color: var(--ink); border-bottom-color: var(--accent); }
footer .vknowl-panel {
  display: block;
  margin: 0.55rem auto;
  max-width: 62rem;
  padding: 0.7rem 1.1rem;
  border: 1px solid var(--line);
  border-left: 4px solid var(--accent);
  border-radius: 6px;
  background: var(--card);
  text-align: left;
}
footer .vknowl-panel[hidden] { display: none; }
footer .vknowl-panel pre {
  margin: 0;
  padding: 0.55rem 0.8rem;
  overflow-x: auto;
  border: 1px solid var(--line);
  border-radius: 5px;
  background: var(--panel);
  font-size: 0.82rem;
}
footer code { padding: 0 0.3em; border: 1px solid var(--line); border-radius: 4px; background: var(--panel); }

@media (prefers-reduced-motion: reduce) {
  html { scroll-behavior: auto; }
  *, *::before, *::after { scroll-behavior: auto !important; transition-duration: 0.01ms !important; }
}

@media (max-width: 58rem) {
  .proof-route { grid-template-columns: 1fr; }
  .route-arrow { transform: rotate(90deg); justify-self: center; }
  .process-grid { grid-template-columns: minmax(0, 1fr); }
  .process-grid::before { display: none; }
}
@media (max-width: 46rem) {
  .resource-grid.grid-2col { grid-template-columns: minmax(0, 1fr); }
  .two-col { grid-template-columns: minmax(0, 1fr); }
  .paper-tools { position: static; grid-template-columns: minmax(0, 1fr); }
  .paper-tools output { padding: 0; }
  .node-head { display: block; }
  .status-badge { display: inline-block; margin-top: 0.55rem; }
}