:root {
  color-scheme: light;
  --paper: #f5f2e9;
  --paper-deep: #e9e3d3;
  --white: #fffdf7;
  --ink: #17211d;
  --muted: #59635e;
  --forest: #0b5748;
  --forest-dark: #073e35;
  --teal: #187a74;
  --red: #c44f3d;
  --red-dark: #913629;
  --red-soft: rgba(196, 79, 61, 0.13);
  --blue: #286b9d;
  --blue-dark: #1d4f76;
  --blue-soft: rgba(40, 107, 157, 0.13);
  --gold: #d29a4a;
  --hairline: rgba(23, 33, 29, 0.18);
  --shadow: 0 22px 60px rgba(21, 42, 34, 0.1);
  --serif: "Newsreader", Georgia, "Times New Roman", serif;
  --sans:
    "IBM Plex Sans", Inter, system-ui, -apple-system, BlinkMacSystemFont,
    "Segoe UI", sans-serif;
  --mono: "IBM Plex Mono", "SFMono-Regular", Consolas, monospace;
}

* {
  box-sizing: border-box;
}

html {
  min-width: 320px;
  background: var(--paper);
}

body {
  margin: 0;
  background:
    radial-gradient(
      circle at 92% 2%,
      rgba(24, 122, 116, 0.1),
      transparent 24rem
    ),
    var(--paper);
  color: var(--ink);
  font-family: var(--sans);
  line-height: 1.55;
  text-rendering: optimizeLegibility;
}

button,
input {
  font: inherit;
}

.sr-only {
  position: absolute;
  width: 1px;
  height: 1px;
  padding: 0;
  overflow: hidden;
  clip: rect(0, 0, 0, 0);
  white-space: nowrap;
  border: 0;
}

.math {
  font-family: Georgia, "Times New Roman", serif;
}

.demo-shell {
  width: min(1280px, calc(100% - 32px));
  margin: 0 auto;
  padding: clamp(30px, 5vw, 72px) 0 34px;
}

.demo-header {
  display: grid;
  grid-template-columns: minmax(0, 1.15fr) minmax(280px, 0.7fr);
  align-items: end;
  gap: clamp(30px, 7vw, 96px);
  padding: 0 clamp(2px, 1vw, 12px) clamp(32px, 5vw, 58px);
}

.eyebrow,
.section-label {
  margin: 0 0 12px;
  color: var(--forest);
  font-family: var(--mono);
  font-size: 0.7rem;
  font-weight: 650;
  letter-spacing: 0.12em;
  line-height: 1.4;
  text-transform: uppercase;
}

.demo-header h1 {
  max-width: 820px;
  margin: 0;
  font-family: var(--serif);
  font-size: clamp(2.75rem, 6vw, 5.6rem);
  font-weight: 430;
  letter-spacing: -0.052em;
  line-height: 0.96;
}

.intro {
  max-width: 500px;
  margin: 0 0 0.35rem;
  color: var(--muted);
  font-size: clamp(1rem, 1.5vw, 1.16rem);
}

.lemma-rail {
  display: grid;
  grid-template-columns: minmax(0, 1fr) 34px minmax(0, 1fr) 34px minmax(0, 1fr);
  align-items: stretch;
  gap: 0.75rem;
  margin-bottom: 20px;
}

.lemma-rail article {
  min-width: 0;
  padding: 1.25rem 1.3rem 1.35rem;
  border: 1px solid var(--hairline);
  border-radius: 18px;
  background: rgba(255, 253, 247, 0.72);
}

.lemma-rail article > span {
  color: var(--forest);
  font-family: var(--mono);
  font-size: 0.64rem;
  font-weight: 650;
  letter-spacing: 0.08em;
  text-transform: uppercase;
}

.lemma-rail article > strong {
  display: block;
  margin-top: 0.7rem;
  font-family: var(--serif);
  font-size: 1.12rem;
  font-weight: 520;
  line-height: 1.25;
}

.lemma-rail article > p {
  margin: 0.45rem 0 0;
  color: var(--muted);
  font-size: 0.78rem;
}

.lemma-rail .rail-final {
  border-color: rgba(11, 87, 72, 0.34);
  background: rgba(24, 122, 116, 0.06);
}

.rail-arrow {
  align-self: center;
  color: var(--gold);
  font-family: var(--serif);
  font-size: 1.8rem;
  font-style: normal;
  text-align: center;
}

