/* ────────────────────────────────────────── ENTITY SURFACES
   Theorem (th__), Proof (pf__), Procedure (pr__), Comparative (cmp__).
   Plus the peek primitive (peek__) — drawer / hover-card / inline,
   selectable via tweak. */

/* ─── Peek primitive ─── */
.peek-host { position: relative; }

/* The cite link — every entity reference uses this */
.cite {
  font-family: var(--font-mono);
  color: var(--accent);
  border-bottom: 1px dotted var(--accent);
  cursor: pointer;
  text-decoration: none;
  padding-bottom: 1px;
  transition: background 80ms ease;
}
.cite:hover { background: color-mix(in oklab, var(--accent) 10%, transparent); }

/* DRAWER — slides from right edge of artboard */
.peek--drawer .peek-card {
  position: absolute; top: 0; right: 0; bottom: 0;
  width: 420px; background: var(--paper);
  border-left: 2px solid var(--ink); padding: 28px 32px;
  box-shadow: -8px 0 24px rgba(0,0,0,0.04);
  z-index: 50; overflow-y: auto;
}

/* HOVER-CARD — anchored popover */
.peek--popover .peek-card {
  position: absolute; top: 100%; left: 0;
  width: 420px; background: var(--paper);
  border: 1px solid var(--ink); padding: 18px 22px;
  box-shadow: 0 6px 20px rgba(0,0,0,0.08);
  z-index: 50; margin-top: 6px;
}

/* INLINE — expands in place below the citation */
.peek--inline .peek-card {
  display: block; width: 100%;
  margin: 12px 0; padding: 18px 22px;
  background: var(--paper-2); border-left: 3px solid var(--accent);
  border-top: 1px solid var(--rule-3);
  border-bottom: 1px solid var(--rule-3);
}

.peek-head {
  display: flex; align-items: baseline; gap: 12px;
  padding-bottom: 8px; border-bottom: 1px solid var(--rule-3);
  margin-bottom: 12px;
}
.peek-id { color: var(--ink-4); font-size: 11px; margin-left: auto; }
.peek-close {
  background: none; border: 1px solid var(--rule-2);
  font-family: var(--font-mono); font-size: 11px;
  padding: 3px 8px; cursor: pointer; color: var(--ink-3);
}
.peek-statement {
  font-family: var(--font-text); font-size: 15px; line-height: 1.55;
  color: var(--ink); margin: 8px 0 14px;
}
.peek-foot { display: flex; gap: 8px; padding-top: 10px; border-top: 1px solid var(--rule-3); }


/* ─── THEOREM PAGE (th__) ─── */
.th { background: var(--paper); color: var(--ink); font-family: var(--font-ui); }
.th__top {
  display: flex; justify-content: space-between; align-items: center;
  padding: 16px 48px; min-height: 56px;
}
.th__top-l, .th__top-r { display: flex; align-items: center; gap: 10px; }

.th__hero {
  display: grid; grid-template-columns: 1fr 340px;
  gap: 56px; padding: 40px 48px 32px;
}
.th__title-block { display: flex; flex-direction: column; gap: 12px; }
.th__kicker {
  display: flex; align-items: center; gap: 14px;
  font: 500 11px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
}
.th__kicker--accent { color: var(--accent); }
.th__title {
  font-family: var(--font-ui);
  font-weight: 500; font-size: 56px; line-height: 1.05;
  letter-spacing: -0.01em;
  margin: 0;
}
.th__statement {
  font-family: var(--font-text);
  font-size: 26px; line-height: 1.4; color: var(--ink);
  padding: 22px 0; border-top: 1px solid var(--ink); border-bottom: 1px solid var(--rule);
  margin-top: 12px;
}
.th__statement em { font-style: italic; color: var(--ink-2); }

.th__hyp-row {
  display: grid; grid-template-columns: 1fr 1fr; gap: 24px;
  padding: 24px 0; border-bottom: 1px solid var(--rule-3);
}
.th__hyp { display: flex; flex-direction: column; gap: 6px; }
.th__hyp-label {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
}
.th__hyp-body {
  font-family: var(--font-text); font-size: 16px; line-height: 1.55;
}

