:root {
  color-scheme: light;
  --ink: #102a43;
  --muted: #526b80;
  --paper: #f5fbff;
  --surface: #ffffff;
  --surface-soft: #eaf6ff;
  --line: #cfe4f6;
  --accent: #2f9fe8;
  --accent-dark: #0967a8;
  --accent-soft: #daf2ff;
  --navy: #0b3a5d;
  --violet: #6658d3;
  --violet-soft: #f0edff;
  --shadow: 0 22px 60px rgba(19, 105, 166, 0.12);
  font-family: Inter, ui-sans-serif, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
}

* { box-sizing: border-box; }
html { scroll-behavior: smooth; }
body {
  margin: 0;
  color: var(--ink);
  background:
    radial-gradient(circle at 8% 30%, rgba(95, 190, 247, 0.12), transparent 24rem),
    linear-gradient(rgba(9, 103, 168, 0.026) 1px, transparent 1px),
    var(--paper);
  background-size: auto, 100% 40px, auto;
  line-height: 1.62;
}

a { color: inherit; }
.skip-link {
  position: fixed;
  z-index: 100;
  top: 12px;
  left: 18px;
  padding: 9px 13px;
  color: white;
  background: var(--navy);
  border-radius: 8px;
  transform: translateY(-160%);
}
.skip-link:focus { transform: none; }

