:root {
  --proof-sky: #30bced;
  --proof-sky-soft: #daf3fc;
  --proof-graphite: #303036;
  --proof-paper: #fffaff;
  --proof-tomato: #fc5130;
  --proof-teal: #00897b;
  --proof-teal-soft: #dff3ef;
  --proof-violet: #7e57c2;
  --proof-violet-soft: #eee7fa;
  --proof-line: #d7d7dc;
  --proof-muted: #696970;
  --proof-amber: #c77800;
  --proof-amber-soft: #fff3e6;
}

/* ── container ──────────────────────────────────────────────── */

.proof-lab {
  width: min(100%, 1500px);
  margin: 0 auto;
  padding: clamp(.4rem, 1.2vw, .75rem) clamp(.75rem, 2.4vw, 2.5rem) 3.5rem;
  color: var(--proof-graphite);
}

/* ── header (pre-interaction intro) ──────────────────────────── */

.proof-lab__header {
  max-width: 940px;
  margin: 0 auto clamp(.35rem, 1vw, .55rem);
  text-align: center;
}

.proof-lab__breadcrumb {
  margin: 0 0 .35rem;
  color: #167b9e;
  font-size: .72rem;
  font-weight: 700;
  letter-spacing: .08em;
  text-transform: uppercase;
}

.proof-lab__header h1 {
  margin: 0 0 .3rem;
  color: var(--proof-graphite);
  font-size: clamp(1.45rem, 2.6vw, 2.15rem);
  line-height: 1.05;
  letter-spacing: -.03em;
}

.proof-lab__statement {
  max-width: 74ch;
  margin: 0 auto;
  color: var(--proof-graphite);
  font-family: Georgia, "Times New Roman", serif;
  font-size: clamp(1rem, 1.5vw, 1.16rem);
}

/* ── brief: long-form context, collapsed, below the workspace ─── */

.proof-lab__brief {
  display: grid;
  gap: .4rem;
  max-width: 900px;
  margin: .85rem auto 0;
}

.proof-lab__brief-item {
  border: 1px solid var(--proof-line);
  border-radius: 8px;
  background: #fff;
}

.proof-lab__brief-item > summary {
  padding: .5rem .85rem;
  color: #167b9e;
  font-size: .82rem;
  font-weight: 700;
  cursor: pointer;
  list-style: none;
}

.proof-lab__brief-item > summary::-webkit-details-marker {
  display: none;
}

.proof-lab__brief-item > summary::before {
  content: "\25B8\00a0";
  color: var(--proof-muted);
}

.proof-lab__brief-item[open] > summary::before {
  content: "\25BE\00a0";
}

.proof-lab__brief-item > p {
  margin: 0;
  padding: 0 .95rem .8rem;
  max-width: 78ch;
  color: var(--proof-muted);
  font-size: .86rem;
  line-height: 1.55;
}

/* ================================================================
   WORKSPACE — the interactive card.
   A fixed-height card that fills the viewport.  Three vertical
   zones: topbar → diagram → body.  The body scrolls independently;
   diagram and topbar are pinned.  Content visibility is driven by
   data-phase on the workspace: "context", "question", or "result".
   ================================================================ */

.proof-lab__stage {
  display: flex;
  flex-direction: column;
  align-items: center;
  height: calc(100dvh - 6.5rem);
  min-height: 400px;
}

.proof-lab__workspace {
  display: flex;
  flex-direction: column;
  width: min(100%, 900px);
  flex: 1 1 auto;
  min-height: 0;
  border: 1px solid var(--proof-line);
  border-radius: 12px;
  background: #fff;
  box-shadow: 0 2px 16px rgba(48, 48, 54, .06);
  overflow: hidden;
}

/* ── topbar: progress dots + step label + phase badge ────────── */

.proof-lab__topbar {
  display: flex;
  align-items: center;
  gap: .75rem;
  flex-shrink: 0;
  padding: .55rem 1.25rem;
  border-bottom: 1px solid var(--proof-line);
  background: #fafbfd;
}

.proof-lab__step-label {
  color: var(--proof-tomato);
  font-size: .68rem;
  font-weight: 700;
  letter-spacing: .08em;
  text-transform: uppercase;
  white-space: nowrap;
}

.proof-lab__progress {
  display: flex;
  gap: .35rem;
  flex: 1;
}

.proof-lab__progress span {
  width: 8px;
  height: 8px;
  border-radius: 999px;
  background: var(--proof-line);
  transition: width .2s ease, background-color .2s ease;
}

.proof-lab__progress span.is-done {
  background: var(--proof-teal);
}

