:root {
  --bg: #f7f7f5;
  --panel: #ffffff;
  --ink: #1d1f23;
  --muted: #6b7079;
  --line: #e3e3df;
  --accent: #3b5bdb;
  --accent-soft: #e7ecff;
  --yes: #2b8a3e;
  --yes-soft: #e3f4e6;
  --no: #c92a2a;
  --no-soft: #fdeaea;
  --open: #b7791f;
  --open-soft: #fdf3e1;
  --na: #c4c6cb;
  --node: #ffffff;
  --node-line: #c9ccd3;
  --shadow: 0 1px 2px rgba(0,0,0,.05), 0 4px 16px rgba(0,0,0,.05);
  --radius: 10px;
  color-scheme: light;
}
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    --bg: #15171b; --panel: #1d2026; --ink: #e8e9ec; --muted: #9aa0aa; --line: #30343c;
    --accent: #8ea4ff; --accent-soft: #263055;
    --yes: #69db7c; --yes-soft: #1d3324; --no: #ff8787; --no-soft: #3a2224;
    --open: #ffc078; --open-soft: #3a2f1d; --na: #4a4e57;
    --node: #23272e; --node-line: #3e434d; color-scheme: dark;
  }
}
:root[data-theme="dark"] {
  --bg: #15171b; --panel: #1d2026; --ink: #e8e9ec; --muted: #9aa0aa; --line: #30343c;
  --accent: #8ea4ff; --accent-soft: #263055;
  --yes: #69db7c; --yes-soft: #1d3324; --no: #ff8787; --no-soft: #3a2224;
  --open: #ffc078; --open-soft: #3a2f1d; --na: #4a4e57;
  --node: #23272e; --node-line: #3e434d; color-scheme: dark;
}

* { box-sizing: border-box; }
[hidden] { display: none !important; }
html, body { margin: 0; }
body {
  background: var(--bg); color: var(--ink);
  font: 15px/1.55 Inter, system-ui, -apple-system, sans-serif;
  min-height: 100vh;
}
a { color: var(--accent); text-decoration: none; }
a:hover { text-decoration: underline; }
h1, h2, h3 { line-height: 1.25; margin: 0 0 .5em; }
h1 { font-size: 1.7rem; }
h2 { font-size: 1.15rem; margin-top: 1.6em; }
h3 { font-size: 1rem; }
.muted { color: var(--muted); }
.small { font-size: .85rem; }
code { font-size: .9em; background: var(--accent-soft); padding: 0 .3em; border-radius: 4px; }
.katex { font-size: 1.05em; }

/* ---- top bar ------------------------------------------------------------ */
.topbar {
  position: sticky; top: 0; z-index: 30;
  display: flex; align-items: center; gap: 24px;
  padding: 10px 24px; background: var(--panel); border-bottom: 1px solid var(--line);
}
.brand { font-weight: 700; font-size: 1.15rem; color: var(--ink); letter-spacing: -.01em; }
.brand span { color: var(--accent); margin-left: 2px; }
.brand:hover { text-decoration: none; }
nav { display: flex; gap: 4px; flex-wrap: wrap; }
nav a { color: var(--muted); padding: 6px 10px; border-radius: 6px; font-weight: 500; }
nav a:hover { background: var(--bg); text-decoration: none; color: var(--ink); }
nav a.active { color: var(--accent); background: var(--accent-soft); }
.search { position: relative; margin-left: auto; width: min(340px, 40vw); }
.search input, input.text, select {
  width: 100%; padding: 7px 11px; border: 1px solid var(--line); border-radius: 8px;
  background: var(--bg); color: var(--ink); font: inherit;
}
.search input:focus, input.text:focus { outline: 2px solid var(--accent-soft); border-color: var(--accent); }
.popover {
  position: absolute; top: calc(100% + 4px); left: 0; right: 0; z-index: 40;
  background: var(--panel); border: 1px solid var(--line); border-radius: 10px; box-shadow: var(--shadow);
  max-height: 60vh; overflow: auto; padding: 4px;
}
.popover .opt { display: flex; gap: 10px; align-items: baseline; padding: 6px 10px; border-radius: 6px; cursor: pointer; }
.popover .opt.hl, .popover .opt:hover { background: var(--accent-soft); }
.popover .opt .muted { font-size: .85rem; }

main { padding: 24px; max-width: 1280px; margin: 0 auto; padding-bottom: 120px; }
main.wide { max-width: none; }
.loading { color: var(--muted); }

