/* =====================================================================
   Interactive companion — styles
   Colour roles are tokens; dark values are stepped for the dark surface.
   ===================================================================== */
:root {
  color-scheme: light;
  --bg: #fcfcfb;
  --panel: #f5f4f0;
  --panel-2: #ffffff;
  --ink: #0b0b0b;
  --ink-2: #52514e;
  --muted: #898781;
  --grid: #e1e0d9;
  --axis: #c3c2b7;
  --border: rgba(11, 11, 11, 0.1);
  --accent: #d95926;

  /* model semantics, fixed across the page */
  --c-contract: #2a78d6; /* affine, ρ < 1 */
  --c-nfsm: #eb6834; /* restoring / NFSM */
  --c-iso: #1baf7a; /* affine, ρ = 1 */

  /* automaton states (categorical order) */
  --s0: #2a78d6;
  --s1: #eb6834;
  --s2: #1baf7a;
  --s3: #eda100;
  --s4: #e87ba4;
  --s5: #008300;
  --s6: #4a3aa7;
  --s7: #e34948;

  --code: #4a3aa7;
  --good: #0ca30c;
  --good-text: #006300;
  --bad: #d03b3b;
  --warn: #b27400;
  --seq: #1c5cab;
  --band-alpha: 0.16;
  --code-panel: #f1f0eb;
  --tk-kw: #7b3fb0;
  --tk-str: #1d7a3e;
  --tk-num: #b35300;
  --tk-fn: #1c5cab;
  --tk-bi: #0f6f73;

  --serif: "Source Serif 4", Georgia, "Times New Roman", serif;
  --sans: Inter, system-ui, -apple-system, "Segoe UI", sans-serif;
  --mono: "JetBrains Mono", ui-monospace, SFMono-Regular, Menlo, monospace;
}
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    color-scheme: dark;
    --bg: #141413;
    --panel: #1c1c1b;
    --panel-2: #232322;
    --ink: #f4f3ef;
    --ink-2: #c3c2b7;
    --muted: #8f8d86;
    --grid: #2c2c2a;
    --axis: #45443f;
    --border: rgba(255, 255, 255, 0.1);
    --accent: #eb6834;
    --c-contract: #3987e5;
    --c-nfsm: #e0652f;
    --c-iso: #199e70;
    --s0: #3987e5;
    --s1: #d95926;
    --s2: #199e70;
    --s3: #c98500;
    --s4: #d55181;
    --s5: #1a9a1a;
    --s6: #9085e9;
    --s7: #e66767;
    --code: #9085e9;
    --good-text: #3cc13c;
    --bad: #e66767;
    --warn: #e0a526;
    --seq: #6da7ec;
    --band-alpha: 0.2;
  --code-panel: #181817;
  --tk-kw: #c3a6f5;
  --tk-str: #7fd39a;
  --tk-num: #f2a65e;
  --tk-fn: #86b6ef;
  --tk-bi: #6fd0d3;
  }
}
:root[data-theme="dark"] {
  color-scheme: dark;
  --bg: #141413;
  --panel: #1c1c1b;
  --panel-2: #232322;
  --ink: #f4f3ef;
  --ink-2: #c3c2b7;
  --muted: #8f8d86;
  --grid: #2c2c2a;
  --axis: #45443f;
  --border: rgba(255, 255, 255, 0.1);
  --accent: #eb6834;
  --c-contract: #3987e5;
  --c-nfsm: #e0652f;
  --c-iso: #199e70;
  --s0: #3987e5;
  --s1: #d95926;
  --s2: #199e70;
  --s3: #c98500;
  --s4: #d55181;
  --s5: #1a9a1a;
  --s6: #9085e9;
  --s7: #e66767;
  --code: #9085e9;
  --good-text: #3cc13c;
  --bad: #e66767;
  --warn: #e0a526;
  --seq: #6da7ec;
  --band-alpha: 0.2;
  --code-panel: #181817;
  --tk-kw: #c3a6f5;
  --tk-str: #7fd39a;
  --tk-num: #f2a65e;
  --tk-fn: #86b6ef;
  --tk-bi: #6fd0d3;
}

* {
  box-sizing: border-box;
}
html {
  scroll-behavior: smooth;
  scroll-padding-top: 64px;
}
body {
  margin: 0;
  background: var(--bg);
  color: var(--ink);
  font: 18px/1.65 var(--serif);
  -webkit-font-smoothing: antialiased;
  overflow-x: hidden;
}
a {
  color: inherit;
  text-decoration-color: var(--accent);
  text-underline-offset: 2px;
}
code {
  font: 0.82em var(--mono);
  background: var(--panel);
  border: 1px solid var(--border);
  border-radius: 4px;
  padding: 0.05em 0.3em;
}