.proof-lab__progress span.is-current {
  width: 24px;
  background: var(--proof-tomato);
}

.proof-lab__step-counter {
  color: var(--proof-muted);
  font-size: .72rem;
  font-weight: 600;
  white-space: nowrap;
}

.proof-lab__phase-badge {
  font-size: .6rem;
  font-weight: 700;
  letter-spacing: .06em;
  text-transform: uppercase;
  padding: .12rem .45rem;
  border-radius: 4px;
  white-space: nowrap;
  transition: background .2s ease, color .2s ease;
}

[data-phase="context"] .proof-lab__phase-badge {
  background: var(--proof-sky-soft);
  color: #167b9e;
}

[data-phase="question"] .proof-lab__phase-badge {
  background: var(--proof-amber-soft);
  color: var(--proof-amber);
}

[data-phase="result"] .proof-lab__phase-badge {
  background: var(--proof-teal-soft);
  color: var(--proof-teal);
}

/* ── canvas: diagram ─────────────────────────────────────────── */

.proof-lab__canvas {
  position: relative;
  flex: 0 0 auto;
  height: min(31%, 220px);
  min-height: 146px;
  padding: .4rem .75rem 0;
  border-bottom: 1px solid var(--proof-line);
  background: var(--proof-paper);
  transition: height .3s ease;
}

.proof-lab__diagram {
  display: block;
  width: 100%;
  height: calc(100% - 1.3rem);
  overflow: visible;
}

.proof-lab__canvas-note {
  height: 1.3rem;
  color: var(--proof-muted);
  font-size: .72rem;
  text-align: center;
  line-height: 1.3rem;
  overflow: hidden;
  white-space: nowrap;
  text-overflow: ellipsis;
}

/* ── body: scrollable phase content ──────────────────────────── */

.proof-lab__body {
  flex: 1 1 auto;
  overflow-y: auto;
  min-height: 0;
  padding: 0;
  scrollbar-gutter: stable;
}

