/* Elements of Proof — styles
   Palette and type are defined as tokens; dark mode redefines the tokens. */

@font-face {
  font-family: 'EOP Mono';
  src: url('fonts/eop-mono-regular.woff2') format('woff2');
  font-weight: 400;
  font-style: normal;
  font-display: swap;
}
@font-face {
  font-family: 'EOP Mono';
  src: url('fonts/eop-mono-semibold.woff2') format('woff2');
  font-weight: 500 700;
  font-style: normal;
  font-display: swap;
}

:root {
  --paper: #fbfcfd;
  --paper-2: #f3f6f9;
  --panel: #eef2f6;
  --ink: #18202a;
  --ink-2: #4c5866;
  --ink-3: #7b8694;
  --rule: #dce2e9;
  --rule-2: #c7d0da;
  --accent: #27446e;
  --accent-2: #3a619a;
  --accent-bg: #e7eef8;
  --good: #1b7a4b;
  --good-bg: #e5f3ec;
  --bad: #b42318;
  --bad-bg: #fbeceb;
  --warn: #8a5a00;
  --warn-bg: #fbf1dc;
  --hl: #fbe39a;
  --hl-2: #c9e3fb;
  --focus: #3a619a;
  --shadow: 0 1px 2px rgba(24, 32, 42, 0.06), 0 4px 16px rgba(24, 32, 42, 0.06);

  --serif: 'STIX Two Text', 'STIX Two', 'Cambria', 'Georgia', serif;
  --sans: 'IBM Plex Sans', 'Segoe UI', 'Helvetica Neue', 'Arial', sans-serif;
  --mono: 'EOP Mono', 'JuliaMono', 'DejaVu Sans Mono', 'Menlo', 'Consolas', 'Segoe UI Symbol', monospace;

  --radius: 6px;
  --gutter: clamp(16px, 2.4vw, 28px);
  color-scheme: light;
}

@media (prefers-color-scheme: dark) {
  :root:not([data-theme='light']) {
    --paper: #0f1318;
    --paper-2: #141920;
    --panel: #181e26;
    --ink: #e4e8ee;
    --ink-2: #aab4c0;
    --ink-3: #7d8896;
    --rule: #262f3a;
    --rule-2: #334050;
    --accent: #93b7ea;
    --accent-2: #b5cdf1;
    --accent-bg: #1a2636;
    --good: #5cc08a;
    --good-bg: #13261c;
    --bad: #f08a7e;
    --bad-bg: #2c1716;
    --warn: #e7b458;
    --warn-bg: #2a2111;
    --hl: #5f4d12;
    --hl-2: #1d3a57;
    --focus: #93b7ea;
    --shadow: 0 1px 2px rgba(0, 0, 0, 0.3), 0 6px 20px rgba(0, 0, 0, 0.25);
    color-scheme: dark;
  }
}
:root[data-theme='dark'] {
  --paper: #0f1318;
  --paper-2: #141920;
  --panel: #181e26;
  --ink: #e4e8ee;
  --ink-2: #aab4c0;
  --ink-3: #7d8896;
  --rule: #262f3a;
  --rule-2: #334050;
  --accent: #93b7ea;
  --accent-2: #b5cdf1;
  --accent-bg: #1a2636;
  --good: #5cc08a;
  --good-bg: #13261c;
  --bad: #f08a7e;
  --bad-bg: #2c1716;
  --warn: #e7b458;
  --warn-bg: #2a2111;
  --hl: #5f4d12;
  --hl-2: #1d3a57;
  --focus: #93b7ea;
  --shadow: 0 1px 2px rgba(0, 0, 0, 0.3), 0 6px 20px rgba(0, 0, 0, 0.25);
  color-scheme: dark;
}

* { box-sizing: border-box; }
html, body { height: 100%; }
body {
  margin: 0;
  background: var(--paper);
  color: var(--ink);
  font-family: var(--serif);
  font-size: 17px;
  line-height: 1.55;
  -webkit-font-smoothing: antialiased;
}
button, input, textarea, select { font: inherit; color: inherit; }
a { color: var(--accent); text-underline-offset: 2px; }
a:hover { color: var(--accent-2); }
:focus-visible { outline: 2px solid var(--focus); outline-offset: 2px; }
[hidden] { display: none !important; }
code, pre, kbd, .mono { font-family: var(--mono); font-size: 0.86em; font-variant-ligatures: none; }
h1, h2, h3 { text-wrap: balance; font-weight: 600; line-height: 1.2; margin: 0; }
p { margin: 0; }
.visually-hidden { position: absolute; width: 1px; height: 1px; overflow: hidden; clip: rect(0 0 0 0); white-space: nowrap; }
@media (prefers-reduced-motion: reduce) {
  *, *::before, *::after { transition: none !important; animation: none !important; }
}