/* ---------------------------------------------------------------- top bar & toc */
.topbar {
  position: sticky;
  top: 0;
  z-index: 20;
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 12px;
  padding: 8px 16px;
  background: color-mix(in srgb, var(--bg) 88%, transparent);
  backdrop-filter: blur(8px);
  border-bottom: 1px solid var(--border);
  font-family: var(--sans);
}
.brand {
  font-weight: 600;
  font-size: 14px;
  text-decoration: none;
}
.brand span {
  color: var(--muted);
  font-weight: 400;
  margin-left: 6px;
}
.topbar-right {
  display: flex;
  align-items: center;
  gap: 12px;
}
.site-back {
  font: 400 13px var(--sans);
  color: var(--muted);
  text-decoration: none;
  white-space: nowrap;
}
.site-back:hover {
  color: var(--accent);
}
@media (max-width: 640px) {
  .site-back {
    display: none;
  }
}
.toc {
  display: none;
}
@media (min-width: 1420px) {
  .toc {
    display: block;
    position: fixed;
    top: 90px;
    left: max(16px, calc(50vw - 690px));
    width: 190px;
    font: 13px/1.4 var(--sans);
  }
  .toc-title {
    color: var(--muted);
    text-transform: uppercase;
    letter-spacing: 0.06em;
    font-size: 11px;
    margin-bottom: 8px;
  }
  .toc ol {
    list-style: none;
    padding: 0;
    margin: 0;
  }
  .toc li {
    margin: 0 0 6px;
  }
  .toc a {
    text-decoration: none;
    color: var(--ink-2);
  }
  .toc a:hover,
  .toc a.active {
    color: var(--ink);
  }
  .toc b {
    display: inline-block;
    width: 26px;
    color: var(--muted);
    font-weight: 500;
  }
}

/* ---------------------------------------------------------------- article grid */
.article {
  display: grid;
  grid-template-columns: minmax(0, 1fr) min(700px, calc(100% - 32px)) minmax(0, 1fr);
  padding-bottom: 80px;
}
.article > * {
  grid-column: 2;
  min-width: 0;
}
.article > .nb-figure {
  grid-column: 1 / -1;
  width: min(1060px, calc(100% - 32px));
  justify-self: center;
}
.hero {
  padding: 56px 0 8px;
}
.kicker {
  font: 500 13px var(--sans);
  color: var(--accent);
  text-transform: uppercase;
  letter-spacing: 0.08em;
  margin: 0 0 12px;
}
h1 {
  font: 600 clamp(30px, 5vw, 44px) / 1.12 var(--serif);
  margin: 0 0 18px;
  letter-spacing: -0.01em;
}
.hero-note {
  font: 400 15px/1.5 var(--sans);
  color: var(--ink-2);
  margin: 14px 0 0;
}
.authors {
  font: 400 15px/1.5 var(--sans);
  color: var(--ink-2);
  margin: -8px 0 18px;
}
.authors span {
  color: var(--muted);
  font-size: 14px;
}
.dek {
  font-size: 21px;
  line-height: 1.5;
  color: var(--ink-2);
  margin: 0;
}
h2 {
  font: 600 28px/1.25 var(--serif);
  margin: 56px 0 12px;
}
h2.small {
  font: 600 13px var(--sans);
  text-transform: uppercase;
  letter-spacing: 0.06em;
  color: var(--muted);
  margin: 0 0 8px;
}
h3 {
  font: 600 21px/1.3 var(--serif);
  margin: 36px 0 8px;
}
p {
  margin: 0 0 14px;
}
ul.tight li {
  margin-bottom: 4px;
}
.howto {
  margin-top: 32px;
  padding: 20px 22px;
  background: var(--panel);
  border: 1px solid var(--border);
  border-radius: 12px;
  font-size: 16.5px;
}
.paperref {
  display: inline-block;
  font: 500 12px/1.4 var(--sans);
  color: var(--accent);
  border: 1px solid color-mix(in srgb, var(--accent) 45%, transparent);
  background: color-mix(in srgb, var(--accent) 7%, transparent);
  border-radius: 999px;
  padding: 3px 10px;
  margin: 48px 0 0;
}
.paperref::before {
  content: "";
  font-weight: 600;
}
.paperref.inline {
  margin: 0;
  font-size: 11.5px;
  padding: 1px 8px;
}
section + section .paperref,
h3 + .paperref,
p + .paperref {
  margin-top: 28px;
}
.paperref + h2 {
  margin-top: 10px;
}
.paperref + h3 {
  margin-top: 10px;
}
.foot {
  margin-top: 56px;
  padding-top: 18px;
  border-top: 1px solid var(--border);
  font: 14px/1.6 var(--sans);
  color: var(--ink-2);
}
.todo {
  color: var(--bad);
}