.th__rail { display: flex; flex-direction: column; gap: 22px; }
.th__qref {
  border: 1px solid var(--rule); background: var(--paper-2);
  padding: 16px;
}
.th__qref-row {
  display: flex; justify-content: space-between; padding: 5px 0;
  font-size: 12px; border-bottom: 1px solid var(--rule-3);
}
.th__qref-row:last-child { border: 0; }

.th__sect { padding: 36px 48px 28px; }
.th__sect-head {
  display: flex; align-items: baseline; gap: 14px; margin-bottom: 14px;
}
.th__sect-id { margin-left: auto; color: var(--ink-4); }

/* Proof teaser block */
.th__proof-teaser {
  border: 1px solid var(--rule); padding: 22px 26px;
  background: var(--paper-2);
}
.th__proof-teaser-head {
  display: flex; justify-content: space-between; align-items: baseline;
  padding-bottom: 12px; border-bottom: 1px solid var(--rule-3);
  margin-bottom: 16px;
}
.th__proof-step {
  display: grid; grid-template-columns: 32px 1fr 200px;
  gap: 16px; align-items: baseline; padding: 8px 0;
}
.th__proof-n { font-family: var(--font-mono); color: var(--accent); font-weight: 600; }
.th__proof-stmt { font-family: var(--font-text); font-size: 15px; line-height: 1.55; }
.th__proof-just { font-size: 11px; color: var(--ink-4); font-family: var(--font-mono); }
.th__proof-fade {
  text-align: center; padding: 14px 0 6px;
  border-top: 1px solid var(--rule-3); margin-top: 12px;
  color: var(--ink-4); font-size: 11px; letter-spacing: 0.1em;
  text-transform: uppercase; font-family: var(--font-mono);
}
.th__proof-expand {
  width: 100%; text-align: center; padding: 14px;
  background: var(--ink); color: var(--paper); border: 0;
  font: 500 11px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; cursor: pointer; margin-top: 8px;
}

/* Variants table */
.th__variants {
  border-top: 1px solid var(--ink); border-bottom: 1px solid var(--rule);
}
.th__var-grid {
  display: grid;
  grid-template-columns: 1.4fr 2fr 1.2fr 1fr;
  align-items: baseline;
}
.th__var-h {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
  padding: 10px 12px; border-bottom: 1px solid var(--rule-2);
}
.th__var-cell {
  padding: 14px 12px; border-bottom: 1px solid var(--rule-3);
  font-size: 13px; line-height: 1.45;
}
.th__var-name { font-weight: 500; }
.th__var-id { font-family: var(--font-mono); color: var(--ink-4); font-size: 11px; }
.th__var-formula { font-family: var(--font-text); font-size: 16px; }
.th__var-domain { color: var(--ink-3); }

/* Uses / used-by lists */
.th__uses {
  display: grid; grid-template-columns: 1fr 1fr; gap: 32px;
}
.th__uses-col {
  display: flex; flex-direction: column;
}
.th__uses-h {
  font: 500 11px/1 var(--font-mono); letter-spacing: 0.08em;
  text-transform: uppercase; color: var(--ink-4);
  padding-bottom: 8px; border-bottom: 1px solid var(--ink); margin-bottom: 0;
}
.th__use-item {
  display: grid; grid-template-columns: auto 1fr auto;
  gap: 12px; align-items: center;
  padding: 10px 0; border-bottom: 1px solid var(--rule-3);
  font-size: 13px;
}
.th__use-shape { width: 12px; height: 12px; }
.th__use-name { font-weight: 500; }
.th__use-id { color: var(--ink-4); font-family: var(--font-mono); font-size: 11px; }


/* ─── PROOF PAGE (pf__) ─── */
.pf { background: var(--paper); color: var(--ink); font-family: var(--font-ui); position: relative; }
.pf__top {
  display: flex; justify-content: space-between; align-items: center;
  padding: 16px 48px; min-height: 56px;
}