.proof-lab__body::-webkit-scrollbar { width: 5px; }
.proof-lab__body::-webkit-scrollbar-thumb {
  background: var(--proof-line);
  border-radius: 3px;
}
.proof-lab__body::-webkit-scrollbar-thumb:hover { background: #b0b0b6; }

/* ── phase visibility ────────────────────────────────────────── */

.proof-lab__phase {
  display: none;
  flex-direction: column;
  min-height: 100%;
  padding: .7rem clamp(.75rem, 2.5vw, 1.5rem) .9rem;
  animation: proofPhaseIn .28s ease both;
}

[data-phase="context"] .proof-lab__phase--context,
[data-phase="question"] .proof-lab__phase--question,
[data-phase="result"]  .proof-lab__phase--result {
  display: flex;
}

@keyframes proofPhaseIn {
  from { opacity: 0; transform: translateY(8px); }
  to   { opacity: 1; transform: translateY(0); }
}

/* ── CONTEXT phase ───────────────────────────────────────────── */

.proof-lab__phase--context h2 {
  margin: 0 0 .4rem;
  color: var(--proof-graphite);
  font-size: clamp(1.1rem, 1.8vw, 1.4rem);
  line-height: 1.2;
}

.proof-lab__exposition {
  margin: 0;
  color: var(--proof-graphite);
  font-size: .88rem;
  line-height: 1.58;
}

/* ── QUESTION phase ──────────────────────────────────────────── */

.proof-lab__question {
  margin: 0 0 .6rem;
  color: var(--proof-graphite);
  font-size: .88rem;
  font-weight: 500;
  line-height: 1.5;
}

.proof-lab__choices {
  display: grid;
  gap: .45rem;
}

.proof-lab__choice {
  border: 1px solid var(--proof-line);
  border-left: 3px solid transparent;
  border-radius: 8px;
  padding: .4rem .6rem;
  background: #fff;
  color: var(--proof-graphite);
  font: inherit;
  font-size: .83rem;
  font-weight: 500;
  line-height: 1.4;
  text-align: left;
  cursor: pointer;
  transition: border-color .15s ease, background .15s ease, border-left-color .15s ease;
}

.proof-lab__choice:hover {
  border-color: var(--proof-sky);
  border-left-color: var(--proof-sky);
  background: var(--proof-sky-soft);
}

.proof-lab__choice:focus-visible {
  outline: 3px solid rgba(48, 188, 237, .42);
  outline-offset: 2px;
}

.proof-lab__hint {
  margin: .5rem 0 0;
  border-left: 3px solid var(--proof-violet);
  padding: .3rem 0 .3rem .65rem;
  color: var(--proof-muted);
  font-size: .82rem;
  line-height: 1.45;
}

/* ── RESULT phase ────────────────────────────────────────────── */

.proof-lab__feedback {
  margin: 0 0 .4rem;
  padding: .5rem .7rem;
  border-radius: 8px;
  font-size: .84rem;
  font-weight: 600;
  line-height: 1.45;
}

.proof-lab__feedback:not(.is-error) {
  background: var(--proof-teal-soft);
  color: var(--proof-teal);
  border-left: 3px solid var(--proof-teal);
}

.proof-lab__feedback.is-error {
  background: #fef0ed;
  color: #ae371f;
  border-left: 3px solid var(--proof-tomato);
}

.proof-lab__formal {
  margin-top: .5rem;
  border-top: 1px solid var(--proof-line);
  padding-top: .4rem;
}

.proof-lab__formal summary {
  color: #167b9e;
  font-size: .8rem;
  font-weight: 700;
  cursor: pointer;
}

.proof-lab__formal p {
  margin: .35rem 0 0;
  color: var(--proof-muted);
  font-size: .82rem;
}

.proof-lab__invariant {
  margin-top: .4rem;
  border-left: 3px solid var(--proof-teal);
  padding: .25rem 0 .25rem .6rem;
  font-size: .76rem;
  line-height: 1.4;
  color: var(--proof-graphite);
}

.proof-lab__invariant strong {
  display: block;
  margin-bottom: .1rem;
  color: var(--proof-teal);
  font-size: .62rem;
  letter-spacing: .07em;
  text-transform: uppercase;
}

/* ── actions bar (bottom of each phase) ──────────────────────── */

.proof-lab__actions {
  display: flex;
  flex-wrap: wrap;
  gap: .45rem;
  margin-top: auto;
  padding-top: .75rem;
}

.proof-lab__button {
  border: 1px solid var(--proof-line);
  border-radius: 8px;
  padding: .42rem .75rem;
  background: #fff;
  color: var(--proof-graphite);
  font: inherit;
  font-size: .82rem;
  font-weight: 600;
  text-align: center;
  cursor: pointer;
  transition: border-color .15s ease, background .15s ease;
}

.proof-lab__button:hover {
  border-color: var(--proof-sky);
  background: var(--proof-sky-soft);
}

.proof-lab__button:focus-visible {
  outline: 3px solid rgba(48, 188, 237, .42);
  outline-offset: 2px;
}

.proof-lab__button--primary {
  margin-left: auto;
  border-color: #167b9e;
  background: var(--proof-sky);
  color: #fff;
}

.proof-lab__button--primary:hover {
  background: #28a8d8;
}

.proof-lab__button--back {
  color: var(--proof-muted);
  font-weight: 500;
}

.proof-lab__button[disabled] {
  cursor: not-allowed;
  opacity: .38;
}

.proof-lab__button[hidden] {
  display: none;
}

/* ── elements below the workspace ──────────────────────────── */

.proof-lab__synthesis {
  max-width: 940px;
  margin: clamp(2.5rem, 6vw, 5rem) auto 0;
  border-top: 1px solid var(--proof-line);
  border-bottom: 1px solid var(--proof-line);
  padding: 1rem 0;
}

.proof-lab__synthesis summary {
  color: #167b9e;
  font-weight: 700;
  cursor: pointer;
}

.proof-lab__synthesis p {
  max-width: 82ch;
  margin: .9rem 0 0;
  color: var(--proof-graphite);
  font-family: Georgia, "Times New Roman", serif;
  line-height: 1.7;
}

.proof-lab__nav {
  display: flex;
  justify-content: space-between;
  gap: 1rem;
  margin-top: clamp(2.5rem, 6vw, 5rem);
  border-top: 1px solid var(--proof-line);
  padding-top: 1rem;
}

.proof-lab__nav a {
  color: #167b9e;
  font-weight: 700;
  text-decoration: none;
}

.proof-lab__nav a:focus-visible {
  outline: 3px solid rgba(48, 188, 237, .42);
  outline-offset: 2px;
}

.proof-lab__nav a:last-child {
  margin-left: auto;
  text-align: right;
}

/* ── SVG diagram internals ──────────────────────────────────── */

.proof-lab__lane {
  stroke: var(--proof-line);
  stroke-width: 1;
}

.proof-lab__lane-label,
.proof-lab__edge-label,
.proof-lab__annotation {
  fill: var(--proof-muted);
  font-family: "Cabin", sans-serif;
}

.proof-lab__lane-label {
  font-size: 14px;
  font-weight: 700;
  letter-spacing: .08em;
  text-transform: uppercase;
}

.proof-lab__edge {
  fill: none;
  stroke: #a0a0a7;
  stroke-width: 2.2;
  transition: stroke .2s ease, stroke-width .2s ease, opacity .2s ease;
}

.proof-lab__edge.is-active {
  stroke: var(--proof-tomato);
  stroke-width: 4;
}

.proof-lab__edge.is-dim {
  opacity: .22;
}

.proof-lab__edge-label {
  font-size: 13px;
  font-weight: 700;
  paint-order: stroke;
  stroke: var(--proof-paper);
  stroke-width: 5px;
}

.proof-lab__node-shape {
  fill: #fff;
  stroke: #9999a1;
  stroke-width: 2.2;
  transition: fill .2s ease, stroke .2s ease, stroke-width .2s ease, opacity .2s ease;
}

.proof-lab__node.is-active .proof-lab__node-shape {
  fill: var(--proof-sky-soft);
  stroke: #167b9e;
  stroke-width: 4;
}

.proof-lab__node.is-good .proof-lab__node-shape {
  fill: var(--proof-teal-soft);
  stroke: var(--proof-teal);
}

.proof-lab__node.is-bad .proof-lab__node-shape {
  fill: #fee8e3;
  stroke: var(--proof-tomato);
}

.proof-lab__node.is-dim {
  opacity: .28;
}

.proof-lab__node.is-accepting .proof-lab__node-shape {
  stroke-width: 4;
}

.proof-lab__node-text,
.proof-lab__node-detail {
  fill: var(--proof-graphite);
  font-family: "Cabin", sans-serif;
  text-anchor: middle;
}

.proof-lab__node-text {
  font-size: 16px;
  font-weight: 700;
}

.proof-lab__node-detail {
  fill: var(--proof-muted);
  font-size: 12px;
}

/* ── proof-lab index page ───────────────────────────────────── */

.proof-lab-index {
  max-width: 1180px;
  margin: 0 auto;
}

.proof-lab-index__chapter {
  margin-top: 2.25rem;
}

.proof-lab-index__grid {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(245px, 1fr));
  gap: .8rem;
}