/* ------------------------------------------------------------ top bar */
.topbar {
  position: sticky;
  top: env(safe-area-inset-top, 0px);
  z-index: 20;
  display: flex;
  align-items: center;
  gap: 12px;
  padding-block: 10px;
  padding-inline: var(--gutter);
  background: color-mix(in srgb, var(--paper) 92%, transparent);
  backdrop-filter: blur(6px);
  border-bottom: 1px solid var(--rule);
  font-family: var(--sans);
  font-size: 14px;
}
.brand {
  font-family: var(--serif);
  font-size: 19px;
  font-weight: 600;
  color: var(--ink);
  text-decoration: none;
  white-space: nowrap;
  letter-spacing: 0.01em;
}
.brand .brand-mark {
  display: inline-block;
  width: 0.62em;
  height: 0.62em;
  margin-right: 0.45em;
  background: var(--accent);
  vertical-align: 0.02em;
}
.crumbs { display: flex; align-items: center; gap: 8px; min-width: 0; color: var(--ink-2); }
.crumbs .sep { color: var(--ink-3); }
.crumbs .crumb-title { white-space: nowrap; overflow: hidden; text-overflow: ellipsis; }
.topbar .spacer { flex: 1; }
.tb-btn {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  padding: 6px 10px;
  border: 1px solid var(--rule-2);
  background: var(--paper);
  border-radius: var(--radius);
  cursor: pointer;
  font-family: var(--sans);
  font-size: 13.5px;
  color: var(--ink);
  text-decoration: none;
  white-space: nowrap;
}
.tb-btn:hover { border-color: var(--accent-2); color: var(--accent); }
.tb-btn[disabled] { opacity: 0.45; cursor: default; pointer-events: none; }
.tb-btn.icon { padding: 6px 8px; }
.progress-pill {
  font-variant-numeric: tabular-nums;
  color: var(--ink-2);
  white-space: nowrap;
}

/* ------------------------------------------------------------ contents */
.contents {
  max-width: 1080px;
  margin: 0 auto;
  padding-inline: var(--gutter);
  padding-block: 40px 80px;
}
.hero {
  display: grid;
  grid-template-columns: minmax(0, 1.25fr) minmax(0, 1fr);
  gap: 48px;
  align-items: start;
  padding-bottom: 36px;
  border-bottom: 1px solid var(--rule);
}
.hero h1 { font-size: clamp(34px, 5vw, 52px); letter-spacing: -0.01em; font-weight: 600; }
.hero .subtitle { font-size: 21px; color: var(--ink-2); margin-top: 8px; font-style: italic; }
.hero .preface { margin-top: 22px; max-width: 62ch; display: grid; gap: 12px; }
.hero .actions { margin-top: 26px; display: flex; flex-wrap: wrap; gap: 12px; align-items: center; font-family: var(--sans); }
.btn {
  display: inline-flex;
  align-items: center;
  gap: 8px;
  padding: 9px 16px;
  border-radius: var(--radius);
  border: 1px solid var(--accent);
  background: var(--accent);
  color: var(--paper);
  font-family: var(--sans);
  font-size: 15px;
  font-weight: 500;
  text-decoration: none;
  cursor: pointer;
}
.btn:hover { background: var(--accent-2); border-color: var(--accent-2); color: var(--paper); }
.btn.secondary { background: transparent; color: var(--accent); }
.btn.secondary:hover { background: var(--accent-bg); color: var(--accent); }
.btn.small { padding: 6px 11px; font-size: 13.5px; }
.stat-line { font-family: var(--sans); font-size: 14px; color: var(--ink-2); font-variant-numeric: tabular-nums; }

.leitfaden-box { border: 1px solid var(--rule); border-radius: var(--radius); padding: 18px 18px 12px; background: var(--paper-2); }
.leitfaden-box .caption { font-family: var(--sans); font-size: 12px; letter-spacing: 0.08em; text-transform: uppercase; color: var(--ink-3); }
.leitfaden-box svg { display: block; width: 100%; height: auto; margin-top: 8px; }
.leitfaden-box .note { font-size: 14px; color: var(--ink-2); margin-top: 6px; }
.lf-node rect { fill: var(--paper); stroke: var(--rule-2); stroke-width: 1; }
.lf-node.done rect { stroke: var(--good); }
.lf-node text { fill: var(--ink); font-family: var(--serif); font-size: 14px; }
.lf-node text.num { fill: var(--accent); font-family: var(--sans); font-size: 11px; font-weight: 600; letter-spacing: 0.06em; }
.lf-node text.cnt { fill: var(--ink-3); font-family: var(--sans); font-size: 10.5px; }
.lf-edge { stroke: var(--ink-3); stroke-width: 1.2; fill: none; }
.lf-arrow { fill: var(--ink-3); }
.lf-node a { cursor: pointer; }
.lf-node a:hover rect { stroke: var(--accent); }

.how { display: grid; grid-template-columns: repeat(3, minmax(0, 1fr)); gap: 28px; padding-block: 30px; border-bottom: 1px solid var(--rule); }
.how h3 { font-size: 17px; font-family: var(--sans); font-weight: 600; margin-bottom: 6px; }
.how p { font-size: 15.5px; color: var(--ink-2); }
.how .n { font-family: var(--sans); font-size: 12px; color: var(--accent); font-weight: 600; letter-spacing: 0.08em; }