.control-panel {
  overflow: hidden;
  border: 1px solid rgba(255, 253, 247, 0.16);
  border-radius: 20px;
  background:
    linear-gradient(rgba(255, 255, 255, 0.025) 1px, transparent 1px),
    linear-gradient(90deg, rgba(255, 255, 255, 0.025) 1px, transparent 1px),
    var(--forest);
  background-size: 36px 36px;
  box-shadow: var(--shadow);
  color: var(--white);
}

.control-heading {
  padding: 23px clamp(22px, 4vw, 46px) 18px;
  border-bottom: 1px solid rgba(255, 253, 247, 0.15);
}

.control-heading .section-label {
  margin-bottom: 5px;
  color: #a9d7cc;
}

.control-note {
  margin: 0;
  color: rgba(255, 253, 247, 0.74);
  font-size: 0.9rem;
}

.state-controls {
  display: grid;
  grid-template-columns: repeat(4, minmax(0, 1fr));
  margin: 0;
  padding: 0;
  border: 0;
}

.state-option {
  position: relative;
  display: block;
  min-width: 0;
  cursor: pointer;
}

.state-option + .state-option {
  border-left: 1px solid rgba(255, 253, 247, 0.15);
}

.state-option input {
  position: absolute;
  width: 1px;
  height: 1px;
  opacity: 0;
}

.state-option > span {
  position: relative;
  display: grid;
  min-height: 92px;
  gap: 0.3rem;
  align-content: center;
  padding: 18px clamp(16px, 2.6vw, 30px);
  background: rgba(255, 253, 247, 0.025);
  transition:
    background 160ms ease,
    box-shadow 160ms ease;
}

.state-option > span::after {
  position: absolute;
  right: 18px;
  bottom: 14px;
  width: 9px;
  height: 9px;
  border: 1px solid rgba(255, 253, 247, 0.5);
  border-radius: 50%;
  content: "";
}

.state-option:hover > span {
  background: rgba(255, 253, 247, 0.08);
}

.state-option input:focus-visible + span {
  outline: 3px solid #efb56e;
  outline-offset: -4px;
}

.state-option input:checked + span {
  background: rgba(255, 253, 247, 0.13);
  box-shadow: inset 0 -4px 0 #efb56e;
}

.state-option input:checked + span::after {
  border-color: #efb56e;
  background: #efb56e;
  box-shadow: 0 0 0 3px rgba(239, 181, 110, 0.18);
}

.state-option-red input:checked + span {
  box-shadow: inset 0 -4px 0 #f17d6b;
}

.state-option-red input:checked + span::after {
  border-color: #f17d6b;
  background: #f17d6b;
}

.state-option-blue input:checked + span {
  box-shadow: inset 0 -4px 0 #79b7e3;
}

.state-option-blue input:checked + span::after {
  border-color: #79b7e3;
  background: #79b7e3;
}

.state-option small,
.state-option strong {
  display: block;
  min-width: 0;
}

.state-option small {
  color: rgba(255, 253, 247, 0.57);
  font-family: var(--mono);
  font-size: 0.58rem;
  letter-spacing: 0.07em;
  text-transform: uppercase;
}

.state-option strong {
  padding-right: 18px;
  color: var(--white);
  font-family: var(--serif);
  font-size: clamp(1rem, 1.7vw, 1.25rem);
  font-weight: 520;
  line-height: 1.15;
}

.visual-layout {
  display: grid;
  grid-template-columns: minmax(0, 1.62fr) minmax(300px, 0.72fr);
  gap: 18px;
  margin-top: 18px;
}

.graph-card,
.count-card {
  min-width: 0;
  margin: 0;
  border: 1px solid var(--hairline);
  border-radius: 20px;
  background: rgba(255, 253, 247, 0.78);
  box-shadow: var(--shadow);
}

.graph-card {
  padding: clamp(24px, 3.5vw, 42px);
}

.graph-card figcaption {
  display: grid;
  grid-template-columns: minmax(0, 1fr) minmax(220px, 0.62fr);
  align-items: end;
  gap: 24px;
}

.graph-card h2,
.count-card h2,
.witness-copy h2 {
  margin: 0;
  font-family: var(--serif);
  font-size: clamp(1.75rem, 2.8vw, 2.55rem);
  font-weight: 470;
  letter-spacing: -0.03em;
  line-height: 1.08;
}