/* ---------------------------------------------------------------- figures */
.nb-figure {
  margin: 28px 0 8px;
  font: 14px/1.5 var(--sans);
  perspective: 2600px;
}
.nb-figure:not(.has-code),
.nb-face {
  padding: 18px 20px 16px;
  background: var(--panel);
  border: 1px solid var(--border);
  border-radius: 14px;
}

/* ---------------------------------------------------------------- flip to code */
.nb-flip {
  position: relative;
  transform-style: preserve-3d;
  transition: transform 0.75s cubic-bezier(0.3, 0.7, 0.2, 1);
}
.nb-figure.flipped .nb-flip {
  transform: rotateY(180deg);
}
.nb-face {
  -webkit-backface-visibility: hidden;
  backface-visibility: hidden;
}
.nb-face.back {
  position: absolute;
  inset: 0;
  transform: rotateY(180deg);
  overflow: auto;
  background: var(--code-panel);
}
.code-btn {
  float: right;
  margin: -4px 0 4px 12px;
  font: 500 12.5px/1 var(--mono);
  padding: 6px 10px;
  min-height: 28px;
}
.nb-figure.flipped .front .code-btn,
.code-btn:hover {
  border-color: var(--accent);
  color: var(--accent);
}
.code-head {
  display: flex;
  align-items: center;
  gap: 10px;
  margin-bottom: 6px;
  font: 500 15px var(--sans);
}
.code-head .code-btn {
  float: none;
  margin: 0 0 0 auto;
}
.code-block-title {
  font: 600 12.5px var(--sans);
  color: var(--ink-2);
  margin: 12px 0 0;
}
pre.code {
  margin: 6px 0 0;
  padding: 12px 0;
  font: 12.5px/1.65 var(--mono);
  background: var(--panel-2);
  border: 1px solid var(--border);
  border-radius: 10px;
  overflow-x: auto;
  counter-reset: ln;
  color: var(--ink);
  tab-size: 4;
  font-variant-ligatures: none;
}
pre.code .ln {
  display: block;
  padding-right: 16px;
  white-space: pre;
}
pre.code .ln::before {
  counter-increment: ln;
  content: counter(ln);
  display: inline-block;
  width: 2.4em;
  margin-right: 1.2em;
  text-align: right;
  color: var(--muted);
  opacity: 0.55;
  user-select: none;
}
.tk-kw {
  color: var(--tk-kw);
  font-weight: 500;
}
.tk-str {
  color: var(--tk-str);
}
.tk-num {
  color: var(--tk-num);
}
.tk-com {
  color: var(--muted);
  font-style: italic;
}
.tk-fn {
  color: var(--tk-fn);
}
.tk-bi {
  color: var(--tk-bi);
}
.live {
  font-style: normal;
  font-weight: 600;
  color: var(--ink);
  background: color-mix(in srgb, var(--accent) 16%, transparent);
  box-shadow: inset 0 0 0 1px color-mix(in srgb, var(--accent) 50%, transparent);
  border-radius: 4px;
  padding: 0 3px;
}
.live.bump {
  animation: live-bump 0.7s ease-out;
}
@keyframes live-bump {
  0% {
    background: color-mix(in srgb, var(--accent) 55%, transparent);
  }
  100% {
    background: color-mix(in srgb, var(--accent) 16%, transparent);
  }
}
.code-foot {
  margin: 12px 2px 0;
  font: 12.5px/1.5 var(--sans);
  color: var(--ink-2);
}
@media (prefers-reduced-motion: reduce) {
  .nb-flip {
    transition: none;
  }
  .live.bump {
    animation: none;
  }
}
.nb-figure figcaption {
  font: 500 15px/1.45 var(--sans);
  margin: 0 0 12px;
  color: var(--ink);
}
.fig-no {
  display: inline-block;
  min-width: 34px;
  padding: 1px 7px;
  margin-right: 8px;
  border-radius: 6px;
  background: var(--ink);
  color: var(--bg);
  font: 600 12px/1.6 var(--sans);
  text-align: center;
  vertical-align: 1px;
}
.nb-fig-body {
  position: relative;
  min-width: 0;
}
.nb-figure,
.nb-panel,
.nb-table-wrap {
  min-width: 0;
  max-width: 100%;
}
.nb-fig-body.busy::after {
  content: "computing…";
  position: absolute;
  top: 6px;
  right: 8px;
  font: 12px var(--sans);
  color: var(--muted);
}
.try {
  margin: 4px 0 12px;
  padding: 7px 14px;
  border-left: 3px solid var(--accent);
  background: var(--panel-2);
  border-radius: 0 8px 8px 0;
  font: 14px/1.5 var(--sans);
  color: var(--ink-2);
}
.try > b {
  color: var(--ink);
  font-size: 12px;
  text-transform: uppercase;
  letter-spacing: 0.06em;
  margin-right: 6px;
}
.nb-error {
  color: var(--bad);
}