.toc { padding-top: 34px; display: grid; gap: 34px; }
.toc-chapter { display: grid; grid-template-columns: 64px minmax(0, 1fr); gap: 8px 18px; }
.toc-num { font-family: var(--serif); font-size: 40px; line-height: 1; color: var(--accent); font-variant-numeric: lining-nums; }
.toc-head h2 { font-size: 24px; }
.toc-head .blurb { color: var(--ink-2); font-style: italic; }
.toc-levels { grid-column: 2; list-style: none; margin: 8px 0 0; padding: 0; display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 0 28px; }
.toc-levels li { border-top: 1px dotted var(--rule-2); }
.toc-levels a {
  display: grid;
  grid-template-columns: 44px minmax(0, 1fr) auto;
  gap: 8px;
  align-items: baseline;
  padding: 7px 0;
  text-decoration: none;
  color: var(--ink);
}
.toc-levels a:hover .t { color: var(--accent); text-decoration: underline; }
.toc-levels .n { font-family: var(--sans); font-size: 13px; color: var(--ink-3); font-variant-numeric: tabular-nums; }
.toc-levels .t { min-width: 0; }
.toc-levels .boss-tag { font-family: var(--sans); font-size: 11px; letter-spacing: 0.06em; text-transform: uppercase; color: var(--ink-3); margin-left: 6px; }
.status { font-family: var(--sans); font-size: 12px; color: var(--ink-3); display: inline-flex; align-items: center; gap: 6px; white-space: nowrap; }
.status .par-ok { color: var(--good); }
.qed { display: inline-block; width: 0.62em; height: 0.62em; background: var(--good); vertical-align: -0.02em; }
.qed.open { background: transparent; border: 1.2px solid var(--ink-3); }
.qed.sorry { background: transparent; border: 1.2px dashed var(--warn); }

.about { margin-top: 48px; padding-top: 28px; border-top: 1px solid var(--rule); display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 36px; font-size: 15.5px; color: var(--ink-2); }
.about h3 { font-family: var(--sans); font-size: 13px; letter-spacing: 0.08em; text-transform: uppercase; color: var(--ink-3); margin-bottom: 8px; font-weight: 600; }
.about ul { margin: 0; padding-left: 18px; }
.about p + p { margin-top: 8px; }
.data-tools { display: flex; flex-wrap: wrap; gap: 8px; margin-top: 12px; font-family: var(--sans); }
.data-tools textarea { width: 100%; min-height: 90px; font-family: var(--mono); font-size: 12px; border: 1px solid var(--rule-2); border-radius: var(--radius); background: var(--paper); padding: 8px; }
.inline-confirm { display: inline-flex; gap: 8px; align-items: center; font-size: 13.5px; color: var(--bad); }

/* ------------------------------------------------------------ level layout */
.level {
  display: grid;
  grid-template-columns: minmax(0, 36fr) minmax(0, 44fr) minmax(250px, 22fr);
  gap: 0;
}
.app.level-mode { height: 100%; display: flex; flex-direction: column; }
.app.level-mode .level { flex: 1; min-height: 0; }
@media (min-width: 901px) {
  .app.level-mode .page, .app.level-mode .bench, .app.level-mode .library { overflow-y: auto; overscroll-behavior: contain; }
}
@media (max-width: 900px) {
  .app.level-mode { height: auto; display: block; }
}
.page, .bench, .library {
  padding-block: 24px 48px;
  padding-inline: var(--gutter);
  min-width: 0;
}
.bench { border-left: 1px solid var(--rule); border-right: 1px solid var(--rule); background: var(--paper-2); }
.library { background: var(--paper); }
.library-drawer-toggle { display: none; }
.library-close { display: none; }

@media (max-width: 1279px) {
  .level { grid-template-columns: minmax(0, 43fr) minmax(0, 57fr); }
  .bench { border-right: none; }
  .library {
    position: fixed;
    top: 0;
    right: 0;
    bottom: 0;
    width: min(380px, 92vw);
    z-index: 40;
    overflow-y: auto;
    border-left: 1px solid var(--rule);
    box-shadow: var(--shadow);
    padding-top: calc(20px + env(safe-area-inset-top, 0px));
    transform: translateX(105%);
    transition: transform 0.2s ease;
  }
  .library.open { transform: none; }
  .library-drawer-toggle { display: inline-flex; }
  .library-close { display: inline-flex; }
  .scrim { position: fixed; inset: 0; background: rgba(10, 14, 20, 0.28); z-index: 35; }
}
@media (max-width: 900px) {
  .level { grid-template-columns: minmax(0, 1fr); }
  .bench { border-left: none; border-top: 1px solid var(--rule); }
  .hero { grid-template-columns: minmax(0, 1fr); gap: 28px; }
  .how { grid-template-columns: minmax(0, 1fr); gap: 16px; }
  .toc-levels { grid-template-columns: minmax(0, 1fr); }
  .about { grid-template-columns: minmax(0, 1fr); }
  .crumbs .crumb-chapter { display: none; }
}
@media (max-width: 560px) {
  .toc-chapter { grid-template-columns: minmax(0, 1fr); }
  .toc-num { font-size: 30px; }
  .toc-levels { grid-column: 1; }
  .topbar { gap: 8px; }
  .tb-label { display: none; }
  .progress-pill { display: none; }
}