.pf__hero {
  padding: 36px 48px 28px;
  display: flex; flex-direction: column; gap: 14px;
}
.pf__target-label {
  font: 500 11px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
}
.pf__target {
  font-family: var(--font-text); font-size: 24px; line-height: 1.4;
  color: var(--ink); padding: 14px 0;
  border-top: 1px solid var(--ink); border-bottom: 1px solid var(--rule);
}
.pf__meta-row { display: flex; gap: 24px; font-size: 12px; color: var(--ink-3); }

.pf__viewseg {
  display: inline-flex; border: 1px solid var(--rule); margin-left: auto;
}
.pf__viewseg-btn {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.08em;
  text-transform: uppercase; padding: 8px 14px;
  border: 0; border-right: 1px solid var(--rule);
  background: var(--paper); color: var(--ink-3); cursor: pointer;
}
.pf__viewseg-btn:last-child { border-right: 0; }
.pf__viewseg-btn.is-on { background: var(--ink); color: var(--paper); }

/* Sequential view */
.pf__seq {
  padding: 20px 48px 36px;
  display: flex; flex-direction: column;
  border-top: 1px solid var(--rule);
}
.pf__step {
  display: grid; grid-template-columns: 50px 1fr 280px;
  gap: 24px; padding: 22px 0;
  border-bottom: 1px solid var(--rule-3);
  align-items: start;
}
.pf__step:last-child { border-bottom: 0; }
.pf__step--current { background: color-mix(in oklab, var(--accent) 4%, transparent); }
.pf__step-n {
  font-family: var(--font-mono); font-size: 22px; font-weight: 600;
  color: var(--ink-4);
}
.pf__step--current .pf__step-n { color: var(--accent); }
.pf__step-body { display: flex; flex-direction: column; gap: 8px; min-width: 0; }
.pf__step-stmt {
  font-family: var(--font-text); font-size: 17px; line-height: 1.55;
  color: var(--ink);
}
.pf__step-comm {
  font-family: var(--font-text); font-size: 14px; line-height: 1.55;
  color: var(--ink-3); font-style: italic; max-width: 64ch;
}
.pf__step-just {
  font-size: 12px; padding: 12px 14px;
  background: var(--paper-2); border: 1px solid var(--rule-3);
  display: flex; flex-direction: column; gap: 6px;
}
.pf__step-just-h {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
}
.pf__step-just-body { color: var(--ink-2); }

.pf__qed {
  display: flex; align-items: baseline; gap: 12px;
  padding: 22px 0 0; margin-top: 16px;
  border-top: 2px solid var(--ink);
}
.pf__qed-mark {
  display: inline-block; width: 12px; height: 12px;
  background: var(--ink);
}

/* Tree view */
.pf__tree { padding: 28px 48px 36px; border-top: 1px solid var(--rule); }
.pf__tree-mode {
  display: inline-flex; border: 1px solid var(--rule); margin-bottom: 18px;
}
.pf__tree-mode button {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.08em;
  text-transform: uppercase; padding: 7px 12px;
  border: 0; border-right: 1px solid var(--rule);
  background: var(--paper); color: var(--ink-3); cursor: pointer;
}
.pf__tree-mode button:last-child { border-right: 0; }
.pf__tree-mode button.is-on { background: var(--ink); color: var(--paper); }

.pf__outline { display: flex; flex-direction: column; gap: 4px; }
.pf__outline-item {
  display: grid; grid-template-columns: 30px 1fr auto;
  gap: 12px; align-items: baseline;
  padding: 8px 0; font-family: var(--font-text); font-size: 14px;
  border-bottom: 1px solid var(--rule-3);
}
.pf__outline-item--l1 { padding-left: 0; font-weight: 500; }
.pf__outline-item--l2 { padding-left: 24px; }
.pf__outline-item--l3 { padding-left: 48px; color: var(--ink-3); }

.pf__svg-tree {
  width: 100%; height: 480px;
  border: 1px solid var(--rule); background: var(--paper-2);
}


