:root {
  --bg: #0e1116;
  --fg: #d8dee9;
  --muted: #6a737d;
  --proven: #2ea043;
  --informal: #58a6ff;
  --conjecture: #d29922;
  --open: #f85149;
  --refuted: #8b949e;
  --border: #21262d;
  --card: #161b22;
}

* { box-sizing: border-box; }
html, body {
  margin: 0;
  padding: 0;
  background: var(--bg);
  color: var(--fg);
  font: 15px/1.6 -apple-system, BlinkMacSystemFont, "Segoe UI", Inter, system-ui, sans-serif;
}

body { max-width: 980px; margin: 0 auto; padding: 24px 20px 80px; }

header { border-bottom: 1px solid var(--border); padding-bottom: 18px; margin-bottom: 24px; }
header h1 { margin: 0 0 6px; font-size: 28px; letter-spacing: -0.01em; }
header .sub { color: var(--muted); margin: 0 0 12px; font-size: 14px; }
header .stmt {
  background: var(--card); border: 1px solid var(--border);
  padding: 12px 14px; border-radius: 6px; font-size: 14px; line-height: 1.55;
  margin: 0;
}

.legend {
  display: flex; flex-wrap: wrap; gap: 8px;
  margin-bottom: 28px;
  font-size: 12px;
}
.chip {
  padding: 3px 10px; border-radius: 999px; border: 1px solid var(--border);
  font-weight: 500;
}
.chip.proven { color: var(--proven); border-color: var(--proven); }
.chip.informal { color: var(--informal); border-color: var(--informal); }
.chip.conjecture { color: var(--conjecture); border-color: var(--conjecture); }
.chip.open { color: var(--open); border-color: var(--open); }
.chip.refuted { color: var(--refuted); border-color: var(--refuted); }

section { margin-bottom: 36px; }
h2 {
  margin: 0 0 14px; font-size: 18px;
  border-bottom: 1px solid var(--border); padding-bottom: 6px;
}
h3 { margin: 18px 0 6px; font-size: 15px; }

.node {
  border: 1px solid var(--border);
  background: var(--card);
  border-left-width: 3px;
  padding: 10px 14px;
  border-radius: 4px;
  margin: 8px 0;
}
.node .title { font-weight: 600; margin-bottom: 4px; }
.node .meta, .node .body { font-size: 13px; color: var(--muted); }
.node.proven { border-left-color: var(--proven); }
.node.informal { border-left-color: var(--informal); }
.node.conjecture { border-left-color: var(--conjecture); }
.node.open { border-left-color: var(--open); }
.node.refuted { border-left-color: var(--refuted); }

.route {
  background: var(--card);
  border: 1px solid var(--border);
  border-radius: 6px;
  padding: 14px 16px;
  margin-bottom: 16px;
}
.route p { margin: 6px 0 10px; font-size: 13px; color: var(--muted); }
.route ul.children { list-style: none; padding-left: 0; margin: 0; }
.route ul.children li.node { font-size: 13px; padding: 6px 12px; border-radius: 3px; margin: 4px 0; }
.route ul.children li.node.proven::before { content: "✓ "; color: var(--proven); }
.route ul.children li.node.open::before { content: "✗ "; color: var(--open); }
.route ul.children li.node.refuted::before { content: "⊘ "; color: var(--refuted); }
.route ul.children li.node.conjecture::before { content: "≈ "; color: var(--conjecture); }
.route ul.children li.node.informal::before { content: "ⓘ "; color: var(--informal); }

ul { line-height: 1.7; }
ul strong { color: #fff; }
table { width: 100%; border-collapse: collapse; font-size: 13px; }
th, td { text-align: left; padding: 8px 10px; border-bottom: 1px solid var(--border); }
th { color: var(--muted); font-weight: 500; }
code { background: #1c2128; padding: 1px 6px; border-radius: 3px; font-size: 12px; }
em { color: #c9d1d9; font-style: normal; font-weight: 500; }

#footer { color: var(--muted); font-size: 12px; border-top: 1px solid var(--border); padding-top: 16px; }
#footer p { margin: 4px 0; }

/* explainer */
details.explainer {
  margin-top: 14px;
  border: 1px solid var(--border);
  background: var(--card);
  border-radius: 6px;
  padding: 8px 14px;
}
details.explainer > summary {
  cursor: pointer;
  font-weight: 600;
  font-size: 14px;
  padding: 4px 0;
  list-style: none;
}
details.explainer > summary::-webkit-details-marker { display: none; }
details.explainer > summary::before {
  content: "▸ ";
  color: var(--muted);
  display: inline-block;
  width: 1em;
  transition: transform 0.15s;
}
details.explainer[open] > summary::before {
  content: "▾ ";
}
.explainer-body { padding: 6px 0 10px; font-size: 14px; }
.explainer-body p { margin: 8px 0; }
.explainer-body em { color: #e6edf3; }

/* svg figure */
figure {
  margin: 14px 0;
  padding: 12px;
  background: #0a0d12;
  border: 1px solid var(--border);
  border-radius: 6px;
}
figure svg { display: block; width: 100%; height: auto; max-width: 100%; }
figcaption { color: var(--muted); font-size: 12px; margin-top: 8px; text-align: center; }

/* svg tree styles */
.vtx { fill: #1f6feb; stroke: #58a6ff; stroke-width: 1.5; }
.vlabel { fill: #fff; font-size: 12px; font-family: ui-monospace, monospace; text-anchor: middle; dominant-baseline: middle; }
.edge { stroke: #8b949e; stroke-width: 2; }
.caption { fill: var(--fg); font-size: 13px; font-weight: 600; }
.meta-text { fill: var(--muted); font-size: 11px; }

/* svg bar chart */
.axis { stroke: #30363d; stroke-width: 1; }
.bar { fill: #2ea043; opacity: 0.85; }
.bar.peak { fill: #d29922; }
.klabel { fill: var(--muted); font-size: 11px; text-anchor: middle; font-family: ui-monospace, monospace; }
.vval { fill: #fff; font-size: 12px; font-weight: 600; text-anchor: middle; }

/* KaTeX tweaks */
.katex { font-size: 1.02em; }
.stmt .katex { font-size: 0.98em; }