/* ------------------------------------------------------------ page (text) */
.page { max-width: 720px; }
.eyebrow { font-family: var(--sans); font-size: 12px; letter-spacing: 0.09em; text-transform: uppercase; color: var(--ink-3); }
.page h1 { font-size: 30px; margin-top: 6px; }
.theorem {
  margin-top: 18px;
  padding: 14px 16px;
  border-left: 3px solid var(--accent);
  background: var(--accent-bg);
  border-radius: 0 var(--radius) var(--radius) 0;
}
.theorem .label { font-weight: 600; }
.theorem .label .tname { font-weight: 400; font-style: italic; color: var(--ink-2); }
.theorem pre { margin: 8px 0 0; white-space: pre; overflow-x: auto; font-size: 14.5px; line-height: 1.5; color: var(--ink); }
.theorem pre.stmt-narrow { display: none; }
@media (max-width: 480px) {
  .theorem pre { font-size: 12.5px; }
  .theorem pre.stmt-wide { display: none; }
  .theorem pre.stmt-narrow { display: block; }
}
.prose { margin-top: 18px; display: grid; gap: 12px; }
.prose ul, .prose ol { margin: 0; padding-left: 22px; display: grid; gap: 4px; }
.prose code { background: var(--panel); padding: 1px 4px; border-radius: 3px; font-size: 0.84em; }
.prose pre.code { margin: 0; padding: 10px 12px; background: var(--panel); border-radius: var(--radius); overflow-x: auto; font-size: 14px; line-height: 1.5; }
.prose pre.code code { background: none; padding: 0; font-size: 1em; }
.prose table { border-collapse: collapse; font-size: 15px; width: 100%; }
.prose .table-wrap { overflow-x: auto; }
.prose th, .prose td { text-align: left; padding: 5px 10px; border-bottom: 1px solid var(--rule); }
.prose th { font-family: var(--sans); font-size: 12px; letter-spacing: 0.06em; text-transform: uppercase; color: var(--ink-3); font-weight: 600; }
.chip-row { display: flex; flex-wrap: wrap; gap: 8px; margin-top: 18px; align-items: center; font-family: var(--sans); font-size: 13px; color: var(--ink-2); }
.chip {
  font-family: var(--mono);
  font-size: 12.5px;
  padding: 2px 8px;
  border-radius: 999px;
  border: 1px solid var(--rule-2);
  background: var(--paper);
  color: var(--accent);
  cursor: pointer;
}
.chip:hover { border-color: var(--accent); }
.hints { margin-top: 22px; border-top: 1px solid var(--rule); padding-top: 14px; display: grid; gap: 10px; }
.hints .hint { font-size: 16px; padding-left: 12px; border-left: 2px solid var(--rule-2); }
.hints .hint .k { font-family: var(--sans); font-size: 11.5px; color: var(--ink-3); letter-spacing: 0.06em; text-transform: uppercase; display: block; }
.hint-actions { display: flex; flex-wrap: wrap; gap: 8px; align-items: center; font-family: var(--sans); }
.solution-box pre { margin: 6px 0 0; padding: 10px 12px; background: var(--panel); border-radius: var(--radius); overflow-x: auto; font-size: 14px; }
.solved-box {
  margin-top: 22px;
  padding: 16px;
  border: 1px solid var(--good);
  background: var(--good-bg);
  border-radius: var(--radius);
  display: grid;
  gap: 10px;
}
.solved-box .qed-line { font-family: var(--sans); font-size: 14px; display: flex; flex-wrap: wrap; gap: 10px; align-items: center; }
.solved-box .qed-line strong { font-weight: 600; color: var(--good); }
.solved-box .next-row { display: flex; gap: 10px; flex-wrap: wrap; }
.lean-export { margin-top: 22px; border: 1px solid var(--rule); border-radius: var(--radius); background: var(--paper); }
.lean-export summary { cursor: pointer; padding: 10px 14px; font-family: var(--sans); font-size: 14px; font-weight: 500; list-style: none; display: flex; justify-content: space-between; gap: 10px; }
.lean-export summary::-webkit-details-marker { display: none; }
.lean-export summary .note { color: var(--ink-3); font-weight: 400; }
.lean-export .body { padding: 0 14px 14px; display: grid; gap: 10px; }
.lean-export pre { margin: 0; max-height: 340px; overflow: auto; padding: 10px 12px; background: var(--panel); border-radius: var(--radius); font-size: 12.5px; line-height: 1.5; }
.lean-export .row { display: flex; flex-wrap: wrap; gap: 8px; align-items: center; font-family: var(--sans); font-size: 13px; color: var(--ink-2); }
.level-nav { display: flex; justify-content: space-between; gap: 10px; margin-top: 28px; font-family: var(--sans); font-size: 14px; }
.level-nav a { text-decoration: none; }

/* ------------------------------------------------------------ workbench */
.bench-head { display: flex; align-items: center; justify-content: space-between; gap: 10px; font-family: var(--sans); font-size: 14px; margin-bottom: 8px; }
.bench-head h2 { font-family: var(--sans); font-size: 13px; letter-spacing: 0.09em; text-transform: uppercase; color: var(--ink-3); font-weight: 600; }
.proof-status { display: inline-flex; align-items: center; gap: 7px; font-size: 13.5px; color: var(--ink-2); white-space: nowrap; }
.proof-status.good { color: var(--good); font-weight: 600; }
.proof-status.bad { color: var(--bad); }
.proof-status.warn { color: var(--warn); }
.bench-tools { display: flex; gap: 6px; }