/* panels */
.nb-panels {
  display: flex;
  flex-wrap: wrap;
  gap: 14px;
  margin-top: 10px;
}
.nb-panel {
  flex: 0 1 auto;
  min-width: 0;
  background: var(--panel-2);
  border: 1px solid var(--border);
  border-radius: 10px;
  padding: 10px 12px;
}
.nb-panel.grow {
  flex: 1 1 380px;
}
.nb-panel.wide {
  flex: 1 1 100%;
  margin-top: 10px;
}
.nb-panels > .nb-panel:not(.grow):not(.wide) {
  flex: 1 1 300px;
  max-width: 420px;
}
.nb-panel-title {
  font: 500 12.5px/1.4 var(--sans);
  color: var(--ink-2);
  margin-bottom: 6px;
}
.nb-svg {
  display: block;
  width: 100%;
  height: auto;
  overflow: visible;
  font-family: var(--sans);
  touch-action: pan-y;
}
.nb-caption {
  font: 13px/1.5 var(--sans);
  color: var(--ink-2);
  margin: 8px 2px 0;
}

/* ---------------------------------------------------------------- controls */
.nb-controls {
  display: flex;
  flex-wrap: wrap;
  align-items: flex-end;
  gap: 10px 22px;
  margin-bottom: 8px;
}
.nb-controls.nb-symbols,
.nb-controls.nb-tabs {
  align-items: center;
  gap: 6px;
}
.nb-group {
  display: flex;
  flex-direction: column;
  gap: 4px;
}
.nb-group-label {
  font: 500 11.5px var(--sans);
  color: var(--muted);
  text-transform: uppercase;
  letter-spacing: 0.05em;
  margin-right: 4px;
}
.nb-group-body {
  display: flex;
  flex-wrap: wrap;
}
.nb-btn {
  font: 500 13px/1 var(--sans);
  color: var(--ink);
  background: var(--panel-2);
  border: 1px solid var(--axis);
  border-radius: 8px;
  padding: 7px 11px;
  min-height: 32px;
  cursor: pointer;
  transition: background 0.12s, border-color 0.12s;
}
.nb-btn:hover {
  border-color: var(--ink-2);
}
.nb-btn:active {
  transform: translateY(1px);
}
.nb-btn:focus-visible,
.nb-seg-btn:focus-visible,
input:focus-visible,
.heat-cell:focus-visible {
  outline: 2px solid var(--accent);
  outline-offset: 2px;
}
a.nb-btn {
  display: inline-flex;
  align-items: center;
  text-decoration: none;
  white-space: nowrap;
}
.nb-btn.ghost {
  background: transparent;
  border-color: var(--border);
  color: var(--ink-2);
}
.nb-btn.sym {
  font-family: var(--mono);
  font-weight: 500;
}
.nb-btn small {
  font: 11px var(--sans);
  color: var(--muted);
  margin-left: 4px;
}
.nb-btn.on,
.nb-btn.tab.on {
  background: var(--ink);
  color: var(--bg);
  border-color: var(--ink);
}
.nb-btn.tab {
  font-family: var(--mono);
}
.nb-seg .nb-group-body {
  align-self: flex-start;
  border: 1px solid var(--axis);
  border-radius: 8px;
  overflow: hidden;
}
.nb-seg-btn {
  font: 500 13px/1 var(--sans);
  color: var(--ink-2);
  background: var(--panel-2);
  border: 0;
  border-right: 1px solid var(--axis);
  padding: 8px 11px;
  min-height: 32px;
  cursor: pointer;
}
.nb-seg-btn:last-child {
  border-right: 0;
}
.nb-seg-btn.on {
  background: var(--ink);
  color: var(--bg);
}
.nb-slider {
  display: flex;
  flex-direction: column;
  gap: 2px;
  width: 190px;
  font: 12.5px var(--sans);
}
.nb-slider-head {
  display: flex;
  justify-content: space-between;
  gap: 8px;
  color: var(--ink-2);
}
.nb-slider-val {
  font: 500 12px var(--mono);
  color: var(--ink);
  white-space: nowrap;
}
.nb-slider input[type="range"] {
  width: 100%;
  accent-color: var(--ink);
  margin: 4px 0 0;
  height: 22px;
}