/* ─── PROCEDURE PAGE (pr__) ─── */
.pr { background: var(--paper); color: var(--ink); font-family: var(--font-ui); }
.pr__top {
  display: flex; justify-content: space-between; align-items: center;
  padding: 16px 48px; min-height: 56px;
}
.pr__hero {
  display: grid; grid-template-columns: 1fr 340px;
  gap: 56px; padding: 36px 48px 28px;
}
.pr__title { font-size: 48px; font-weight: 500; line-height: 1.05; margin: 8px 0 14px; }
.pr__when {
  font-family: var(--font-text); font-size: 18px; line-height: 1.55;
  color: var(--ink-2); max-width: 60ch;
}
.pr__when strong { color: var(--ink); font-weight: 600; }

.pr__sect { padding: 28px 48px; border-top: 1px solid var(--rule); }
.pr__sect-head {
  display: flex; align-items: baseline; gap: 14px; margin-bottom: 18px;
}
.pr__sect-id { margin-left: auto; color: var(--ink-4); }

.pr__example-source {
  font-family: var(--font-text);
  font-size: 28px; padding: 18px 0;
  border-bottom: 1px solid var(--rule-2); margin-bottom: 18px;
}
.pr__example-source-label {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
  display: block; margin-bottom: 8px;
}

.pr__steps { display: flex; flex-direction: column; }
.pr__step {
  border: 1px solid var(--rule-3);
  border-bottom: 0;
  padding: 14px 18px;
  display: grid; grid-template-columns: 32px 1fr auto;
  gap: 14px; align-items: center; cursor: pointer;
  transition: background 100ms ease;
}
.pr__step:last-child { border-bottom: 1px solid var(--rule-3); }
.pr__step:hover { background: var(--paper-2); }
.pr__step--expanded {
  cursor: default; padding: 0; display: block;
  border-color: var(--ink); background: var(--paper-2);
}
.pr__step-n { font-family: var(--font-mono); color: var(--ink-4); font-weight: 500; }
.pr__step--expanded .pr__step-n { color: var(--accent); }
.pr__step-summary { font-size: 14px; }
.pr__step-chev { color: var(--ink-4); font-family: var(--font-mono); font-size: 14px; }

.pr__step-content { padding: 18px 22px; display: flex; flex-direction: column; gap: 16px; }
.pr__step-row { display: grid; grid-template-columns: 110px 1fr; gap: 14px; align-items: baseline; }
.pr__step-row-h {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4); padding-top: 4px;
}
.pr__step-math {
  font-family: var(--font-text); font-size: 22px;
  padding: 12px 16px; background: var(--paper);
  border: 1px solid var(--rule-3);
}
.pr__step-prose {
  font-family: var(--font-text); font-size: 15px; line-height: 1.6;
  color: var(--ink-2);
}
.pr__step-author {
  display: inline-flex; align-items: center; gap: 8px; padding: 6px 10px;
  border: 1px solid var(--rule-2); background: var(--paper);
  font-size: 12px;
}

/* Try-it slot */
.pr__tryit {
  border: 2px solid var(--ink); padding: 24px;
  display: flex; flex-direction: column; gap: 18px;
}
.pr__tryit-head {
  display: flex; justify-content: space-between; align-items: baseline;
  padding-bottom: 12px; border-bottom: 1px solid var(--ink);
}
.pr__tryit-input-row {
  display: flex; gap: 12px; align-items: center;
}
.pr__tryit-input {
  flex: 1; padding: 14px 16px;
  border: 1px solid var(--rule-2); background: var(--paper);
  font-family: var(--font-text); font-size: 22px;
  font-style: italic; color: var(--ink);
}
.pr__tryit-input:focus { outline: none; border-color: var(--accent); }
.pr__tryit-go {
  background: var(--accent); color: var(--paper); border: 0;
  padding: 14px 22px; font: 500 12px/1 var(--font-mono);
  letter-spacing: 0.1em; text-transform: uppercase; cursor: pointer;
}
.pr__tryit-flow { display: flex; flex-direction: column; gap: 12px; padding-top: 6px; }
.pr__tryit-line {
  display: grid; grid-template-columns: 90px 1fr;
  gap: 14px; align-items: baseline;
  padding: 8px 0; border-bottom: 1px solid var(--rule-3);
}
.pr__tryit-prompt {
  font: 500 10px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
}
.pr__tryit-line--user .pr__tryit-prompt { color: var(--accent); }
.pr__tryit-content {
  font-family: var(--font-text); font-size: 18px;
}
.pr__tryit-content--prose { font-size: 14px; line-height: 1.6; color: var(--ink-2); font-style: italic; }
.pr__tryit-cursor {
  display: inline-block; width: 7px; height: 18px; background: var(--accent);
  vertical-align: -3px; margin-left: 2px;
  animation: pr-blink 900ms steps(2, end) infinite;
}
@keyframes pr-blink { 50% { opacity: 0; } }


