: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); }

/* node-level details */
.route .node details > summary {
  cursor: pointer;
  list-style: none;
  display: inline;
}
.route .node details > summary::-webkit-details-marker { display: none; }
.route .node details > summary::after {
  content: " ▸";
  color: var(--muted);
  font-size: 10px;
}
.route .node details[open] > summary::after {
  content: " ▾";
}
.node-detail {
  margin-top: 8px;
  padding: 8px 12px;
  border-left: 2px solid var(--proven);
  background: rgba(46, 160, 67, 0.04);
  border-radius: 3px;
  font-size: 12.5px;
  line-height: 1.65;
  color: var(--fg);
}
.node-detail p { margin: 6px 0; }
.node-detail ul { margin: 6px 0 6px 8px; padding-left: 14px; }
.node-detail li { margin: 2px 0; }
.node-detail h4 { margin: 12px 0 4px; font-size: 13px; color: #fff; }
.node-detail strong { color: #fff; }
.node.open .node-detail { border-left-color: var(--open); background: rgba(248, 81, 73, 0.04); }
.node.refuted .node-detail { border-left-color: var(--refuted); background: rgba(139, 148, 158, 0.04); }
.node.conjecture .node-detail { border-left-color: var(--conjecture); background: rgba(210, 153, 34, 0.04); }
.node.informal .node-detail { border-left-color: var(--informal); background: rgba(88, 166, 255, 0.04); }

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 p.meta-note { color: var(--muted); font-size: 13px; padding-left: 10px; border-left: 2px solid var(--border); margin-left: 2px; }
.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; }

/* numbering badges */
.numid {
  display: inline-block;
  font-family: ui-monospace, monospace;
  font-size: 11px;
  font-weight: 700;
  background: rgba(255,255,255,0.06);
  color: var(--fg);
  padding: 1px 6px;
  border-radius: 3px;
  margin-right: 6px;
  letter-spacing: 0.02em;
  border: 1px solid var(--border);
}
.node.proven .numid { color: var(--proven); border-color: var(--proven); }
.node.open .numid { color: var(--open); border-color: var(--open); }
.node.refuted .numid { color: var(--refuted); border-color: var(--refuted); }
.node.conjecture .numid { color: var(--conjecture); border-color: var(--conjecture); }
.node.informal .numid { color: var(--informal); border-color: var(--informal); }

ul.numbered-list { list-style: none; padding-left: 0; }
ul.numbered-list > li { margin: 6px 0; padding: 4px 0; }
ul.numbered-list .numid { color: var(--fg); }

/* numbering key */
details.numbering-key {
  margin-bottom: 18px;
  font-size: 13px;
  border: 1px dashed var(--border);
  border-radius: 5px;
  padding: 6px 12px;
  background: rgba(255,255,255,0.02);
}
details.numbering-key > summary {
  cursor: pointer;
  font-weight: 500;
  color: var(--muted);
  list-style: none;
}
details.numbering-key > summary::-webkit-details-marker { display: none; }
details.numbering-key > summary::before { content: "▸ "; color: var(--muted); }
details.numbering-key[open] > summary::before { content: "▾ "; }

/* anchor highlight */
.flash {
  animation: flash 2s ease-out;
}
@keyframes flash {
  0% { background: rgba(88,166,255,0.25); box-shadow: 0 0 0 2px rgba(88,166,255,0.5); }
  100% { background: transparent; box-shadow: none; }
}

/* node hover affords clicking link icon */
.node[id] { position: relative; }
.node[id]:hover::after {
  content: "#" attr(id);
  position: absolute;
  right: 8px;
  top: 8px;
  font-size: 10px;
  font-family: ui-monospace, monospace;
  color: var(--muted);
  opacity: 0.7;
}

.badge-new {
  background: var(--informal);
  color: #fff;
  font-size: 10px;
  padding: 1px 6px;
  border-radius: 3px;
  margin-left: 6px;
  font-weight: 600;
  vertical-align: middle;
}
.badge-proven {
  background: var(--proven);
  color: #fff;
  font-size: 10px;
  padding: 1px 6px;
  border-radius: 3px;
  margin-left: 6px;
  font-weight: 600;
  vertical-align: middle;
}

/* session timeline */
details.session-timeline {
  margin-bottom: 18px;
  font-size: 13px;
  border: 1px solid var(--informal);
  background: rgba(88, 166, 255, 0.04);
  border-radius: 6px;
  padding: 8px 14px;
}
details.session-timeline > summary {
  cursor: pointer;
  font-weight: 600;
  color: var(--informal);
  list-style: none;
}
details.session-timeline > summary::-webkit-details-marker { display: none; }
ol.timeline {
  margin: 8px 0;
  padding-left: 20px;
}
ol.timeline > li { margin: 4px 0; line-height: 1.6; }

/* newly proven highlight */
.newly-proven {
  background: rgba(46, 160, 67, 0.06);
  padding: 6px 10px;
  border-left: 3px solid var(--proven);
  border-radius: 3px;
}

/* ---- #1107 additions ---- */
.lead { font-size: 16px; line-height: 1.75; }
.lead strong { color: #fff; }
.explainer { border: 1px solid var(--border); background: var(--card); border-radius: 6px;
  padding: 10px 14px; margin: 14px 0; }
.explainer summary { cursor: pointer; font-weight: 600; color: var(--informal); font-size: 14px; }
.explainer-body { font-size: 14px; line-height: 1.7; padding-top: 8px; }
table.d { border-collapse: collapse; width: 100%; font-size: 13px; margin: 12px 0; }
table.d th, table.d td { border: 1px solid var(--border); padding: 6px 9px; text-align: left; }
table.d th { background: var(--card); font-weight: 600; }
table.d td.num { text-align: right; font-variant-numeric: tabular-nums; }
table.d tr.hi td { background: rgba(248,81,73,.08); }
.numline { font-family: ui-monospace, SFMono-Regular, Menlo, monospace; font-size: 13px;
  background: var(--card); border: 1px solid var(--border); border-radius: 5px;
  padding: 9px 12px; overflow-x: auto; color: #9ecbff; }
.callout { border-left: 3px solid var(--conjecture); background: var(--card);
  padding: 10px 14px; border-radius: 4px; margin: 14px 0; font-size: 14px; }
.callout.bad { border-left-color: var(--open); }
.callout.good { border-left-color: var(--proven); }
.tag { display: inline-block; font-size: 11px; padding: 1px 7px; border-radius: 999px;
  border: 1px solid var(--border); margin-left: 6px; vertical-align: middle; }
.tag.thm { color: var(--proven); border-color: var(--proven); }
.tag.num { color: var(--informal); border-color: var(--informal); }
.tag.open { color: var(--open); border-color: var(--open); }
.tag.rec { color: var(--conjecture); border-color: var(--conjecture); }
footer { border-top: 1px solid var(--border); margin-top: 40px; padding-top: 16px;
  font-size: 12px; color: var(--muted); }
.toc { font-size: 13px; columns: 2; column-gap: 28px; }
.toc a { color: var(--informal); text-decoration: none; display: block; padding: 2px 0; }
.toc a:hover { text-decoration: underline; }

/* ---- 交互实验 ---- */
.lab { border:1px solid var(--border); background:var(--card); border-radius:8px; padding:16px; margin:16px 0; }
.lab .row { display:flex; flex-wrap:wrap; gap:10px; align-items:center; margin-bottom:12px; }
.lab label { font-size:13px; color:var(--muted); }
.lab select, .lab input[type=number] {
  background:#0e1116; color:var(--fg); border:1px solid var(--border);
  border-radius:5px; padding:6px 9px; font:inherit; font-size:14px; }
.lab input[type=number] { width:130px; }
.lab button { background:var(--informal); color:#04121f; border:0; border-radius:5px;
  padding:7px 16px; font:inherit; font-size:14px; font-weight:600; cursor:pointer; }
.lab button:hover { filter:brightness(1.12); }
.lab .presets { font-size:12px; color:var(--muted); }
.lab .presets a { color:var(--informal); text-decoration:none; margin-right:10px; cursor:pointer; }
.lab .presets a:hover { text-decoration:underline; }
.out { font-size:14px; line-height:1.7; }
.out .good { color:var(--proven); margin-bottom:6px; }
.out .bad { color:var(--open); margin-bottom:6px; }
.out .hint { color:var(--muted); font-size:12.5px; margin:8px 0; }
.out .ok { color:var(--proven); } .out .no { color:var(--open); }
.reps { display:flex; flex-wrap:wrap; gap:7px; margin-top:10px; }
.rep { border:1px solid var(--border); border-radius:5px; padding:5px 9px;
  font-family:ui-monospace,SFMono-Regular,Menlo,monospace; font-size:12.5px; background:#0e1116; }
.rep.allpure { border-color:var(--proven); background:rgba(46,160,67,.10); }
.rep i { color:var(--muted); font-style:normal; }
.term { color:#9ecbff; }
.term.pure { color:var(--proven); font-weight:600; }
.term .fx { color:var(--muted); font-size:11px; }
.term .fx { color:var(--muted); font-size:10.5px; margin-left:2px; }
.rep i { margin:0 4px; }