/* stats */
.nb-stats {
  display: grid;
  grid-auto-flow: column;
  grid-auto-columns: 1fr;
  gap: 8px;
  margin-top: 12px;
}
.nb-stat {
  background: var(--panel-2);
  border: 1px solid var(--border);
  border-radius: 8px;
  padding: 7px 10px;
  display: flex;
  flex-direction: column;
  gap: 2px;
  min-width: 0;
}
.nb-stat-label {
  font: 11.5px var(--sans);
  color: var(--muted);
}
.nb-stat-val {
  font: 500 13px/1.45 var(--sans);
  color: var(--ink);
}
.nb-stat[data-status="good"] .nb-stat-val {
  color: var(--good-text);
}
.nb-stat[data-status="bad"] .nb-stat-val {
  color: var(--bad);
}
.nb-stat[data-status="warn"] .nb-stat-val {
  color: var(--warn);
}
.nb-stat[data-status="good"] {
  border-left: 3px solid var(--good);
}
.nb-stat[data-status="bad"] {
  border-left: 3px solid var(--bad);
}
.nb-stat[data-status="warn"] {
  border-left: 3px solid var(--warn);
}

/* legend */
.nb-legend {
  display: flex;
  flex-wrap: wrap;
  gap: 4px 16px;
  font: 12px var(--sans);
  color: var(--ink-2);
  margin-top: 6px;
}
.nb-legend > span {
  display: inline-flex;
  align-items: center;
  gap: 6px;
}
.nb-legend .sw {
  display: inline-block;
  flex: none;
}
.sw.line {
  width: 18px;
  height: 0;
  border-top: 2px solid var(--sw);
}
.sw.line.dash {
  border-top-style: dashed;
}
.sw.line.dotted {
  border-top-style: dotted;
}
.sw.dot {
  width: 8px;
  height: 8px;
  border-radius: 50%;
  background: var(--sw);
}
.sw.ring {
  width: 12px;
  height: 12px;
  border-radius: 50%;
  border: 1.5px dashed var(--sw);
}
.sw.diamond {
  width: 8px;
  height: 8px;
  background: var(--sw);
  transform: rotate(45deg);
}
.sw.bar {
  width: 5px;
  height: 14px;
  border-radius: 2px;
  background: var(--sw);
}
i.dot {
  display: inline-block;
  width: 9px;
  height: 9px;
  border-radius: 50%;
  background: var(--sw);
  margin-right: 7px;
  vertical-align: 0;
}

/* tooltip */
.nb-tip {
  position: fixed;
  z-index: 50;
  pointer-events: none;
  display: none;
  background: var(--panel-2);
  color: var(--ink);
  border: 1px solid var(--border);
  box-shadow: 0 6px 24px rgba(0, 0, 0, 0.14);
  border-radius: 8px;
  padding: 8px 10px;
  font: 12.5px/1.45 var(--sans);
  min-width: 150px;
}
.tip-head {
  font-weight: 600;
  margin-bottom: 4px;
}
.tip-row {
  display: flex;
  align-items: center;
  gap: 6px;
  color: var(--ink-2);
}
.tip-row i {
  width: 8px;
  height: 8px;
  border-radius: 50%;
}
.tip-row b {
  margin-left: auto;
  padding-left: 12px;
  color: var(--ink);
  font: 500 12px var(--mono);
}