.editor {
  position: relative;
  display: grid;
  grid-template-columns: auto minmax(0, 1fr);
  border: 1px solid var(--rule-2);
  border-radius: var(--radius);
  background: var(--paper);
  font-family: var(--mono);
  font-size: 14.5px;
  line-height: 1.6;
  overflow: hidden;
}
.editor:focus-within { border-color: var(--accent-2); box-shadow: 0 0 0 3px color-mix(in srgb, var(--accent-2) 18%, transparent); }
.gutter {
  padding: 10px 0;
  min-width: 44px;
  text-align: right;
  color: var(--ink-3);
  background: var(--paper-2);
  border-right: 1px solid var(--rule);
  user-select: none;
  font-size: 12px;
  font-variant-numeric: tabular-nums;
}
.gutter div { padding: 0 8px 0 6px; height: 1.6em; line-height: 1.6em; font-size: 12px; white-space: nowrap; position: relative; }
.gutter .mark { display: inline-block; width: 10px; margin-right: 4px; text-align: center; }
.gutter .err .mark { color: var(--bad); }
.gutter .err { color: var(--bad); }
.gutter .cur { color: var(--ink); }
.gutter .skip { opacity: 0.45; }
.code-area { position: relative; min-width: 0; overflow: hidden; }
.code-area pre, .code-area textarea {
  margin: 0;
  padding: 10px 12px;
  font: inherit;
  line-height: inherit;
  letter-spacing: 0;
  tab-size: 2;
  white-space: pre;
  word-wrap: normal;
  overflow-wrap: normal;
  border: 0;
}
.code-area pre {
  position: absolute;
  inset: 0;
  pointer-events: none;
  color: var(--ink);
  overflow: hidden;
}
.code-area textarea {
  position: relative;
  display: block;
  width: 100%;
  min-height: calc(1.6em * 7 + 20px);
  resize: none;
  background: transparent;
  color: transparent;
  caret-color: var(--ink);
  outline: none;
  overflow-x: auto;
  overflow-y: hidden;
}
.code-area textarea::selection { background: color-mix(in srgb, var(--accent-2) 30%, transparent); color: transparent; }
.code-area textarea::placeholder { color: var(--ink-3); }
.tok-tactic { color: var(--accent); font-weight: 600; }
.tok-kw { color: var(--accent); }
.tok-sym { color: var(--ink-2); }
.tok-num { color: #9a3b8a; }
.tok-comment { color: var(--ink-3); font-style: italic; }
.tok-hole { color: var(--warn); }
.tok-err { text-decoration: underline wavy var(--bad); text-decoration-skip-ink: none; text-underline-offset: 3px; }
.tok-warn { text-decoration: underline wavy var(--warn); text-underline-offset: 3px; }
.line-cur { background: color-mix(in srgb, var(--accent-bg) 70%, transparent); }
.line-skip { opacity: 0.5; }
.abbr-pending { text-decoration: underline; text-decoration-color: var(--accent-2); }

.symbar { display: flex; flex-wrap: wrap; gap: 4px; margin-top: 8px; }
.symbar button {
  min-width: 32px;
  padding: 3px 6px;
  border: 1px solid var(--rule);
  border-radius: 4px;
  background: var(--paper);
  font-family: var(--mono);
  font-size: 14px;
  cursor: pointer;
  color: var(--ink);
}
.symbar button:hover { border-color: var(--accent-2); color: var(--accent); }
.symbar .hint-text { font-family: var(--sans); font-size: 12px; color: var(--ink-3); align-self: center; margin-left: 4px; }

.tabs { display: flex; gap: 2px; margin-top: 18px; border-bottom: 1px solid var(--rule); font-family: var(--sans); font-size: 14px; }
.tabs button {
  border: 0;
  background: none;
  padding: 7px 12px;
  cursor: pointer;
  color: var(--ink-2);
  border-bottom: 2px solid transparent;
  margin-bottom: -1px;
}
.tabs button[aria-selected='true'] { color: var(--ink); border-bottom-color: var(--accent); font-weight: 500; }
.tab-panel { padding-top: 12px; }

/* goal view */
.goal-meta { font-family: var(--sans); font-size: 12.5px; color: var(--ink-3); margin-bottom: 8px; display: flex; gap: 8px; flex-wrap: wrap; justify-content: space-between; }
.goal-meta .where code { font-size: 12px; }
.goal {
  border: 1px solid var(--rule);
  background: var(--paper);
  border-radius: var(--radius);
  padding: 10px 12px;
  font-family: var(--mono);
  font-size: 14px;
  line-height: 1.55;
  overflow-x: auto;
}
.goal + .goal { margin-top: 8px; }
.goal.secondary { opacity: 0.78; }
.goal .case { font-family: var(--sans); font-size: 12px; color: var(--ink-3); margin-bottom: 2px; }
.goal .case b { font-family: var(--mono); font-weight: 500; color: var(--ink-2); }
.hyp { white-space: pre-wrap; word-break: break-word; }
.hyp .hname {
  border: 0;
  background: none;
  padding: 0;
  font: inherit;
  color: var(--accent);
  cursor: pointer;
  border-bottom: 1px dotted transparent;
}
.hyp .hname:hover { border-bottom-color: var(--accent); }
.hyp.obj .hname { color: var(--ink-2); }
.hyp.inst { color: var(--ink-3); }
.hyp.inst .hname { color: var(--ink-3); }
.hyp .rwable { cursor: help; }
.target { margin-top: 4px; padding-top: 4px; border-top: 1px dashed var(--rule-2); white-space: pre-wrap; word-break: break-word; }
.target .turn { color: var(--accent); font-weight: 600; margin-right: 0.4em; }
mark.hl, mark.hl-new { background: var(--hl); color: inherit; border-radius: 2px; padding: 0 1px; }
mark.hl-new { background: var(--hl-2); }
.no-goals {
  display: flex;
  align-items: center;
  gap: 10px;
  padding: 12px 14px;
  border: 1px solid var(--good);
  background: var(--good-bg);
  border-radius: var(--radius);
  font-family: var(--sans);
  font-size: 15px;
  color: var(--good);
  font-weight: 500;
}
.no-goals.plain { border-color: var(--rule); background: var(--paper); color: var(--ink-2); font-weight: 400; }
.message {
  margin-top: 10px;
  padding: 10px 12px;
  border-radius: var(--radius);
  font-family: var(--sans);
  font-size: 14px;
  line-height: 1.5;
  white-space: pre-wrap;
  word-break: break-word;
}
.message.error { background: var(--bad-bg); border: 1px solid color-mix(in srgb, var(--bad) 45%, transparent); }
.message.warning { background: var(--warn-bg); border: 1px solid color-mix(in srgb, var(--warn) 45%, transparent); }
.message.info { background: var(--accent-bg); border: 1px solid color-mix(in srgb, var(--accent) 30%, transparent); }
.message .mhead { font-weight: 600; font-size: 12.5px; letter-spacing: 0.04em; text-transform: uppercase; display: block; margin-bottom: 3px; }
.message.error .mhead { color: var(--bad); }
.message.warning .mhead { color: var(--warn); }
.message.info .mhead { color: var(--accent); }
.message code { font-size: 0.93em; background: color-mix(in srgb, var(--paper) 70%, transparent); padding: 0 3px; border-radius: 3px; }
.rw-note { margin-top: 10px; font-family: var(--sans); font-size: 13px; color: var(--ink-2); display: grid; gap: 6px; }
.rw-note .rw-line { font-family: var(--mono); font-size: 13.5px; color: var(--ink); background: var(--paper); border: 1px dashed var(--rule-2); border-radius: var(--radius); padding: 6px 10px; overflow-x: auto; white-space: pre-wrap; }
.guide { margin-top: 10px; font-size: 15.5px; color: var(--ink-2); padding-left: 12px; border-left: 2px solid var(--accent-2); }
.guide .k { font-family: var(--sans); font-size: 11.5px; letter-spacing: 0.06em; text-transform: uppercase; color: var(--ink-3); display: block; }

/* proof tree (Gentzen style) */
.tree-wrap { overflow-x: auto; padding: 8px 2px 14px; }
.tree-top { display: flex; align-items: flex-start; justify-content: space-between; gap: 12px; }
.tree-help { font-family: var(--sans); font-size: 12.5px; color: var(--ink-3); margin-bottom: 10px; }
.tree-root { display: inline-block; min-width: 100%; text-align: center; }
.inf { display: inline-grid; grid-template-columns: auto auto; align-items: end; vertical-align: bottom; margin: 0 6px; text-align: center; }
.inf-prem { grid-column: 1; grid-row: 1; display: flex; align-items: flex-end; justify-content: center; gap: 14px; }
.inf-line { grid-column: 1; grid-row: 2; border-top: 1.5px solid var(--ink); margin: 3px 0; min-width: 28px; }
.inf-lbl { grid-column: 2; grid-row: 2; align-self: center; justify-self: start; text-align: left; }
.inf-lbl button {
  border: 0;
  background: none;
  padding: 0 0 0 6px;
  font-family: var(--mono);
  font-size: 11.5px;
  color: var(--accent);
  white-space: nowrap;
  cursor: pointer;
}
.inf-lbl button:hover { text-decoration: underline; }
.inf-concl { grid-column: 1; grid-row: 3; font-family: var(--mono); font-size: 12.5px; padding: 0 4px; white-space: nowrap; }
.inf-concl .turn { color: var(--ink-3); margin-right: 3px; }
.inf.leaf { display: inline-block; }
.inf.open > .inf-concl { border: 1px dashed var(--ink-3); border-radius: 4px; padding: 1px 6px; color: var(--ink-2); }
.inf.error > .inf-concl { border: 1px solid var(--bad); color: var(--bad); border-radius: 4px; padding: 1px 6px; }
.inf.sorry > .inf-concl { border: 1px dashed var(--warn); color: var(--warn); border-radius: 4px; padding: 1px 6px; }
.inf-side { display: inline-flex; flex-direction: column; align-items: center; padding: 0 6px; border-left: 1px dotted var(--rule-2); }
.inf-side .side-lbl { font-family: var(--sans); font-size: 10.5px; color: var(--ink-3); letter-spacing: 0.05em; text-transform: uppercase; margin-bottom: 4px; }
.tree-legend { display: flex; flex-wrap: wrap; gap: 14px; margin-top: 10px; font-family: var(--sans); font-size: 12px; color: var(--ink-3); }

/* ------------------------------------------------------------ library */
.lib-head { display: flex; align-items: center; justify-content: space-between; gap: 8px; }
.lib-head h2 { font-family: var(--sans); font-size: 13px; letter-spacing: 0.09em; text-transform: uppercase; color: var(--ink-3); font-weight: 600; }
.lib-tabs { display: flex; gap: 2px; margin-top: 10px; border-bottom: 1px solid var(--rule); font-family: var(--sans); font-size: 13.5px; }
.lib-tabs button { border: 0; background: none; padding: 6px 9px; cursor: pointer; color: var(--ink-2); border-bottom: 2px solid transparent; margin-bottom: -1px; }
.lib-tabs button[aria-selected='true'] { color: var(--ink); border-bottom-color: var(--accent); font-weight: 500; }
.lib-list { margin-top: 10px; display: grid; gap: 8px; }
.lib-item { border: 1px solid var(--rule); border-radius: var(--radius); background: var(--paper); }
.lib-item > summary {
  cursor: pointer;
  list-style: none;
  padding: 8px 10px;
  display: flex;
  align-items: baseline;
  justify-content: space-between;
  gap: 8px;
}
.lib-item > summary::-webkit-details-marker { display: none; }
.lib-item .lname { font-family: var(--mono); font-size: 14px; font-weight: 600; color: var(--accent); }
.lib-item .new-tag { font-family: var(--sans); font-size: 10.5px; letter-spacing: 0.07em; text-transform: uppercase; color: var(--good); border: 1px solid currentColor; border-radius: 3px; padding: 0 4px; }
.lib-item .lsum { font-size: 14.5px; color: var(--ink-2); padding: 0 10px 8px; }
.lib-item .lbody { padding: 0 10px 10px; display: grid; gap: 10px; font-size: 14.5px; }
.lib-item .lbody .notes { color: var(--ink-2); }
.lib-item .usage { display: flex; flex-direction: column; gap: 4px; }
.lib-item .usage button { text-align: left; font-family: var(--mono); font-size: 12.5px; border: 1px solid var(--rule); background: var(--paper-2); border-radius: 4px; padding: 3px 7px; cursor: pointer; white-space: pre; overflow-x: auto; color: var(--ink); }
.lib-item .usage button:hover { border-color: var(--accent-2); }
.thm-stmt { font-family: var(--mono); font-size: 12.5px; padding: 0 10px 8px; color: var(--ink); white-space: pre-wrap; word-break: break-word; }
.thm-actions { display: flex; flex-wrap: wrap; gap: 6px; padding: 0 10px 10px; }
.thm-actions button { font-family: var(--mono); font-size: 12px; border: 1px solid var(--rule-2); background: var(--paper); border-radius: 4px; padding: 2px 7px; cursor: pointer; color: var(--accent); }
.thm-actions button:hover { border-color: var(--accent); }
.lib-empty { font-size: 14.5px; color: var(--ink-3); font-style: italic; }
.lib-group-title { font-family: var(--sans); font-size: 11.5px; letter-spacing: 0.08em; text-transform: uppercase; color: var(--ink-3); margin-top: 6px; }
.symtable { width: 100%; border-collapse: collapse; font-size: 14px; }
.symtable td { padding: 5px 6px; border-bottom: 1px solid var(--rule); vertical-align: top; }
.symtable td:first-child { font-family: var(--mono); font-size: 16px; width: 2.4em; text-align: center; }
.symtable code { font-size: 12.5px; color: var(--accent); }
.defs { display: grid; gap: 6px; font-size: 14px; margin-top: 12px; color: var(--ink-2); }
.defs code { color: var(--ink); }

/* natural-deduction rule */
.rule { display: inline-flex; flex-direction: column; align-items: center; font-family: var(--mono); font-size: 13px; padding: 6px 4px 2px; }
.rule-row { display: flex; align-items: flex-end; gap: 16px; justify-content: center; min-height: 1.4em; }
.rule-prem { text-align: center; white-space: nowrap; }
.rule-prem.disch { display: inline-flex; flex-direction: column; align-items: center; line-height: 1.25; }
.rule-prem.disch .assume { color: var(--ink-2); }
.rule-prem.disch .vdots { display: inline-flex; flex-direction: column; gap: 2px; margin: 2px 0; }
.rule-prem.disch .vdots i { width: 2.5px; height: 2.5px; border-radius: 50%; background: var(--ink-3); display: block; }
.rule-barline { position: relative; align-self: stretch; border-top: 1.4px solid var(--ink); margin: 4px 0; min-width: 60px; }
.rule-barline .rname { position: absolute; left: 100%; top: -0.72em; margin-left: 6px; font-family: var(--serif); font-size: 13px; color: var(--ink-2); white-space: nowrap; }
.rule-concl { white-space: nowrap; }
.rule-side { font-family: var(--sans); font-size: 12px; color: var(--ink-3); margin-top: 4px; }
.rule-side code { font-size: 12px; color: var(--ink-2); }
.rules { display: flex; flex-wrap: wrap; gap: 8px 22px; padding: 4px 34px 4px 0; overflow-x: auto; }

/* toast */
.toast {
  position: fixed;
  left: 50%;
  bottom: calc(24px + env(safe-area-inset-bottom, 0px));
  transform: translateX(-50%);
  background: var(--ink);
  color: var(--paper);
  font-family: var(--sans);
  font-size: 14px;
  padding: 8px 14px;
  border-radius: var(--radius);
  box-shadow: var(--shadow);
  z-index: 60;
}
.kbd { font-family: var(--mono); font-size: 12px; border: 1px solid var(--rule-2); border-bottom-width: 2px; border-radius: 4px; padding: 0 5px; background: var(--paper); }

/* ------------------------------------------------------------ progress, how to play */
.progress-card,
.how-card {
  border: 1px solid var(--rule);
  border-radius: var(--radius);
  padding: 18px 20px;
  background: var(--paper-2);
  font-family: var(--sans);
}
.progress-card .caption,
.how-card .caption { font-size: 12px; letter-spacing: 0.08em; text-transform: uppercase; color: var(--ink-3); }
.hero-figure { display: flex; flex-wrap: wrap; align-items: baseline; gap: 4px 10px; margin-top: 8px; }
.hero-figure .big { font-size: 56px; line-height: 1; font-weight: 600; color: var(--ink); }
.hero-figure .of { font-size: 15px; color: var(--ink-2); }
.kpis { display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 12px 18px; margin-top: 16px; padding-top: 14px; border-top: 1px solid var(--rule); }
.kpi { display: flex; flex-direction: column; gap: 2px; min-width: 0; }
.kpi .k-label { font-size: 12.5px; color: var(--ink-2); }
.kpi .k-value { font-size: 20px; font-weight: 600; color: var(--ink); }
.meters { list-style: none; margin: 16px 0 0; padding: 14px 0 0; border-top: 1px solid var(--rule); display: grid; gap: 4px; }
.meters a {
  display: grid;
  grid-template-columns: 1.2em minmax(0, 8.5em) minmax(40px, 1fr) 4.4em;
  align-items: center;
  gap: 10px;
  padding: 3px 0;
  color: var(--ink);
  text-decoration: none;
  font-size: 13px;
}
.meters a:hover .m-name { color: var(--accent); text-decoration: underline; }
.meters .m-num { color: var(--ink-3); font-variant-numeric: tabular-nums; text-align: right; }
.meters .m-name { white-space: nowrap; overflow: hidden; text-overflow: ellipsis; }
.meter { position: relative; height: 8px; border-radius: 4px; background: var(--accent-bg); overflow: hidden; }
.meter .fill { position: absolute; top: 0; bottom: 0; left: 0; background: var(--accent); border-radius: 4px; }
.meters .m-count { color: var(--ink-2); font-variant-numeric: tabular-nums; text-align: right; white-space: nowrap; }
.how-card { display: grid; gap: 14px; }
.how-step .n { font-size: 12px; color: var(--accent); font-weight: 600; letter-spacing: 0.08em; text-transform: uppercase; }
.how-step h3 { font-size: 16px; font-weight: 600; margin: 2px 0 4px; }
.how-step p { font-family: var(--serif); font-size: 15px; color: var(--ink-2); }

/* the Leitfaden, full width under the hero */
section.leitfaden-box { margin-top: 32px; }
.lf-scroll { overflow-x: auto; }
.lf-scroll svg { min-width: 640px; max-width: 824px; }

/* ------------------------------------------------------------ sandbox */
.sandbox-callout {
  margin-top: 48px;
  padding: 20px 22px;
  border: 1px solid var(--rule);
  border-radius: var(--radius);
  background: var(--paper-2);
  display: flex;
  flex-wrap: wrap;
  gap: 16px 28px;
  align-items: center;
  justify-content: space-between;
}
.sandbox-callout h2 { font-size: 22px; }
.sandbox-callout p { color: var(--ink-2); max-width: 60ch; margin-top: 4px; }
.sb-libs { display: flex; flex-wrap: wrap; gap: 6px; margin-top: 18px; font-family: var(--sans); }
.sb-libs .seg { border: 1px solid var(--rule-2); border-radius: 999px; background: var(--paper); padding: 5px 12px; font-size: 13.5px; cursor: pointer; color: var(--ink-2); }
.sb-libs .seg:hover { border-color: var(--accent); color: var(--accent); }
.sb-libs .seg.on { background: var(--accent); border-color: var(--accent); color: var(--paper); }
.sb-examples .chip { font-family: var(--sans); font-size: 13px; }
.sb-statement .label { display: block; margin-bottom: 8px; }
#sig-error .message { margin-top: 10px; }
.editor.compact { grid-template-columns: minmax(0, 1fr); }
.editor.compact .gutter { display: none; }
.editor.compact .code-area textarea { min-height: calc(1.6em * 2 + 20px); }

/* a proof opened from a shared link */
.shared-banner {
  display: flex;
  flex-wrap: wrap;
  gap: 8px 14px;
  align-items: center;
  justify-content: space-between;
  margin-bottom: 10px;
  padding: 8px 12px;
  border: 1px solid var(--rule-2);
  border-left: 3px solid var(--accent);
  border-radius: var(--radius);
  background: var(--accent-bg);
  font-family: var(--sans);
  font-size: 13.5px;
  color: var(--ink);
}
.shared-banner .sb-actions { display: flex; gap: 6px; }