.graph-card figcaption > p {
  margin: 0 0 0.2rem;
  color: var(--muted);
  font-size: 0.86rem;
}

.graph-wrap {
  margin-top: 24px;
  overflow: hidden;
  border: 1px solid rgba(23, 33, 29, 0.1);
  border-radius: 16px;
  background:
    linear-gradient(rgba(23, 33, 29, 0.03) 1px, transparent 1px),
    linear-gradient(90deg, rgba(23, 33, 29, 0.03) 1px, transparent 1px),
    rgba(235, 230, 216, 0.36);
  background-size: 34px 34px;
}

.graph {
  display: block;
  width: 100%;
  aspect-ratio: 760 / 560;
}

.graph-edge {
  fill: none;
  stroke-linecap: round;
  stroke-width: 4;
  transition:
    opacity 180ms ease,
    stroke-width 180ms ease;
  vector-effect: non-scaling-stroke;
}

.edge-red {
  stroke: var(--red);
}

.edge-blue {
  stroke: var(--blue);
}

.clone-edge {
  stroke-width: 5;
}

.final-edge {
  stroke-width: 8;
}

.edge-missing {
  stroke: #6b756f;
  stroke-dasharray: 10 8;
  stroke-width: 3;
}

.graph.is-resolved .graph-edge:not(.is-witness) {
  opacity: 0.14;
}

.graph.is-resolved .graph-edge.is-witness {
  stroke-width: 7;
  filter: drop-shadow(0 0 5px rgba(255, 253, 247, 0.9));
}

.graph.is-resolved .final-edge.is-witness {
  stroke-width: 10;
}

.triangle-area {
  stroke-width: 2;
  vector-effect: non-scaling-stroke;
}

.triangle-area-red {
  fill: rgba(196, 79, 61, 0.17);
  stroke: rgba(145, 54, 41, 0.58);
}

.triangle-area-blue {
  fill: rgba(40, 107, 157, 0.15);
  stroke: rgba(29, 79, 118, 0.58);
}

.node circle {
  fill: var(--forest-dark);
  stroke: var(--white);
  stroke-width: 3;
  vector-effect: non-scaling-stroke;
}

.node text {
  fill: var(--white);
  font-family: var(--serif);
  font-size: 20px;
  font-weight: 650;
  pointer-events: none;
  text-anchor: middle;
}

.node-clone circle {
  fill: var(--gold);
  stroke: #fff8e8;
  stroke-width: 4;
}

.graph.is-resolved .node:not(.is-active) {
  opacity: 0.18;
}

.graph.is-resolved .node.is-active circle {
  filter: drop-shadow(0 0 8px rgba(210, 154, 74, 0.6));
}

.edge-label,
.clone-note {
  font-family: var(--mono);
  pointer-events: none;
  text-anchor: middle;
}

.edge-label {
  fill: #5c6661;
  font-size: 12px;
  font-weight: 650;
}

.edge-label-red {
  fill: var(--red-dark);
}

.edge-label-blue {
  fill: var(--blue-dark);
}

.clone-note {
  fill: #7b5c29;
  font-size: 10px;
  letter-spacing: 0.04em;
  text-transform: uppercase;
}

.graph-key {
  display: flex;
  flex-wrap: wrap;
  gap: 12px 20px;
  margin-top: 18px;
  color: var(--muted);
  font-family: var(--mono);
  font-size: 0.64rem;
  letter-spacing: 0.05em;
  text-transform: uppercase;
}

.graph-key span {
  display: inline-flex;
  align-items: center;
  gap: 8px;
}

.key-line {
  display: inline-block;
  width: 24px;
  height: 0;
  border-top: 3px solid;
}

.key-red {
  border-color: var(--red);
}

.key-blue {
  border-color: var(--blue);
}

.key-missing {
  border-color: #6b756f;
  border-top-style: dashed;
}

.key-node {
  display: inline-block;
  width: 12px;
  height: 12px;
  border: 2px solid var(--white);
  border-radius: 50%;
  box-shadow: 0 0 0 1px rgba(23, 33, 29, 0.28);
}

.key-clone {
  background: var(--gold);
}

.count-card {
  display: flex;
  flex-direction: column;
  padding: clamp(24px, 3.5vw, 40px);
}