/* ---------------------------------------------------------------- tables */
.nb-table-wrap {
  overflow-x: auto;
  margin-top: 6px;
}
.nb-table {
  width: 100%;
  border-collapse: collapse;
  font: 13px/1.45 var(--sans);
}
.nb-table th,
.nb-table td {
  text-align: left;
  padding: 6px 8px;
  border-bottom: 1px solid var(--grid);
  vertical-align: top;
}
.nb-table th {
  font-weight: 500;
  color: var(--muted);
  font-size: 12px;
}
.nb-table td.num {
  font: 12.5px var(--mono);
  text-align: right;
  font-variant-numeric: tabular-nums;
}
.nb-table .mono {
  font: 12.5px var(--mono);
}
.nb-table tr.on td {
  background: color-mix(in srgb, var(--accent) 12%, transparent);
  font-weight: 600;
}
.nb-table.compact td,
.nb-table.compact th {
  padding: 4px 8px;
}
.nb-table.map td:first-child {
  white-space: nowrap;
  color: var(--accent);
  font-weight: 500;
}
.nb-table.map td:nth-child(2) {
  white-space: nowrap;
}
.status-good {
  color: var(--good-text);
}
.status-bad {
  color: var(--bad);
}
.status-warn {
  color: var(--warn);
}
.nb-table.results {
  min-width: 860px;
  table-layout: fixed;
}
.nb-table.results th.task {
  text-align: center;
  color: var(--ink);
  font-weight: 600;
}
.nb-table.results th.task.definite {
  background: color-mix(in srgb, var(--c-contract) 8%, transparent);
}
.nb-table.results th.model {
  width: 150px;
  white-space: nowrap;
  color: var(--ink);
  font-weight: 600;
  font-size: 13px;
}
.nb-table.results .sub {
  display: block;
  white-space: normal;
  font: 400 11px/1.3 var(--sans);
  color: var(--muted);
}
.nb-table.results td.cell {
  text-align: center;
  vertical-align: middle;
  font: 500 12.5px var(--mono);
  border: 2px solid var(--panel-2);
  background: color-mix(in srgb, var(--seq) calc(var(--f, 0) * 100%), var(--panel-2));
  color: var(--ink);
  cursor: default;
}
.nb-table.results td.cell.deep {
  color: #fff;
}
.nb-table.results td.cell.deep .sub {
  color: rgba(255, 255, 255, 0.82);
}
:root[data-theme="dark"] .nb-table.results td.cell.deep,
:root[data-theme="dark"] .nb-table.results td.cell.deep .sub {
  color: #0b0b0b;
}
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) .nb-table.results td.cell.deep,
  :root:not([data-theme="light"]) .nb-table.results td.cell.deep .sub {
    color: #0b0b0b;
  }
}
.nb-table.results tr.nfsm th.model {
  color: var(--accent);
}
.nb-table.results td.seeds {
  padding: 3px;
}
.nb-table.results .seed {
  display: block;
  font-size: 11px;
  padding: 1px 2px;
  margin: 1px 0;
  border-radius: 3px;
  background: color-mix(in srgb, var(--seq) calc(var(--f, 0) * 100%), var(--panel-2));
}
.nb-table.results .seed.x {
  color: var(--muted);
}

/* ---------------------------------------------------------------- figure-specific HTML */
.nb-tape {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 4px;
  min-height: 30px;
  margin-bottom: 6px;
  font: 12px var(--mono);
}
.tape-label {
  color: var(--muted);
  margin-right: 2px;
}
.tape-chip {
  padding: 2px 6px;
  border-radius: 5px;
  background: var(--panel);
  border: 1px solid var(--border);
}
.tape-more,
.tape-empty {
  color: var(--muted);
  font-family: var(--sans);
}
.nb-story {
  font: 14px/2 var(--mono);
  max-height: 440px;
  overflow-y: auto;
}
.tok {
  display: inline-block;
  padding: 0 5px;
  margin: 0 1px;
  border-radius: 4px;
  color: var(--muted);
  cursor: pointer;
}
.tok.read {
  color: var(--ink);
}
.tok.last {
  background: var(--ink);
  color: var(--bg);
}
.tok.q {
  font-weight: 600;
}
.nb-answer {
  margin-top: 10px;
  font: 14px var(--sans);
}
.nb-answer b {
  color: var(--accent);
}
.nb-gif-wrap {
  background: #fff;
  border-radius: 10px;
  overflow: hidden;
  border: 1px solid var(--border);
}
.nb-gif {
  display: block;
  width: 100%;
  height: auto;
  min-height: 200px;
}

/* ---------------------------------------------------------------- SVG marks */
.nb-svg text {
  fill: var(--ink-2);
}
.nb-svg .grid {
  stroke: var(--grid);
  stroke-width: 1;
}
.nb-svg .baseline {
  stroke: var(--axis);
  stroke-width: 1;
}
.nb-svg .tick {
  font: 11px var(--sans);
  fill: var(--muted);
  font-variant-numeric: tabular-nums;
}
.nb-svg .axis-label {
  font: 12px var(--sans);
  fill: var(--ink-2);
}
.nb-svg .svg-note {
  font: 11.5px var(--sans);
  fill: var(--ink-2);
}
.nb-svg .svg-note.strong {
  font-weight: 600;
  fill: var(--ink);
}
.nb-svg .svg-note.tiny {
  font-size: 10px;
  fill: var(--muted);
}
.nb-svg .svg-note.bad {
  fill: var(--bad);
  font-weight: 600;
}
.nb-svg .svg-note.good {
  fill: var(--good-text);
  font-weight: 600;
}
.nb-svg .series {
  fill: none;
  stroke-width: 2;
  stroke-linejoin: round;
  stroke-linecap: round;
}
.nb-svg .series.thin {
  stroke-width: 1.2;
}
.nb-svg .series.thick {
  stroke-width: 3;
}
.nb-svg .series.dash {
  stroke-dasharray: 5 4;
}
.nb-svg .series.dot {
  stroke-dasharray: 1 4;
}
.nb-svg .marker-line {
  stroke: var(--muted);
  stroke-width: 1.2;
  stroke-dasharray: 3 3;
}
.nb-svg .marker-line.bad {
  stroke: var(--bad);
}
.nb-svg .hit {
  fill: transparent;
  cursor: crosshair;
}
.nb-svg .crosshair {
  stroke: var(--muted);
  stroke-width: 1;
}
.nb-svg .hover-dot {
  stroke: var(--panel-2);
  stroke-width: 2;
}