/* ---- generic ------------------------------------------------------------ */
.btn {
  display: inline-flex; align-items: center; gap: 6px; cursor: pointer;
  border: 1px solid var(--line); background: var(--panel); color: var(--ink);
  border-radius: 8px; padding: 5px 11px; font: inherit; font-size: .88rem; font-weight: 500;
}
.btn:hover { border-color: var(--accent); color: var(--accent); text-decoration: none; }
.btn.primary { background: var(--accent); color: #fff; border-color: var(--accent); }
.btn.primary:hover { filter: brightness(1.08); color: #fff; }
.btn.on { background: var(--accent-soft); color: var(--accent); border-color: var(--accent); }
.btn.small { padding: 2px 8px; font-size: .8rem; }
.chip {
  display: inline-flex; align-items: center; gap: 4px; padding: 1px 9px; border-radius: 999px;
  font-size: .78rem; background: var(--bg); border: 1px solid var(--line); color: var(--muted); cursor: pointer;
  white-space: nowrap;
}
.chip.on { background: var(--accent-soft); color: var(--accent); border-color: var(--accent); }
.chip .count { opacity: .7; }
.card {
  background: var(--panel); border: 1px solid var(--line); border-radius: var(--radius); padding: 16px 18px;
}
.row { display: flex; gap: 10px; align-items: center; flex-wrap: wrap; }
.grow { flex: 1; }
.badge { font-size: .72rem; padding: 1px 7px; border-radius: 999px; font-weight: 600; }
.badge.warn { background: var(--open-soft); color: var(--open); }
.badge.ai { background: #f3e8ff; color: #7c3aed; }
@media (prefers-color-scheme: dark) { :root:not([data-theme="light"]) .badge.ai { background: #2e2245; color: #c4a5ff; } }
.badge.folk { background: var(--bg); color: var(--muted); border: 1px solid var(--line); }
.yes { color: var(--yes); } .no { color: var(--no); } .open { color: var(--open); } .na { color: var(--na); }
table.grid { border-collapse: collapse; width: 100%; font-size: .9rem; }
table.grid th, table.grid td { border-bottom: 1px solid var(--line); padding: 7px 10px; text-align: left; vertical-align: top; }
table.grid th { font-size: .78rem; text-transform: uppercase; letter-spacing: .04em; color: var(--muted); font-weight: 600; }
table.grid td.c, table.grid th.c { text-align: center; }
table.grid th.c { text-transform: none; }

/* ---- catalogue ---------------------------------------------------------- */
.cat-layout { display: grid; grid-template-columns: 220px 1fr; gap: 28px; }
.facets h3 { font-size: .78rem; text-transform: uppercase; letter-spacing: .05em; color: var(--muted); margin-top: 1.2em; }
.facets .chips { display: flex; flex-wrap: wrap; gap: 6px; }
.cat-list { display: grid; gap: 12px; }
.stmt-card { display: grid; grid-template-columns: 150px 1fr auto; gap: 18px; align-items: start; }
.stmt-card .label { font-size: 1.3rem; padding-top: 2px; }
.stmt-card .name { font-weight: 600; }
.stmt-card .def { color: var(--ink); margin: 4px 0 6px; font-size: .92rem; }
.stmt-card .forms { font-size: .85rem; color: var(--muted); }
.stmt-card .forms a { margin-right: 8px; }
.stmt-card .tags { display: flex; gap: 5px; flex-wrap: wrap; margin-top: 6px; }
.sel-toggle.on { background: var(--accent); color: #fff; border-color: var(--accent); }

/* ---- statement page ----------------------------------------------------- */
.stmt-head { display: flex; gap: 20px; align-items: baseline; flex-wrap: wrap; }
.stmt-head .label { font-size: 2.1rem; }
.def-box { font-size: 1.02rem; }
.io { display: grid; grid-template-columns: 1fr 1fr; gap: 12px; margin-top: 12px; }
.io .card { padding: 10px 14px; }
.io h3 { font-size: .75rem; text-transform: uppercase; letter-spacing: .05em; color: var(--muted); margin: 0 0 4px; }
.two-col { display: grid; grid-template-columns: 1fr 1fr; gap: 20px; }
.rel-cols { display: grid; grid-template-columns: repeat(auto-fill, minmax(230px, 1fr)); gap: 14px; }
.rel-cols .card h3 { font-size: .85rem; }
.rel-list { display: flex; flex-wrap: wrap; gap: 6px; }
.rel-list .chip { font-size: .85rem; color: var(--ink); }
.reflist li { margin-bottom: 6px; }
.role { font-size: .72rem; text-transform: uppercase; letter-spacing: .04em; color: var(--muted); margin-right: 6px; }

/* ---- reduction picker / lattice ---------------------------------------- */
.lattice text { font: 600 11px Inter, sans-serif; fill: var(--ink); pointer-events: none; }
.lattice .edge { stroke: var(--node-line); stroke-width: 1.2; fill: none; }
.lattice .node rect { fill: var(--panel); stroke: var(--node-line); stroke-width: 1.2; rx: 6; }
.lattice .node.pick { cursor: pointer; }
.lattice .node.pick:hover rect { stroke: var(--accent); }
.lattice .node.sel rect { fill: var(--accent); stroke: var(--accent); }
.lattice .node.sel text { fill: #fff; }
.lattice .node.st-implies rect { fill: var(--yes-soft); stroke: var(--yes); }
.lattice .node.st-separated rect { fill: var(--no-soft); stroke: var(--no); }
.lattice .node.st-open rect { fill: var(--open-soft); stroke: var(--open); stroke-dasharray: 3 2; }
.lattice .node.st-na rect { fill: var(--bg); stroke: var(--line); }
.lattice .node.st-na text { fill: var(--na); }
.lattice .node.st-contradiction rect { fill: #000; }

/* ---- diagram ------------------------------------------------------------ */
.diagram-page { display: grid; grid-template-columns: 300px 1fr; gap: 0; height: calc(100vh - 57px); }
.diagram-side { border-right: 1px solid var(--line); background: var(--panel); padding: 16px; overflow: auto; }
.diagram-side h3 { font-size: .75rem; text-transform: uppercase; letter-spacing: .05em; color: var(--muted); margin: 18px 0 8px; }
.diagram-side h3:first-child { margin-top: 0; }
.sel-list { display: flex; flex-direction: column; gap: 4px; }
.sel-item { display: flex; align-items: center; gap: 8px; padding: 3px 6px; border-radius: 6px; }
.sel-item:hover { background: var(--bg); }
.sel-item .x { margin-left: auto; cursor: pointer; color: var(--muted); border: 0; background: none; font-size: 1rem; }
.sel-item .x:hover { color: var(--no); }
.toggle { display: flex; align-items: center; gap: 8px; font-size: .9rem; cursor: pointer; margin-bottom: 6px; }
.legend { display: grid; gap: 6px; font-size: .85rem; }
.legend svg { vertical-align: middle; }
.viewport { position: relative; overflow: hidden; background:
  radial-gradient(circle, var(--line) 1px, transparent 1px) 0 0 / 22px 22px, var(--bg); cursor: grab; }
.viewport.dragging { cursor: grabbing; }
.viewport .stage { position: absolute; left: 0; top: 0; transform-origin: 0 0; }
.viewport svg.edges { position: absolute; left: 0; top: 0; overflow: visible; }
.dnode {
  position: absolute; transform: translate(-50%, -50%);
  background: var(--node); border: 1.5px solid var(--node-line); border-radius: 9px;
  padding: 6px 12px; white-space: nowrap; text-align: center; cursor: pointer;
  box-shadow: 0 1px 2px rgba(0,0,0,.06); transition: opacity .12s, border-color .12s, box-shadow .12s;
  user-select: none;
}
.dnode .eq { display: block; font-size: .78em; color: var(--muted); }
.dnode.base { border-style: dashed; }
.dnode:hover, .dnode.focus { border-color: var(--accent); box-shadow: 0 0 0 3px var(--accent-soft); }
.dnode.above { border-color: var(--accent); }
.dnode.below { border-color: var(--yes); }
.dim .dnode:not(.focus):not(.above):not(.below) { opacity: .28; }
.dim path.imp:not(.hl) { opacity: .15; }
.dim path.sepa:not(.hl), .dim path.opn:not(.hl) { opacity: .12; }
path.imp { stroke: var(--ink); stroke-width: 1.6; fill: none; opacity: .75; cursor: pointer; }
path.imp.hl { stroke: var(--accent); opacity: 1; stroke-width: 2.2; }
path.sepa { stroke: var(--no); stroke-width: 1.4; fill: none; stroke-dasharray: 6 4; cursor: pointer; }
path.opn { stroke: var(--open); stroke-width: 1.4; fill: none; stroke-dasharray: 2 4; cursor: pointer; }
path.hit { stroke: transparent; stroke-width: 12; fill: none; cursor: pointer; }
.zoombar { position: absolute; right: 14px; bottom: 14px; display: flex; gap: 6px; z-index: 5; }
.empty-hint { position: absolute; inset: 0; display: grid; place-items: center; color: var(--muted); text-align: center; padding: 40px; }

/* ---- compare ------------------------------------------------------------ */
.matrix { border-collapse: separate; border-spacing: 3px; }
.matrix th { font-weight: 500; padding: 4px 8px; white-space: nowrap; }
.matrix th.col { vertical-align: bottom; }
.matrix td { padding: 0; }
.matrix td .cell { display: block; border-radius: 6px; padding: 2px; cursor: pointer; border: 1px solid transparent; }
.matrix td .cell:hover { border-color: var(--accent); }
.matrix td.diag { background: var(--bg); border-radius: 6px; }
.pmatrix td.c { font-size: 1.05rem; cursor: pointer; }
.pmatrix td.c:hover { background: var(--accent-soft); }

/* ---- drawer (proofs, pair details) ------------------------------------- */
.drawer {
  position: fixed; top: 57px; right: 0; bottom: 0; width: min(560px, 100vw); z-index: 25;
  background: var(--panel); border-left: 1px solid var(--line); box-shadow: -8px 0 24px rgba(0,0,0,.08);
  overflow: auto; padding: 20px 22px;
}
.drawer .close { position: absolute; right: 14px; top: 12px; }
.proof { list-style: none; padding-left: 0; margin: 0; }
.proof ul { list-style: none; padding-left: 18px; border-left: 1px solid var(--line); margin: 4px 0 4px 6px; }
.proof li { margin: 4px 0; }
.proof .fact { font-weight: 500; }
.proof .rule { font-size: .75rem; color: var(--muted); margin-left: 6px; }
.proof .cite { font-size: .85rem; margin-top: 2px; }
.proof .note { font-size: .82rem; color: var(--muted); }
.proof summary { cursor: pointer; }
.verdict { font-size: 1.05rem; padding: 10px 14px; border-radius: 8px; margin: 10px 0; }
.verdict.implies { background: var(--yes-soft); }
.verdict.separated { background: var(--no-soft); }
.verdict.open { background: var(--open-soft); }
.verdict.na { background: var(--bg); }

/* ---- selection tray ----------------------------------------------------- */
.tray {
  position: fixed; left: 50%; transform: translateX(-50%); bottom: 16px; z-index: 20;
  display: flex; align-items: center; gap: 10px; padding: 8px 10px 8px 16px;
  background: var(--panel); border: 1px solid var(--line); border-radius: 999px; box-shadow: var(--shadow);
  max-width: calc(100vw - 32px);
}
.tray > .small { white-space: nowrap; }
.tray .items { display: flex; gap: 6px; overflow-x: auto; max-width: 52vw; }
.tray .chip { color: var(--ink); font-size: .85rem; }

/* ---- results & refs ----------------------------------------------------- */
.filters { display: flex; gap: 10px; flex-wrap: wrap; margin-bottom: 14px; }
.filters > * { width: auto; }
.res-stmt { white-space: nowrap; }
.ref-entry { margin-bottom: 14px; }
.ref-entry .title { font-weight: 600; }
.stats { display: grid; grid-template-columns: repeat(auto-fill, minmax(150px, 1fr)); gap: 12px; margin: 16px 0; }
.stats .card { text-align: center; }
.stats .num { font-size: 1.6rem; font-weight: 700; }

@media (max-width: 860px) {
  .topbar { flex-wrap: wrap; gap: 8px; padding: 8px 16px; }
  .search { width: 100%; }
  main { padding: 16px; }
  .cat-layout, .two-col, .io { grid-template-columns: 1fr; }
  .stmt-card { grid-template-columns: 1fr; gap: 6px; }
  .diagram-page { grid-template-columns: 1fr; height: auto; }
  .viewport { height: 70vh; order: -1; }
  .drawer { top: 0; }
}

/* ---- expandable lists ------------------------------------------------------ */
.lazy-items { display: grid; gap: 12px; }
.more-bar { display: flex; align-items: center; gap: 10px; margin-top: 10px; flex-wrap: wrap; }
.more-bar:empty { display: none; }
.rel-cols .more-bar { margin-top: 6px; }

.badge.read-pdf-zotero, .badge.read-pdf-arxiv, .badge.read-pdf-oa { background: var(--yes-soft); color: var(--yes); }
.badge.read-abstract { background: var(--open-soft); color: var(--open); }
.badge.read-screened, .badge.read-none { background: var(--bg); color: var(--muted); border: 1px solid var(--line); }