.proof-lab-index__card {
  display: block;
  border: 1px solid var(--proof-line);
  border-left: 4px solid var(--proof-sky);
  border-radius: 8px;
  padding: 1rem;
  background: #fff;
  color: var(--proof-graphite);
  text-decoration: none;
}

.proof-lab-index__card:hover {
  border-color: var(--proof-sky);
  color: var(--proof-graphite);
  text-decoration: none;
}

.proof-lab-index__card small {
  color: var(--proof-tomato);
  font-weight: 700;
  letter-spacing: .06em;
  text-transform: uppercase;
}

.proof-lab-index__card strong {
  display: block;
  margin: .35rem 0;
}

.proof-lab-index__card span {
  color: var(--proof-muted);
  font-size: .9rem;
}

/* ── responsive ─────────────────────────────────────────────── */

@media (max-width: 560px) {
  .proof-lab__header {
    margin-bottom: .5rem;
  }

  .proof-lab__stage {
    height: calc(100dvh - 4rem);
    align-items: stretch;
  }

  .proof-lab__workspace {
    width: auto;
    border-radius: 0;
    border-left: 0;
    border-right: 0;
    margin-inline: calc(-1 * clamp(.75rem, 2.4vw, 2.5rem));
  }

  .proof-lab__canvas {
    min-height: 132px;
  }

  .proof-lab__nav {
    align-items: flex-start;
    flex-direction: column;
  }

  .proof-lab__nav a:last-child {
    margin-left: 0;
    text-align: left;
  }
}

@media (prefers-reduced-motion: reduce) {
  .proof-lab *,
  .proof-lab *::before,
  .proof-lab *::after {
    scroll-behavior: auto !important;
    transition-duration: .001ms !important;
    animation-duration: .001ms !important;
  }
}

@media print {
  .proof-lab__stage {
    display: block;
    height: auto;
  }

  .proof-lab__workspace {
    display: block;
    height: auto;
    box-shadow: none;
    border: 0;
  }

  .proof-lab__canvas {
    height: auto;
    border: 0;
    padding: 0;
  }

  .proof-lab__body { overflow: visible; }

  .proof-lab__phase { display: flex !important; }

  .proof-lab__choices,
  .proof-lab__actions,
  .proof-lab__topbar { display: none; }
}