/* automaton graphs */
.nb-svg .edge {
  fill: none;
  stroke: var(--axis);
  stroke-width: 1.6;
}
.nb-svg .edge.hot {
  stroke: var(--accent);
  stroke-width: 2.4;
}
.nb-svg .arrowhead {
  fill: var(--axis);
}
.nb-svg .arrowhead.hot {
  fill: var(--accent);
}
.nb-svg .node {
  fill: color-mix(in srgb, var(--c) 22%, var(--panel-2));
  stroke: var(--c);
  stroke-width: 1.5;
}
.nb-svg .node.current {
  fill: var(--c);
  stroke: var(--ink);
  stroke-width: 2.5;
}
.nb-svg .node-label {
  font: 600 12px var(--sans);
  fill: var(--ink);
}
.nb-svg .node-label.current {
  fill: #fff;
}
.nb-svg .node-label.small {
  font-size: 11px;
}

/* cells, codes, trajectories */
.nb-svg .cell,
.nb-svg .band {
  fill: var(--c);
  fill-opacity: var(--band-alpha);
  stroke: none;
}
.nb-svg .cell-edge,
.nb-svg .band-edge {
  stroke: var(--panel-2);
  stroke-width: 2;
}
.nb-svg .cell-label {
  font: 500 11.5px var(--sans);
  fill: var(--ink-2);
}
.nb-svg .deadzone {
  fill: var(--panel);
  stroke: var(--axis);
  stroke-dasharray: 2 3;
}
.nb-svg .unit {
  fill: none;
  stroke: var(--axis);
  stroke-width: 1;
}
.nb-svg .code {
  fill: var(--code);
  stroke: var(--panel-2);
  stroke-width: 1.5;
}
.nb-svg .reach {
  fill: var(--ink);
  fill-opacity: 0.05;
  stroke: var(--ink);
  stroke-width: 1.4;
  stroke-dasharray: 4 3;
}
.nb-svg .pt.ok {
  fill: var(--muted);
  fill-opacity: 0.75;
}
.nb-svg .pt.bad {
  fill: var(--bad);
}
.nb-svg .nominal {
  fill: var(--ink);
  stroke: var(--panel-2);
  stroke-width: 2;
}
.nb-svg .chip {
  fill: color-mix(in srgb, var(--c) 30%, var(--panel-2));
  stroke: var(--c);
  stroke-width: 1;
}
.nb-svg .chip.pending {
  fill: var(--panel);
  stroke: var(--axis);
  stroke-dasharray: 3 2;
}
.nb-svg .chip-label {
  font: 600 11px var(--mono);
  fill: var(--ink);
}
.nb-svg .traj {
  fill: none;
  stroke: var(--muted);
  stroke-opacity: 0.45;
  stroke-width: 1;
}
.nb-svg .nominal-line {
  fill: none;
  stroke: var(--ink);
  stroke-width: 1.6;
}
.nb-svg .reach-bar {
  stroke: var(--ink-2);
  stroke-width: 5;
  stroke-linecap: round;
  stroke-opacity: 0.75;
}
.nb-svg .reach-bar.bad {
  stroke: var(--bad);
  stroke-opacity: 0.9;
}
.nb-svg .codept {
  fill: var(--code);
  stroke: var(--panel-2);
  stroke-width: 1.2;
}
.nb-svg .fp.stable {
  fill: var(--ink);
}
.nb-svg .fp.unstable {
  fill: var(--panel-2);
  stroke: var(--ink);
  stroke-width: 1.5;
}
.nb-svg .tube {
  fill: var(--muted);
  fill-opacity: 0.18;
  stroke: none;
}
.nb-svg .tube-bad {
  fill: var(--bad);
  fill-opacity: 0.35;
  stroke: none;
}
.nb-svg .run-bad {
  fill: var(--bad);
}
.nb-svg .tick-sym {
  stroke-width: 2;
  stroke-linecap: round;
}
.nb-svg .target-line {
  fill: none;
  stroke: var(--ink);
  stroke-width: 1;
  stroke-dasharray: 2 3;
}