.count-card h2 {
  max-width: 380px;
}

.triangle-total {
  display: grid;
  grid-template-columns: auto minmax(0, 1fr);
  align-items: end;
  gap: 14px;
  margin-top: 26px;
  padding: 20px 0;
  border-top: 1px solid var(--hairline);
  border-bottom: 1px solid var(--hairline);
}

.triangle-total strong {
  color: var(--forest);
  font-family: var(--serif);
  font-size: clamp(4rem, 8vw, 6.3rem);
  font-weight: 470;
  letter-spacing: -0.06em;
  line-height: 0.78;
}

.triangle-total span {
  max-width: 150px;
  padding-bottom: 0.25rem;
  color: var(--muted);
  font-size: 0.72rem;
  line-height: 1.35;
}

.triangle-total.is-red strong {
  color: var(--red-dark);
}

.triangle-total.is-blue strong {
  color: var(--blue-dark);
}

.equivalence {
  display: grid;
  grid-template-columns: 1fr auto 1fr;
  align-items: center;
  gap: 12px;
  margin-top: 18px;
  padding: 17px 0;
  border-bottom: 1px solid var(--hairline);
}

.equivalence > span {
  min-width: 0;
}

.equivalence strong,
.equivalence small {
  display: block;
}

.equivalence strong {
  color: var(--forest);
  font-family: var(--serif);
  font-size: clamp(2rem, 4vw, 3rem);
  font-weight: 480;
  letter-spacing: -0.04em;
  line-height: 0.95;
}

.equivalence.is-red strong {
  color: var(--red-dark);
}

.equivalence.is-blue strong {
  color: var(--blue-dark);
}

.equivalence small {
  margin-top: 7px;
  color: var(--muted);
  font-size: 0.66rem;
  line-height: 1.35;
}

.equivalence > i {
  color: var(--gold);
  font-family: var(--serif);
  font-size: 1.5rem;
  font-style: normal;
}

.formula-card {
  margin-top: 18px;
  padding: 16px;
  border-radius: 13px;
  background: var(--paper-deep);
  text-align: center;
}

.formula-card.is-red {
  background: var(--red-soft);
}

.formula-card.is-blue {
  background: var(--blue-soft);
}

.formula-card p {
  margin: 0;
  font-size: clamp(1.05rem, 1.8vw, 1.35rem);
}

.formula-card small {
  display: block;
  margin-top: 5px;
  color: var(--muted);
  font-size: 0.69rem;
}

.status-box {
  display: grid;
  gap: 4px;
  margin-top: auto;
  padding: 18px;
  border: 1px solid rgba(11, 87, 72, 0.23);
  border-radius: 13px;
  background: rgba(24, 122, 116, 0.06);
}

.status-box.is-red {
  border-color: rgba(196, 79, 61, 0.3);
  background: var(--red-soft);
}

.status-box.is-blue {
  border-color: rgba(40, 107, 157, 0.3);
  background: var(--blue-soft);
}

.status-box strong {
  font-family: var(--serif);
  font-size: 1.08rem;
  font-weight: 560;
}

.status-box span {
  color: var(--muted);
  font-size: 0.75rem;
}

.color-word-red {
  color: var(--red-dark);
}

.color-word-blue {
  color: var(--blue-dark);
}

.witness-section {
  display: grid;
  grid-template-columns: minmax(250px, 0.62fr) minmax(0, 1fr);
  gap: clamp(28px, 5vw, 68px);
  align-items: start;
  margin-top: 18px;
  padding: clamp(28px, 4vw, 48px);
  border: 1px solid var(--hairline);
  border-radius: 20px;
  background: rgba(255, 253, 247, 0.72);
}

.witness-copy p:last-child {
  margin: 1rem 0 0;
  color: var(--muted);
  font-size: 0.86rem;
}

.witness-list {
  display: grid;
  grid-template-columns: repeat(2, minmax(0, 1fr));
  gap: 14px;
}

.witness-card {
  min-width: 0;
  padding: 22px;
  border: 1px solid var(--hairline);
  border-radius: 14px;
  background: rgba(255, 253, 247, 0.72);
}

.witness-card-red {
  border-top: 4px solid var(--red);
}

.witness-card-blue {
  border-top: 4px solid var(--blue);
}