.masthead {
  position: relative;
  overflow: hidden;
  color: white;
  background:
    radial-gradient(circle at 16% 8%, rgba(166, 225, 255, 0.5), transparent 25rem),
    radial-gradient(circle at 87% 76%, rgba(80, 202, 240, 0.3), transparent 24rem),
    linear-gradient(135deg, #075b9a 0%, #117fbe 58%, #249bd1 100%);
}
.masthead::before {
  position: absolute;
  inset: 0;
  content: "";
  opacity: 0.18;
  background-image:
    linear-gradient(rgba(255, 255, 255, 0.34) 1px, transparent 1px),
    linear-gradient(90deg, rgba(255, 255, 255, 0.34) 1px, transparent 1px);
  background-size: 52px 52px;
  mask-image: linear-gradient(to bottom, black, transparent 92%);
}
.masthead::after {
  position: absolute;
  right: -11rem;
  bottom: -17rem;
  width: 33rem;
  height: 33rem;
  content: "";
  border: 1px solid rgba(255, 255, 255, 0.2);
  border-radius: 50%;
  box-shadow:
    0 0 0 4rem rgba(255, 255, 255, 0.04),
    0 0 0 9rem rgba(255, 255, 255, 0.035);
}

.topline,
.hero,
main,
footer {
  width: min(1180px, calc(100% - 40px));
  margin-inline: auto;
}
.topline {
  position: relative;
  z-index: 1;
  min-height: 68px;
  display: flex;
  align-items: center;
  border-bottom: 1px solid rgba(255, 255, 255, 0.2);
}
.wordmark {
  display: inline-flex;
  align-items: center;
  gap: 11px;
  color: white;
  font-size: 1rem;
  font-weight: 780;
  letter-spacing: -0.02em;
  text-decoration: none;
}
.mark {
  width: 34px;
  height: 34px;
  display: grid;
  grid-template-columns: repeat(2, 5px);
  place-content: center;
  gap: 5px;
  border: 1px solid rgba(255, 255, 255, 0.55);
  border-radius: 10px;
  background: rgba(255, 255, 255, 0.12);
}
.mark i {
  width: 5px;
  height: 5px;
  display: block;
  border-radius: 50%;
  background: white;
}

.hero {
  position: relative;
  z-index: 1;
  max-width: 990px;
  padding: clamp(64px, 8vw, 105px) 0 64px;
  text-align: center;
}
.eyebrow,
.result-label {
  margin: 0 0 10px;
  color: var(--accent-dark);
  font-size: 0.73rem;
  font-weight: 820;
  letter-spacing: 0.14em;
  text-transform: uppercase;
}
.hero > .eyebrow { color: rgba(255, 255, 255, 0.82); }
h1, h2 {
  margin-top: 0;
  font-family: Georgia, "Times New Roman", serif;
  font-weight: 500;
  letter-spacing: -0.04em;
}
h1 {
  max-width: 900px;
  margin: 0 auto 22px;
  font-size: clamp(3.2rem, 7.5vw, 6.35rem);
  line-height: 0.98;
  text-wrap: balance;
}
h2 {
  margin-bottom: 0;
  font-size: clamp(2rem, 4vw, 3.25rem);
  line-height: 1.06;
}
h3 { margin-top: 0; letter-spacing: -0.02em; line-height: 1.25; }
p { margin-top: 0; }
.lede {
  max-width: 760px;
  margin: 0 auto 34px;
  color: rgba(255, 255, 255, 0.92);
  font-size: clamp(1.05rem, 2vw, 1.28rem);
}

.resource-tabs {
  display: grid;
  grid-template-columns: repeat(4, 1fr);
  gap: 10px;
  margin: 0 auto;
}
.resource-tabs a {
  min-height: 64px;
  display: flex;
  flex-direction: column;
  align-items: center;
  justify-content: center;
  padding: 10px 14px;
  border: 1px solid rgba(255, 255, 255, 0.5);
  border-radius: 12px;
  color: white;
  background: rgba(5, 64, 105, 0.22);
  box-shadow: 0 10px 28px rgba(1, 43, 77, 0.09);
  font-size: 0.93rem;
  font-weight: 780;
  line-height: 1.25;
  text-decoration: none;
  backdrop-filter: blur(8px);
  transition: transform 150ms ease, background 150ms ease, border-color 150ms ease;
}
.resource-tabs a span {
  color: rgba(255, 255, 255, 0.8);
  font-size: 0.65rem;
  font-weight: 700;
  letter-spacing: 0.08em;
  text-transform: uppercase;
}
.resource-tabs a:hover,
.resource-tabs a:focus-visible {
  transform: translateY(-3px);
  border-color: rgba(255, 255, 255, 0.82);
  background: rgba(5, 64, 105, 0.32);
}
.status-line {
  display: flex;
  flex-wrap: wrap;
  justify-content: center;
  gap: 8px 20px;
  margin-top: 25px;
  color: rgba(255, 255, 255, 0.84);
  font-size: 0.74rem;
}
.status-line strong {
  display: inline-flex;
  align-items: center;
  gap: 8px;
  color: white;
}
.status-line strong > span {
  width: 7px;
  height: 7px;
  border-radius: 50%;
  background: #a7f3d0;
  box-shadow: 0 0 0 4px rgba(167, 243, 208, 0.16);
}

main { padding-block: 78px 76px; }
section { scroll-margin-top: 24px; }
.wide-actions { display: flex; flex-wrap: wrap; gap: 11px; }
.button {
  min-height: 46px;
  display: inline-flex;
  align-items: center;
  justify-content: center;
  padding: 0 19px;
  border: 1px solid var(--accent-dark);
  border-radius: 999px;
  font-size: 0.86rem;
  font-weight: 770;
  text-decoration: none;
  transition: transform 150ms ease, box-shadow 150ms ease, background 150ms ease;
}
.button:hover,
.button:focus-visible { transform: translateY(-2px); box-shadow: 0 10px 24px rgba(9, 103, 168, 0.17); }
.button.primary { color: white; background: var(--accent-dark); }
.button.secondary { color: var(--accent-dark); background: rgba(255, 255, 255, 0.74); }

.theorem-section,
.results-section { margin-top: 112px; }
.section-intro {
  display: grid;
  grid-template-columns: minmax(0, 1.15fr) minmax(260px, 0.74fr);
  gap: 42px;
  align-items: end;
  margin-bottom: 34px;
}
.section-intro > p { margin-bottom: 2px; color: var(--muted); }
.proof-rail {
  display: grid;
  grid-template-columns: 1fr auto 1fr auto 1fr auto 1fr auto 1fr;
  gap: 9px;
  align-items: stretch;
}
.proof-node {
  min-width: 0;
  display: flex;
  flex-direction: column;
  padding: 19px 16px;
  border: 1px solid var(--line);
  border-top: 4px solid var(--accent);
  border-radius: 13px;
  background: var(--surface);
  box-shadow: 0 8px 28px rgba(19, 105, 166, 0.05);
  text-decoration: none;
  transition: transform 150ms ease, border-color 150ms ease, box-shadow 150ms ease;
}
.proof-node:hover,
.proof-node:focus-visible { transform: translateY(-4px); border-color: #8cc8ed; box-shadow: var(--shadow); }
.proof-node.final-node { color: white; border-color: var(--navy); background: linear-gradient(145deg, var(--accent-dark), var(--navy)); }
.node-id {
  min-height: 34px;
  color: #c46f13;
  font-family: ui-monospace, SFMono-Regular, Menlo, monospace;
  font-size: 0.68rem;
  font-weight: 800;
}
.final-node .node-id { color: #a9e7ff; }
.proof-node strong { margin-bottom: 9px; font-size: 0.98rem; line-height: 1.25; }
.proof-node small { margin-top: auto; color: var(--muted); font-size: 0.75rem; line-height: 1.4; }
.final-node small { color: rgba(255, 255, 255, 0.72); }
.proof-arrow { display: grid; place-items: center; color: var(--accent); font-size: 1.15rem; }
.external-input {
  display: grid;
  grid-template-columns: auto 1fr auto;
  gap: 13px;
  align-items: center;
  margin-top: 17px;
  padding: 14px 18px;
  border: 1px dashed #a9a0e7;
  border-radius: 12px;
  background: var(--violet-soft);
}
.external-input p { margin: 0; color: #4e4b70; font-size: 0.87rem; }
.external-input a { color: #5144b6; font-size: 0.78rem; font-weight: 780; text-decoration: none; }
.external-mark {
  width: 24px;
  height: 24px;
  display: grid;
  place-items: center;
  color: white;
  border-radius: 50%;
  background: var(--violet);
  font-weight: 800;
}
.wide-actions { margin-top: 24px; }

.theorem-section {
  padding: clamp(28px, 5vw, 50px);
  border: 1px solid var(--line);
  border-top: 5px solid var(--accent);
  border-radius: 0 0 18px 18px;
  background: linear-gradient(145deg, #edf8ff, #f9fcff);
  box-shadow: 0 18px 48px rgba(19, 105, 166, 0.07);
}
.theorem-heading {
  display: grid;
  grid-template-columns: minmax(0, 0.9fr) minmax(300px, 1.15fr);
  gap: 44px;
  align-items: center;
}
.theorem-heading code {
  overflow-wrap: anywhere;
  padding: 17px 19px;
  color: var(--accent-dark);
  border: 1px solid var(--line);
  border-radius: 10px;
  background: rgba(255, 255, 255, 0.78);
  font-family: ui-monospace, SFMono-Regular, Menlo, monospace;
  font-size: 0.88rem;
}
.theorem-copy { max-width: 850px; margin: 32px 0; color: var(--muted); font-size: 1.02rem; }
.theorem-links { display: grid; grid-template-columns: repeat(4, 1fr); gap: 10px; }
.theorem-links a {
  min-width: 0;
  display: flex;
  flex-direction: column;
  padding: 14px;
  border: 1px solid var(--line);
  border-radius: 10px;
  background: rgba(255, 255, 255, 0.8);
  text-decoration: none;
}
.theorem-links a:hover,
.theorem-links a:focus-visible { border-color: var(--accent); }
.theorem-links span { color: var(--muted); font-size: 0.68rem; }
.theorem-links strong { overflow-wrap: anywhere; margin-top: 4px; color: var(--accent-dark); font-size: 0.8rem; }

.results-list {
  overflow: hidden;
  border: 1px solid var(--line);
  border-radius: 14px;
  background: var(--surface);
}
.result-row {
  display: grid;
  grid-template-columns: minmax(230px, 0.9fr) minmax(280px, 1.25fr) auto;
  gap: 26px;
  align-items: center;
  padding: 21px 23px;
  border-top: 1px solid var(--line);
}
.result-row:first-child { border-top: 0; }
.result-row.result-main { box-shadow: inset 4px 0 0 var(--accent); }
.result-row.result-external { box-shadow: inset 4px 0 0 var(--violet); background: #fcfbff; }
.result-label { display: block; margin-bottom: 4px; font-size: 0.66rem; }
.result-external .result-label { color: var(--violet); }
.result-row h3 { margin-bottom: 0; font-size: 1.02rem; }
.result-row p { margin-bottom: 0; color: var(--muted); font-size: 0.85rem; }
.result-links { display: flex; gap: 15px; }
.result-links a,
.index-link {
  color: var(--accent-dark);
  font-size: 0.78rem;
  font-weight: 780;
  text-decoration: none;
}
.result-links a:hover,
.result-links a:focus-visible,
.index-link:hover,
.index-link:focus-visible { text-decoration: underline; }
.index-link { display: inline-block; margin-top: 19px; }

.provenance {
  display: grid;
  grid-template-columns: 0.8fr 1.2fr;
  gap: 60px;
  margin-top: 104px;
  padding: 34px 0;
  border-top: 1px solid var(--line);
  border-bottom: 1px solid var(--line);
}
.provenance p { margin-bottom: 8px; color: var(--muted); font-size: 0.9rem; }
.provenance a { color: var(--accent-dark); text-underline-offset: 3px; }

footer {
  min-height: 96px;
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 24px;
  color: var(--muted);
  font-size: 0.8rem;
}
footer p { margin: 0; }
footer a { color: var(--accent-dark); font-weight: 760; text-decoration: none; }
footer a:hover,
footer a:focus-visible { text-decoration: underline; }

@media (max-width: 1020px) {
  .proof-rail { grid-template-columns: 1fr; gap: 8px; }
  .proof-arrow { height: 22px; transform: rotate(90deg); }
  .proof-node { min-height: 110px; }
  .node-id { min-height: 0; margin-bottom: 13px; }
  .theorem-links { grid-template-columns: repeat(2, 1fr); }
  .result-row { grid-template-columns: minmax(220px, 0.9fr) minmax(240px, 1.1fr) auto; gap: 18px; }
}

@media (max-width: 760px) {
  .topline, .hero, main, footer { width: min(100% - 28px, 1180px); }
  .topline { min-height: 62px; }
  .hero { padding: 58px 0 52px; }
  h1 { font-size: clamp(2.8rem, 13.5vw, 4.8rem); }
  .resource-tabs { grid-template-columns: repeat(2, 1fr); max-width: 540px; }
  .status-line { gap: 7px 14px; }
  main { padding-block: 64px 58px; }
  .theorem-section, .results-section { margin-top: 84px; }
  .section-intro, .theorem-heading, .provenance { grid-template-columns: 1fr; gap: 22px; }
  .external-input { grid-template-columns: auto 1fr; }
  .external-input a { grid-column: 2; }
  .result-row { grid-template-columns: 1fr; gap: 10px; }
  .result-links { margin-top: 2px; }
  footer { min-height: 112px; flex-direction: column; align-items: flex-start; justify-content: center; gap: 5px; }
}

@media (max-width: 490px) {
  .hero { padding-top: 48px; }
  .resource-tabs { gap: 8px; }
  .resource-tabs a { min-height: 61px; padding-inline: 8px; font-size: 0.86rem; }
  .status-line > span { display: none; }
  .wide-actions { align-items: stretch; flex-direction: column; }
  .button { width: 100%; }
  .theorem-section { padding: 25px 18px; }
  .theorem-links { grid-template-columns: 1fr; }
  .result-row { padding: 19px 18px; }
}

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