/* ─── COMPARATIVE VIEW (cmp__) ─── */
.cmp { background: var(--paper); color: var(--ink); font-family: var(--font-ui); }
.cmp__top {
  display: flex; justify-content: space-between; align-items: center;
  padding: 16px 48px; min-height: 56px;
}
.cmp__hero { padding: 28px 48px 8px; }
.cmp__hero-h {
  font-size: 36px; font-weight: 500; line-height: 1.1; margin: 8px 0;
}
.cmp__hero-sub {
  font-family: var(--font-text); font-size: 18px;
  color: var(--ink-2); max-width: 70ch;
}

.cmp__table {
  margin: 24px 48px 36px;
  border: 1px solid var(--ink);
}
.cmp__row {
  display: grid; grid-template-columns: 200px repeat(3, 1fr);
  border-bottom: 1px solid var(--rule-3);
}
.cmp__row:last-child { border-bottom: 0; }
.cmp__row--header { background: var(--ink); color: var(--paper); }
.cmp__row--diverges { background: color-mix(in oklab, var(--accent) 5%, transparent); }

.cmp__row-label {
  padding: 18px 16px; border-right: 1px solid var(--rule-3);
  font: 500 11px/1 var(--font-mono); letter-spacing: 0.1em;
  text-transform: uppercase; color: var(--ink-4);
  display: flex; align-items: flex-start; flex-direction: column; gap: 4px;
}
.cmp__row--diverges .cmp__row-label { color: var(--accent); }
.cmp__row--header .cmp__row-label { color: var(--paper); border-right-color: var(--ink-3); }
.cmp__row-tag {
  font: 500 9px/1 var(--font-mono); padding: 2px 6px;
  border: 1px solid currentColor; opacity: 0.7;
  margin-top: auto;
}

.cmp__cell {
  padding: 18px 22px; border-right: 1px solid var(--rule-3);
  display: flex; flex-direction: column; gap: 6px;
}
.cmp__cell:last-child { border-right: 0; }

.cmp__col-head {
  display: flex; flex-direction: column; gap: 8px;
}
.cmp__col-name {
  font-family: var(--font-ui); font-weight: 500; font-size: 22px;
  color: var(--paper);
}
.cmp__col-id {
  font-family: var(--font-mono); font-size: 11px; color: var(--ink-5);
}
.cmp__col-shape { display: flex; align-items: center; gap: 8px; }

.cmp__cell-formula {
  font-family: var(--font-text); font-size: 17px; line-height: 1.4;
}
.cmp__cell-prose {
  font-family: var(--font-text); font-size: 14px; line-height: 1.55;
  color: var(--ink-2);
}
.cmp__cell-mono { font-family: var(--font-mono); font-size: 12px; color: var(--ink-3); }
.cmp__cell-list { font-size: 12px; color: var(--ink-2); display: flex; flex-direction: column; gap: 4px; }

.cmp__legend {
  display: flex; align-items: center; gap: 18px; padding: 0 48px 28px;
  font-size: 12px; color: var(--ink-3);
}
.cmp__legend-swatch {
  display: inline-block; width: 14px; height: 14px;
  background: color-mix(in oklab, var(--accent) 12%, var(--paper));
  border: 1px solid var(--accent); vertical-align: middle; margin-right: 8px;
}