.witness-card > span {
  color: var(--muted);
  font-family: var(--mono);
  font-size: 0.61rem;
  letter-spacing: 0.07em;
  text-transform: uppercase;
}

.witness-card > strong {
  display: block;
  margin-top: 0.55rem;
  overflow-wrap: anywhere;
  font-family: var(--serif);
  font-size: clamp(1.15rem, 2vw, 1.5rem);
  font-weight: 520;
  line-height: 1.2;
}

.witness-card > p {
  margin: 0.65rem 0 0;
  color: var(--muted);
  font-size: 0.75rem;
}

.demo-footer {
  display: grid;
  grid-template-columns: minmax(0, 0.8fr) minmax(0, 1.2fr);
  gap: 40px;
  padding: 26px 8px 0;
  color: var(--muted);
  font-size: 0.78rem;
}

.demo-footer p {
  margin: 0;
}

.general-formula {
  text-align: right;
}

.is-embedded body {
  background: transparent;
}

.is-embedded .demo-shell {
  width: min(1280px, calc(100% - 18px));
  padding-top: 24px;
}

@media (max-width: 1040px) {
  .state-option > span {
    padding-right: 18px;
    padding-left: 18px;
  }

  .visual-layout {
    grid-template-columns: minmax(0, 1.35fr) minmax(285px, 0.65fr);
  }
}

@media (max-width: 900px) {
  .demo-header {
    grid-template-columns: 1fr;
    gap: 22px;
  }

  .intro {
    max-width: 720px;
  }

  .state-controls {
    grid-template-columns: repeat(2, minmax(0, 1fr));
  }

  .state-option:nth-of-type(3) {
    border-top: 1px solid rgba(255, 253, 247, 0.15);
    border-left: 0;
  }

  .state-option:nth-of-type(4) {
    border-top: 1px solid rgba(255, 253, 247, 0.15);
  }

  .visual-layout {
    grid-template-columns: 1fr;
  }

  .count-card {
    display: grid;
    grid-template-columns: minmax(180px, 0.75fr) minmax(220px, 1fr);
    gap: 0 28px;
  }

  .count-card > .section-label,
  .count-card > h2,
  .triangle-total {
    grid-column: 1;
  }

  .equivalence,
  .formula-card,
  .status-box {
    grid-column: 2;
  }

  .equivalence {
    grid-row: 1 / span 3;
    align-self: end;
    margin-top: 0;
    border-top: 1px solid var(--hairline);
  }

  .formula-card {
    grid-row: 4;
  }

  .status-box {
    grid-row: 5;
    margin-top: 14px;
  }

  .witness-section {
    grid-template-columns: 1fr;
    gap: 24px;
  }
}

@media (max-width: 720px) {
  .demo-shell,
  .is-embedded .demo-shell {
    width: min(100% - 14px, 1280px);
    padding-top: 22px;
  }

  .demo-header {
    padding-right: 9px;
    padding-left: 9px;
  }

  .demo-header h1 {
    font-size: clamp(2.55rem, 13vw, 4rem);
  }

  .lemma-rail {
    grid-template-columns: 1fr;
    gap: 0.65rem;
  }

  .rail-arrow {
    height: 18px;
    line-height: 18px;
    transform: rotate(90deg);
  }

  .graph-card figcaption {
    grid-template-columns: 1fr;
    gap: 14px;
  }

  .count-card {
    display: flex;
  }

  .equivalence,
  .formula-card,
  .status-box {
    margin-top: 18px;
  }

  .witness-list {
    grid-template-columns: 1fr;
  }

  .demo-footer {
    grid-template-columns: 1fr;
    gap: 16px;
  }

  .general-formula {
    text-align: left;
  }
}

@media (max-width: 480px) {
  .state-controls {
    grid-template-columns: 1fr;
  }

  .state-option + .state-option,
  .state-option:nth-of-type(3),
  .state-option:nth-of-type(4) {
    border-top: 1px solid rgba(255, 253, 247, 0.15);
    border-left: 0;
  }

  .state-option > span {
    min-height: 76px;
  }

  .graph-card,
  .count-card,
  .witness-section {
    padding: 20px;
  }

  .graph-wrap {
    margin-right: -8px;
    margin-left: -8px;
  }

  .graph-key {
    display: grid;
    grid-template-columns: repeat(2, minmax(0, 1fr));
  }

  .edge-label {
    font-size: 10px;
  }
}

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