/* scan */
.nb-svg .scan-edge {
  stroke: var(--axis);
  stroke-width: 1.2;
}
.nb-svg .scan-edge.carried {
  stroke-dasharray: 2 3;
}
.nb-svg .scan-box rect {
  fill: var(--panel-2);
  stroke: var(--axis);
  stroke-width: 1;
}
.nb-svg .scan-box.done rect {
  stroke: var(--c-nfsm);
  stroke-width: 1.8;
}
.nb-svg .scan-tab {
  font: 500 11.5px var(--mono);
  fill: var(--ink);
}
.nb-svg .scan-span {
  font: 9.5px var(--sans);
  fill: var(--muted);
}

/* NFSM heatmap & bars */
.nb-svg .heat-cell {
  cursor: pointer;
}
.nb-svg .heat {
  fill: color-mix(in srgb, var(--seq) calc(var(--f) * 100%), var(--panel-2));
  stroke: var(--grid);
}
.nb-svg .heat-cell:hover .heat {
  stroke: var(--ink);
}
.nb-svg .argmax {
  fill: none;
  stroke: var(--c-nfsm);
  stroke-width: 3;
}
.nb-svg .argmax.wrong {
  stroke: var(--bad);
}
.nb-svg .target-cell {
  fill: none;
  stroke: var(--ink);
  stroke-width: 1.2;
  stroke-dasharray: 3 2;
}
.nb-svg .heat-val {
  font: 500 11px var(--mono);
  fill: var(--ink);
  pointer-events: none;
}
.nb-svg .heat-val.inv {
  fill: #fff;
}
.nb-svg .bar {
  fill: var(--axis);
}
.nb-svg .bar.hl {
  fill: var(--c-nfsm);
}

/* cups & heads */
.nb-svg .cup {
  fill: var(--panel);
  stroke: var(--ink-2);
  stroke-width: 1.5;
}
.nb-svg .cup.hot {
  stroke: var(--accent);
  stroke-width: 2.4;
}
.nb-svg .ball {
  fill: var(--panel-2);
  stroke: var(--ink-2);
  stroke-width: 1.5;
}
.nb-svg .ball.one {
  fill: var(--c-nfsm);
  stroke: var(--c-nfsm);
}
.nb-svg .ball-label {
  font: 600 13px var(--sans);
  fill: var(--ink);
}
.nb-svg .ball-label.one {
  fill: #fff;
}
.nb-svg .idx {
  fill: var(--panel-2);
  stroke: var(--axis);
}
.nb-svg .idx.on {
  fill: var(--c-nfsm);
  stroke: var(--c-nfsm);
}
.nb-svg .idx-label {
  font: 600 12px var(--sans);
  fill: var(--ink-2);
}
.nb-svg .idx-label.on {
  fill: #fff;
}

/* ---------------------------------------------------------------- small screens */
@media (max-width: 640px) {
  body {
    font-size: 17px;
  }
  .nb-face,
  .nb-figure:not(.has-code) {
    padding: 14px 12px;
  }
  .nb-slider {
    width: 100%;
  }
  .nb-panels > .nb-panel:not(.grow):not(.wide) {
    max-width: none;
  }
  .dek {
    font-size: 19px;
  }
  .nb-stats {
    grid-auto-flow: row;
  }
}
@media (prefers-reduced-motion: reduce) {
  html {
    scroll-behavior: auto;
  }
}

/* N5: running realization on the circle */
.nb-svg .drift-target {
  fill: none;
  stroke: var(--ink);
  stroke-width: 1.6;
}
.nb-svg .drift-ray {
  stroke: var(--ink-2);
  stroke-width: 1;
  stroke-dasharray: 2 3;
}
.nb-svg .drift-state {
  fill: var(--c);
  stroke: var(--panel-2);
  stroke-width: 2;
}
.nb-svg .drift-state.bad {
  stroke: var(--bad);
  stroke-width: 3;
}
.nb-svg .now-line {
  stroke: var(--ink-2);
  stroke-width: 1;
}
.nb-svg .series.faded {
  opacity: 0.4;
}

/* LLM-generation notice */
.llm-note {
  margin: 0 0 14px;
  padding: 8px 12px;
  border: 1px solid var(--border);
  border-radius: 8px;
  background: var(--panel-2);
  font: 13px/1.5 var(--sans);
  color: var(--ink-2);
}

.nb-svg .misread-tick {
  fill: var(--bad);
}