/* ============================================================
   ch25「形式化方法与程序验证」章节专属样式
   境界：化神三层·形式证道 · 证道靛 #3730A3
   Boss：状态爆炸之雾 · 雾灰 #9CA3AF
   顿悟：突破金 var(--ch-epiphany)（理解发生之处/金光裂纹/顿悟脉冲）
   点缀：证明金 var(--ch-epiphany)（ch25专属点缀色）
   背景：暖深蓝灰 var(--ch-bg-warm)（禁止纯黑）
   全部色值走 tokens 变量；玻璃态卡片；发光仅限边框/背景。
   ============================================================ */

/* ---------- 章节境界色覆写：证道靛 ---------- */
:root, :root[data-theme="light"] {
  --accent: #3730A3;
  --accent-ink: #312E81;
  --accent-soft: rgba(55, 48, 163, 0.12);
  --glass-line: rgba(55, 48, 163, 0.22);
  --glow: 0 0 18px rgba(55, 48, 163, 0.28);
  --on-accent: #FFFFFF;
  --r-xs: 4px;
}
:root[data-theme="dark"] {
  --accent: #6366F1;
  --accent-ink: #818CF8;
  --accent-soft: rgba(99, 102, 241, 0.16);
  --glass-line: rgba(129, 140, 248, 0.22);
  --glow: 0 0 22px rgba(99, 102, 241, 0.34);
  --on-accent: #FFFFFF;
  --r-xs: 4px;
}

/* ---------- 章节专用叙事色 ---------- */
:root {
  --ch-boss: #9CA3AF;          /* 状态爆炸之雾 · 雾灰 */
  --ch-boss-ink: #6B7280;
  --ch-boss-soft: rgba(156, 163, 175, 0.18);
  --ch-boss-line: rgba(156, 163, 175, 0.38);
  --ch-epiphany: var(--ch-epiphany);      /* 顿悟突破金（理解发生之处） */
  --ch-epiphany-soft: rgba(251, 191, 36, 0.16);
  --ch-epiphany-ink: #D97706;
  --ch-indigo: #4F46E5;        /* 证明靛蓝 */
  --ch-indigo-soft: rgba(79, 70, 229, 0.14);
  --ch-indigo-ink: #3730A3;
  /* 场景功能色 */
  --logic-stone: #4F46E5;      /* 逻辑基石靛蓝 */
  --state-node: #6366F1;       /* 状态节点靛蓝 */
  --state-edge: rgba(99, 102, 241, 0.4);
  --state-explored: #10B981;   /* 已探索翠绿 */
  --state-violation: var(--ch-boss);  /* 违反性质红 */
  --ltl-color: #4F46E5;        /* LTL线性时间靛蓝 */
  --ctl-color: #06B6D4;        /* CTL分支时间青 */
  --op-next: var(--ch-epiphany);          /* X 下一个金 */
  --op-future: #10B981;        /* F 最终翠绿 */
  --op-global: #06B6D4;        /* G 总是青 */
  --op-until: #A855F7;         /* U 直到紫 */
  --op-all: #4F46E5;           /* A 所有路径靛蓝 */
  --op-exists: var(--ch-amber);        /* E 存在路径琥珀 */
  --spin-silver: #C0C0C0;      /* SPIN银 */
  --nusmv-indigo: #4F46E5;     /* NuSMV靛 */
  --verify-pass: #10B981;      /* 验证通过翠绿 */
  --verify-fail: var(--ch-boss);      /* 验证失败红 */
  --explosion-curve: var(--ch-boss);  /* 2^n爆炸曲线赤红 */
  --linear-curve: #06B6D4;     /* 线性参考曲线青 */
  --mitigation-bdd: #10B981;   /* BDD缓解翠绿 */
  --mitigation-abs: #06B6D4;   /* 抽象精化青 */
  --mitigation-por: #A855F7;   /* 偏序归约紫 */
  --mitigation-sat: var(--ch-epiphany);   /* SAT缓解金 */
  --proof-chain: var(--ch-epiphany);      /* 证明金链 */
  --proof-crack: #9CA3AF;      /* 证明断裂碎片灰 */
  --hoare-triple: #4F46E5;     /* Hoare三元组靛蓝 */
  --invariant: #10B981;        /* 不变式翠绿 */
  --precondition: #06B6D4;     /* 前置条件青 */
  --postcondition: #A855F7;    /* 后置条件紫 */
  --curry-gold: var(--ch-epiphany);       /* Curry-Howard金 */
  --proposition: #4F46E5;      /* 命题靛蓝 */
  --type: #06B6D4;             /* 类型青 */
  --halting-ring: #9CA3AF;     /* 停机自指环灰 */
  --halting-break: var(--ch-boss);    /* 矛盾断裂红 */
  --scar-crack: var(--ch-boss);       /* 证明之伤裂缝红 */
  --scar-healed: var(--ch-epiphany);      /* 证明之伤愈合金纹 */
  /* S9 Boss */
  --fog-body: #9CA3AF;         /* 雾脸灰白 */
  --fog-glow: rgba(156, 163, 175, 0.4);
  --fog-thick: rgba(156, 163, 175, 0.85);
  --gold-crack: var(--ch-epiphany);       /* 金光裂纹 */
  --scar-projection: #3730A3;  /* 刻痕投影深靛蓝 */
  --mentor-hint: #8B5CF6;      /* 老祖救场紫光 */
  --answer-correct: #10B981;   /* 正解翠绿 */
  --answer-wrong: var(--ch-boss);     /* 错答红 */
  --answer-eliminated: #4B5563;/* 被刻痕划去的选项灰 */
  --breakthrough: #FBBF24;     /* 突破金光 */
  /* 选项/状态色 */
  --opt-correct: #22C55E;
  --opt-wrong: var(--ch-boss);
  --opt-excluded: #4B5563;
  --case-passed: #10B981;      /* 案卷"测试通过"翠绿 */
  --case-bug: var(--ch-boss);         /* 案卷隐藏bug赤红 */
  --ch-ok: #22C55E;
  --ch-warn: var(--ch-boss);
  --ch-bg-warm: var(--ch-bg-warm);       /* 暖深蓝灰背景 */
}

/* ---------- 开场（opening） ---------- */
#opening {
  position: relative; z-index: 2;
  min-height: 100vh; min-height: 100dvh;
  display: flex; flex-direction: column; align-items: center; justify-content: center;
  gap: var(--sp-5); text-align: center;
  padding: calc(var(--nav-h) + var(--sp-6)) var(--sp-4) var(--sp-7);
  background: radial-gradient(ellipse at center, var(--bg-sunk) 0%, var(--ch-bg-warm) 70%);
}
.op-title span {
  display: inline-block; opacity: 0;
  text-shadow: 0 0 60px var(--accent-soft), 0 0 24px var(--ch-indigo-soft);
}
.inv-crack {
  display: inline-block; margin-left: var(--sp-1);
  font-size: 0.65rem; color: var(--ch-epiphany);
  background: rgba(251,191,36,0.14); padding: 0 4px; border-radius: 3px;
}
#scar-panel, #wound-panel {
  position: absolute; right: 0; bottom: calc(100% + var(--sp-1));
  width: 280px; padding: var(--sp-3); z-index: 85;
}
#scar-panel h3, #wound-panel h3 { font-size: 0.9rem; margin-bottom: var(--sp-2); color: var(--ch-epiphany-ink); }
#scar-list p { font-size: 0.8rem; color: var(--ch-indigo); margin: var(--sp-1) 0; }
#wound-list p { font-size: 0.8rem; color: var(--scar-crack); margin: var(--sp-1) 0; }
.option.excluded { opacity: 0.3; cursor: default; transform: none; text-decoration: line-through; border-color: var(--opt-excluded); background: rgba(75,85,99,0.16); }
.sim-range, input[type="range"], .knob-range, select { accent-color: var(--accent); }
.btn-warn { border-color: var(--ch-warn); color: var(--ch-warn); }
.btn-warn:hover { background: rgba(239,68,68,0.12); }

/* ============================================================
   S0 测试vs验证反直觉挑战器 · 雾锁证道门
   ============================================================ */
.cmp-case-bet { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.bet-question {
  text-align: center; font-size: 1rem; color: var(--accent-ink);
  padding: var(--sp-2); letter-spacing: 0.08em;
}
.case-gallery {
  display: grid; grid-template-columns: repeat(5, 1fr); gap: var(--sp-2);
  padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-sunk);
}
.case-card {
  padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; text-align: center;
  transition: all 300ms cubic-bezier(0.22,1,0.36,1); min-height: 110px;
  display: flex; flex-direction: column; align-items: center; justify-content: center; gap: 4px;
  opacity: 0.7;
}
.case-card:hover { border-color: var(--case-bug); opacity: 1; transform: translateY(-2px); }
.case-card.revealed { border-color: var(--case-bug); background: rgba(239,68,68,0.08); opacity: 1; }
.case-card .cc-name { font-family: var(--font-mono); font-size: 0.78rem; font-weight: 600; color: var(--text-1); }
.case-card .cc-domain { font-size: 0.66rem; color: var(--text-3); }
.case-card .cc-status { font-size: 0.66rem; color: var(--case-passed); border: 1px solid var(--case-passed); border-radius: 3px; padding: 0 4px; }
.case-card.revealed .cc-status { color: var(--case-bug); border-color: var(--case-bug); text-decoration: line-through; }
.bet-opts { display: grid; grid-template-columns: repeat(3, 1fr); gap: var(--sp-2); }
.bet-opt {
  padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-size: 0.85rem; text-align: center;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); min-height: 50px;
  display: flex; align-items: center; justify-content: center;
}
.bet-opt:hover { border-color: var(--ch-epiphany); transform: translateY(-1px); }
.bet-opt.selected { background: var(--ch-epiphany-soft); border-color: var(--ch-epiphany); color: var(--ch-epiphany-ink); box-shadow: 0 0 12px var(--ch-epiphany-soft); }
.bet-opt.correct { border-color: var(--ch-ok); background: rgba(34,197,94,0.12); color: var(--ch-ok); }
.bet-opt.wrong { border-color: var(--ch-warn); background: rgba(239,68,68,0.10); color: var(--ch-warn); }
.case-reveal {
  width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--case-bug); border-radius: var(--r-sm);
  background: rgba(239,68,68,0.08); font-size: 0.78rem; color: var(--text-2);
  animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1);
}
.case-reveal .cr-name { color: var(--case-bug); font-weight: 600; }
.case-reveal .cr-cause { color: var(--text-3); font-size: 0.72rem; margin-top: 2px; }
.fog-account {
  width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--ch-boss-line);
  border-radius: var(--r-sm); background: var(--ch-boss-soft);
  font-size: 0.82rem; color: var(--text-2); font-style: italic;
  animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1);
}
.fog-account .fa-line { margin: var(--sp-1) 0; }
.fog-account .fa-line b { color: var(--ch-boss-ink); font-style: normal; }
.tv-comparison {
  width: 100%; display: grid; grid-template-columns: 1fr 1fr; gap: var(--sp-2);
  animation: riftOpen 600ms cubic-bezier(0.22,1,0.36,1);
}
.tv-side {
  padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-sunk); display: flex; flex-direction: column; gap: var(--sp-1);
}
.tv-side.test-side { border-left: 4px solid var(--ch-boss); }
.tv-side.verify-side { border-left: 4px solid var(--ch-epiphany); }
.tv-side .ts-label { font-size: 0.78rem; color: var(--text-3); font-family: var(--font-mono); }
.tv-side .ts-def { font-size: 0.9rem; color: var(--text-1); font-weight: 600; }
.tv-side .ts-limit { font-size: 0.78rem; color: var(--text-2); font-style: italic; }

/* ============================================================
   S1 逻辑基石 · 蕴含之误 · 真值表组装
   ============================================================ */
.cmp-logic-stone { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.predict-panel { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.predict-question { text-align: center; font-size: 1rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.predict-opts { display: grid; grid-template-columns: 1fr 1fr 1fr; gap: var(--sp-2); }
.predict-opt {
  padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-size: 0.85rem; text-align: center;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); min-height: 50px;
  display: flex; align-items: center; justify-content: center;
}
.predict-opt:hover { border-color: var(--accent); transform: translateY(-1px); }
.predict-opt.selected { background: var(--accent-soft); border-color: var(--accent); color: var(--accent-ink); box-shadow: var(--glow); }
.predict-opt.correct { border-color: var(--ch-ok); background: rgba(34,197,94,0.12); color: var(--ch-ok); }
.predict-opt.wrong { border-color: var(--ch-warn); background: rgba(239,68,68,0.10); color: var(--ch-warn); }
.predict-feedback {
  margin-top: var(--sp-2); padding: var(--sp-2) var(--sp-3); border-radius: var(--r-sm);
  font-size: 0.85rem; animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1);
}
.predict-feedback.right { border-color: var(--ch-ok); background: rgba(34,197,94,0.10); color: var(--ch-ok); }
.predict-feedback.wrong { border-color: var(--ch-warn); background: rgba(239,68,68,0.10); color: var(--ch-warn); }
.truth-table-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.truth-table { width: 100%; border-collapse: collapse; font-family: var(--font-mono); font-size: 0.85rem; }
.truth-table th, .truth-table td {
  border: 1px solid var(--glass-line); padding: var(--sp-2); text-align: center;
}
.truth-table th { background: var(--bg-elev); color: var(--accent-ink); font-weight: 600; }
.truth-table td.clickable { cursor: pointer; transition: all 200ms cubic-bezier(0.22,1,0.36,1); }
.truth-table td.clickable:hover { background: var(--accent-soft); border-color: var(--accent); }
.truth-table td.filled-true { background: rgba(34,197,94,0.12); color: var(--ch-ok); font-weight: 600; }
.truth-table td.filled-false { background: rgba(239,68,68,0.10); color: var(--ch-warn); font-weight: 600; }
.truth-table td.vacuous { background: var(--ch-epiphany-soft); color: var(--ch-epiphany-ink); }
.truth-feedback {
  margin-top: var(--sp-2); padding: var(--sp-2) var(--sp-3); border-radius: var(--r-sm);
  font-size: 0.82rem; animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1);
}
.truth-feedback.reject { border-color: var(--ch-warn); background: rgba(239,68,68,0.10); color: var(--ch-warn); font-style: italic; }
.truth-feedback.ok { border-color: var(--ch-epiphany); background: var(--ch-epiphany-soft); color: var(--ch-epiphany-ink); }
.quantifier-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.quantifier-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.quantifier-example { font-family: var(--font-mono); font-size: 0.85rem; color: var(--text-1); padding: var(--sp-2); border: 1px dashed var(--glass-line); border-radius: var(--r-xs); background: var(--bg-elev); margin-bottom: var(--sp-2); }
.quantifier-opts { display: flex; gap: var(--sp-2); justify-content: center; }
.quantifier-opt {
  padding: var(--sp-2) var(--sp-4); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 1rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); min-width: 60px; text-align: center;
}
.quantifier-opt:hover { border-color: var(--logic-stone); transform: translateY(-1px); }
.quantifier-opt.correct { border-color: var(--ch-ok); background: rgba(34,197,94,0.12); color: var(--ch-ok); }
.quantifier-opt.wrong { border-color: var(--ch-warn); background: rgba(239,68,68,0.10); color: var(--ch-warn); }
.quantifier-result { margin-top: var(--sp-2); font-family: var(--font-mono); font-size: 0.82rem; color: var(--text-2); min-height: 28px; }
.exclude-mark {
  width: 100%; margin-top: var(--sp-2); padding: var(--sp-2) var(--sp-3);
  border: 1px solid var(--ch-epiphany); border-radius: var(--r-sm);
  background: var(--ch-epiphany-soft); font-size: 0.82rem; color: var(--ch-epiphany-ink);
  font-style: italic; animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1);
}

/* ============================================================
   S2 状态空间指数爆炸追踪器
   ============================================================ */
.cmp-state-tracker { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.slider-panel { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.slider-row { display: flex; align-items: center; gap: var(--sp-3); width: 100%; margin-bottom: var(--sp-2); }
.slider-row input[type="range"] { flex: 1; }
.slider-value { font-family: var(--font-mono); font-size: 1.1rem; color: var(--accent-ink); min-width: 60px; text-align: center; font-weight: 600; }
.state-info { display: flex; gap: var(--sp-4); justify-content: center; flex-wrap: wrap; }
.state-info .si-cell { text-align: center; }
.state-info .si-label { font-size: 0.72rem; color: var(--text-3); }
.state-info .si-value { font-family: var(--font-mono); font-size: 0.95rem; color: var(--accent-ink); font-weight: 600; }
.state-info .si-value.warn { color: var(--ch-warn); }
.state-info .si-value.fatal { color: var(--explosion-curve); }
.state-canvas-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.state-canvas-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.state-canvas, .explosion-canvas, .mitigation-canvas, .proof-canvas, .hoare-canvas, .curry-canvas, .halting-canvas, .pipeline-canvas, .depth-curve, .syntax-canvas, .scope-canvas, .cfg-canvas {
  width: 100%; max-width: 480px; height: auto; border: 1px solid var(--glass-line); border-radius: var(--r-xs); background: var(--bg-elev);
}
.mitigation-panel { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.mitigation-panel h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.mitigation-row { display: grid; grid-template-columns: repeat(4, 1fr); gap: var(--sp-2); }
.mitigation-card {
  padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; text-align: center;
  transition: all 300ms cubic-bezier(0.22,1,0.36,1); min-height: 70px;
  display: flex; flex-direction: column; align-items: center; justify-content: center; gap: 4px;
}
.mitigation-card:hover { border-color: var(--mitigation-bdd); transform: translateY(-2px); }
.mitigation-card.applied { border-color: var(--mitigation-bdd); background: rgba(16,185,129,0.10); }
.mitigation-card[data-strategy="bdd"] { border-left: 3px solid var(--mitigation-bdd); }
.mitigation-card[data-strategy="abs"] { border-left: 3px solid var(--mitigation-abs); }
.mitigation-card[data-strategy="por"] { border-left: 3px solid var(--mitigation-por); }
.mitigation-card[data-strategy="sat"] { border-left: 3px solid var(--mitigation-sat); }
.mitigation-card .mc-name { font-family: var(--font-mono); font-size: 0.78rem; font-weight: 600; color: var(--text-1); }
.mitigation-card .mc-desc { font-size: 0.66rem; color: var(--text-3); }
.prediction-panel { width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--explosion-curve); border-radius: var(--r-sm); background: rgba(239,68,68,0.08); font-size: 0.85rem; color: var(--explosion-curve); animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1); }

/* ============================================================
   S3 LTL与CTL时序逻辑公式组装器
   ============================================================ */
.cmp-temporal-logic { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.mode-toggle { display: flex; gap: var(--sp-2); justify-content: center; }
.mode-btn {
  padding: var(--sp-2) var(--sp-4); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 0.85rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1);
}
.mode-btn:hover { border-color: var(--accent); }
.mode-btn.active[data-mode="LTL"] { background: var(--accent-soft); border-color: var(--ltl-color); color: var(--ltl-color); box-shadow: var(--glow); }
.mode-btn.active[data-mode="CTL"] { background: var(--accent-soft); border-color: var(--ctl-color); color: var(--ctl-color); box-shadow: var(--glow); }
.formula-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.formula-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.formula-target {
  font-family: var(--font-mono); font-size: 1rem; color: var(--text-1); text-align: center;
  padding: var(--sp-2); border: 1px dashed var(--glass-line); border-radius: var(--r-xs);
  background: var(--bg-elev); margin-bottom: var(--sp-2); min-height: 44px;
  display: flex; align-items: center; justify-content: center;
}
.formula-target .ft-slot {
  display: inline-block; min-width: 36px; padding: 2px 8px; margin: 0 2px;
  border: 1px dashed var(--glass-line); border-radius: var(--r-xs); color: var(--text-3);
  transition: all 200ms cubic-bezier(0.22,1,0.36,1);
}
.formula-target .ft-slot.filled { border-style: solid; border-color: var(--proof-chain); color: var(--proof-chain); background: var(--ch-epiphany-soft); }
.op-pool { display: flex; gap: var(--sp-1); justify-content: center; flex-wrap: wrap; }
.op-block {
  width: 44px; height: 44px; display: flex; align-items: center; justify-content: center;
  border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-elev);
  cursor: pointer; font-family: var(--font-mono); font-size: 0.9rem; font-weight: 600;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); user-select: none;
}
.op-block:hover { transform: translateY(-2px); }
.op-block[data-op="X"] { color: var(--op-next); border-color: var(--op-next); }
.op-block[data-op="F"] { color: var(--op-future); border-color: var(--op-future); }
.op-block[data-op="G"] { color: var(--op-global); border-color: var(--op-global); }
.op-block[data-op="U"] { color: var(--op-until); border-color: var(--op-until); }
.op-block[data-op="A"] { color: var(--op-all); border-color: var(--op-all); }
.op-block[data-op="E"] { color: var(--op-exists); border-color: var(--op-exists); }
.op-block[data-op="req"], .op-block[data-op="ack"] { color: var(--accent-ink); border-color: var(--accent); min-width: 60px; }
.op-block.placed { opacity: 0.35; cursor: default; }
.op-block.disabled { opacity: 0.25; cursor: not-allowed; }
.formula-feedback { margin-top: var(--sp-2); font-family: var(--font-mono); font-size: 0.82rem; color: var(--text-2); min-height: 28px; text-align: center; }
.formula-feedback.ok { color: var(--ch-ok); }
.formula-feedback.err { color: var(--ch-warn); }
.semantics-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.semantics-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.tool-binding { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.tool-binding h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.tool-code { font-family: var(--font-mono); font-size: 0.78rem; color: var(--text-2); padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-xs); background: var(--bg-elev); white-space: pre-wrap; margin-bottom: var(--sp-2); }
.tool-verdict { font-family: var(--font-mono); font-size: 0.85rem; padding: var(--sp-2); border-radius: var(--r-xs); text-align: center; }
.tool-verdict.pass { border: 1px solid var(--verify-pass); background: rgba(16,185,129,0.10); color: var(--verify-pass); }
.tool-verdict.fail { border: 1px solid var(--verify-fail); background: rgba(239,68,68,0.10); color: var(--verify-fail); }
.tl-comparison { width: 100%; display: grid; grid-template-columns: 1fr 1fr; gap: var(--sp-2); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.tl-comp-side { padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.tl-comp-side.ltl { border-left: 4px solid var(--ltl-color); }
.tl-comp-side.ctl { border-left: 4px solid var(--ctl-color); }
.tl-comp-side .tc-label { font-family: var(--font-mono); font-size: 0.78rem; color: var(--text-3); margin-bottom: 4px; }
.tl-comp-side .tc-formula { font-family: var(--font-mono); font-size: 0.85rem; color: var(--text-1); margin-bottom: 4px; }
.tl-comp-side .tc-desc { font-size: 0.75rem; color: var(--text-2); }

/* ============================================================
   S4 验证工具 · SPIN与NuSMV
   ============================================================ */
.cmp-verify-tool { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.tool-tabs { display: flex; gap: var(--sp-2); justify-content: center; }
.tool-tab {
  padding: var(--sp-2) var(--sp-4); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 0.85rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1);
}
.tool-tab:hover { border-color: var(--accent); }
.tool-tab.active[data-tool="spin"] { background: var(--accent-soft); border-color: var(--spin-silver); color: var(--spin-silver); }
.tool-tab.active[data-tool="nusmv"] { background: var(--accent-soft); border-color: var(--nusmv-indigo); color: var(--nusmv-indigo); }
.tool-editor { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.tool-editor h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.code-template { font-family: var(--font-mono); font-size: 0.78rem; color: var(--text-1); padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-xs); background: var(--bg-elev); white-space: pre; line-height: 1.6; margin-bottom: var(--sp-2); }
.code-template .ct-line { display: block; transition: all 200ms cubic-bezier(0.22,1,0.36,1); padding: 1px 4px; border-radius: 2px; }
.code-template .ct-line.missing { color: var(--ch-warn); background: rgba(239,68,68,0.08); cursor: pointer; }
.code-template .ct-line.filled { color: var(--verify-pass); background: rgba(16,185,129,0.08); }
.code-template .ct-line.highlight { background: var(--accent-soft); }
.property-input { display: flex; gap: var(--sp-2); align-items: center; margin-bottom: var(--sp-2); }
.property-input label { font-family: var(--font-mono); font-size: 0.78rem; color: var(--text-3); }
.property-input code { font-family: var(--font-mono); font-size: 0.82rem; color: var(--accent-ink); padding: var(--sp-1) var(--sp-2); background: var(--accent-soft); border-radius: var(--r-xs); }
.verify-result { padding: var(--sp-2) var(--sp-3); border-radius: var(--r-sm); font-size: 0.85rem; animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1); }
.verify-result.pass { border: 1px solid var(--verify-pass); background: rgba(16,185,129,0.10); color: var(--verify-pass); }
.verify-result.fail { border: 1px solid var(--verify-fail); background: rgba(239,68,68,0.10); color: var(--verify-fail); }
.fdiv-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.fdiv-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.fdiv-table { display: grid; grid-template-columns: repeat(5, 1fr); gap: 4px; margin-bottom: var(--sp-2); }
.fdiv-cell {
  padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-xs);
  background: var(--bg-elev); cursor: pointer; text-align: center; font-family: var(--font-mono); font-size: 0.7rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); min-height: 40px;
  display: flex; align-items: center; justify-content: center;
}
.fdiv-cell:hover { border-color: var(--accent); }
.fdiv-cell.verified { border-color: var(--verify-pass); background: rgba(16,185,129,0.10); color: var(--verify-pass); }
.fdiv-cell.defect { border-color: var(--verify-fail); background: rgba(239,68,68,0.10); color: var(--verify-fail); }

/* ============================================================
   S5 状态爆炸 · 穷举之极限
   ============================================================ */
.cmp-explosion { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.pusher-panel { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); transition: all 600ms cubic-bezier(0.22,1,0.36,1); }
.pusher-panel.burning { border-color: var(--explosion-curve); background: rgba(239,68,68,0.06); box-shadow: 0 0 24px rgba(239,68,68,0.2); }
.pusher-row { display: flex; align-items: center; gap: var(--sp-3); width: 100%; margin-bottom: var(--sp-2); }
.pusher-row input[type="range"] { flex: 1; }
.pusher-value { font-family: var(--font-mono); font-size: 1.2rem; color: var(--accent-ink); min-width: 80px; text-align: center; font-weight: 600; }
.pusher-value.fatal { color: var(--explosion-curve); }
.explosion-data { display: flex; gap: var(--sp-4); justify-content: center; flex-wrap: wrap; margin-bottom: var(--sp-2); }
.ed-cell { text-align: center; }
.ed-cell .ed-label { font-size: 0.72rem; color: var(--text-3); }
.ed-cell .ed-value { font-family: var(--font-mono); font-size: 0.95rem; color: var(--accent-ink); font-weight: 600; }
.ed-cell .ed-value.fatal { color: var(--explosion-curve); }
.cosmos-scale { width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-xs); background: var(--bg-elev); margin-bottom: var(--sp-2); }
.cosmos-bar { width: 100%; height: 12px; border: 1px solid var(--glass-line); border-radius: 6px; background: var(--bg-sunk); overflow: hidden; position: relative; }
.cosmos-fill { height: 100%; width: 0; background: var(--explosion-curve); transition: width 600ms cubic-bezier(0.22,1,0.36,1); }
.cosmos-mark { position: absolute; top: -2px; height: 16px; width: 2px; background: var(--ch-epiphany); }
.cosmos-label { display: flex; justify-content: space-between; font-size: 0.7rem; color: var(--text-3); margin-top: 2px; font-family: var(--font-mono); }
.collapse-zone {
  width: 100%; padding: var(--sp-3); border: 1px solid var(--explosion-curve); border-radius: var(--r-sm);
  background: rgba(239,68,68,0.10); text-align: center; font-style: italic; color: var(--explosion-curve);
  animation: shatterIn 800ms cubic-bezier(0.22,1,0.36,1);
}
@keyframes shatterIn {
  0% { opacity: 0; transform: scale(0.8) rotate(-2deg); }
  50% { opacity: 1; transform: scale(1.05) rotate(1deg); }
  100% { opacity: 1; transform: scale(1) rotate(0deg); }
}
.wound-display {
  width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--scar-crack); border-radius: var(--r-sm);
  background: rgba(239,68,68,0.08); font-size: 0.82rem; color: var(--scar-crack); font-style: italic;
  animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1);
}

/* ============================================================
   S6 定理证明 · Coq与Lean
   ============================================================ */
.cmp-proof-tower { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.proof-build-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.proof-build-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.proof-chain-display {
  font-family: var(--font-mono); font-size: 0.82rem; padding: var(--sp-2); border: 1px dashed var(--glass-line);
  border-radius: var(--r-xs); background: var(--bg-elev); margin-bottom: var(--sp-2); min-height: 60px;
  display: flex; flex-direction: column; gap: 4px;
}
.proof-step {
  padding: var(--sp-1) var(--sp-2); border-left: 2px solid var(--proof-chain); color: var(--text-1);
  animation: riftOpen 300ms cubic-bezier(0.22,1,0.36,1);
}
.proof-step .ps-rule { color: var(--proof-chain); font-weight: 600; }
.proof-step.broken { border-left-color: var(--proof-crack); color: var(--proof-crack); text-decoration: line-through; }
.rule-pool { display: flex; gap: var(--sp-1); justify-content: center; flex-wrap: wrap; }
.rule-block {
  padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 0.78rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); min-height: 44px;
  display: flex; align-items: center; justify-content: center;
}
.rule-block:hover { border-color: var(--proof-chain); transform: translateY(-2px); }
.rule-block.placed { opacity: 0.35; cursor: default; }
.coq-terminal { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.coq-terminal h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.coq-output { font-family: var(--font-mono); font-size: 0.78rem; color: var(--text-1); padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-xs); background: var(--bg-sunk); white-space: pre; line-height: 1.6; min-height: 80px; }
.coq-output .coq-prompt { color: var(--proof-chain); }
.coq-output .coq-err { color: var(--ch-warn); }
.coq-output .coq-ok { color: var(--verify-pass); }
.coq-cmds { display: flex; gap: var(--sp-1); flex-wrap: wrap; margin-top: var(--sp-2); }
.coq-cmd {
  padding: 4px 10px; border: 1px solid var(--glass-line); border-radius: var(--r-xs);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 0.75rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1);
}
.coq-cmd:hover { border-color: var(--proof-chain); }
.coq-cmd.used { opacity: 0.4; cursor: default; }
.four-color-note { width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--proof-chain); border-radius: var(--r-sm); background: var(--ch-epiphany-soft); font-size: 0.82rem; color: var(--ch-epiphany-ink); animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1); }

/* ============================================================
   S7 Hoare之秤 · 程序正确性证明
   ============================================================ */
.cmp-hoare-scale { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.hoare-triple-display {
  width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-sunk); display: flex; align-items: center; justify-content: center; gap: var(--sp-3);
  font-family: var(--font-mono); font-size: 1rem;
}
.hoare-triple-display .ht-pre { color: var(--precondition); }
.hoare-triple-display .ht-stmt { color: var(--hoare-triple); font-weight: 600; }
.hoare-triple-display .ht-post { color: var(--postcondition); }
.hoare-triple-display .ht-brace { color: var(--text-3); }
.invariant-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.invariant-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.invariant-opts { display: grid; grid-template-columns: repeat(3, 1fr); gap: var(--sp-2); margin-bottom: var(--sp-2); }
.invariant-opt {
  padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 0.82rem; text-align: center;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); min-height: 50px;
  display: flex; align-items: center; justify-content: center;
}
.invariant-opt:hover { border-color: var(--invariant); transform: translateY(-1px); }
.invariant-opt.correct { border-color: var(--invariant); background: rgba(16,185,129,0.10); color: var(--invariant); }
.invariant-opt.wrong { border-color: var(--ch-warn); background: rgba(239,68,68,0.10); color: var(--ch-warn); }
.invariant-check { padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-xs); background: var(--bg-elev); font-family: var(--font-mono); font-size: 0.78rem; }
.invariant-check .ic-line { margin: var(--sp-1) 0; display: flex; align-items: center; gap: var(--sp-2); }
.invariant-check .ic-cond { color: var(--text-3); min-width: 80px; }
.invariant-check .ic-result { font-weight: 600; }
.invariant-check .ic-result.ok { color: var(--ch-ok); }
.invariant-check .ic-result.fail { color: var(--ch-warn); }
.scar-heal-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--scar-crack); border-radius: var(--r-sm); background: rgba(239,68,68,0.06); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); transition: all 800ms cubic-bezier(0.22,1,0.36,1); }
.scar-heal-zone.healed { border-color: var(--scar-healed); background: var(--ch-epiphany-soft); }
.scar-heal-zone h4 { font-size: 0.85rem; color: var(--scar-crack); margin-bottom: var(--sp-2); }
.scar-heal-zone.healed h4 { color: var(--scar-healed); }
.scar-crack-display { font-family: var(--font-mono); font-size: 0.82rem; color: var(--scar-crack); padding: var(--sp-2); border: 1px solid var(--scar-crack); border-radius: var(--r-xs); background: var(--bg-elev); margin-bottom: var(--sp-2); }
.scar-heal-zone.healed .scar-crack-display { color: var(--scar-healed); border-color: var(--scar-healed); }
.tool-cards { width: 100%; display: grid; grid-template-columns: repeat(3, 1fr); gap: var(--sp-2); }
.tool-card {
  padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-sunk); text-align: center;
  transition: all 300ms cubic-bezier(0.22,1,0.36,1); min-height: 80px;
  display: flex; flex-direction: column; align-items: center; justify-content: center; gap: 4px;
  opacity: 0.6;
}
.tool-card:hover { border-color: var(--accent); opacity: 1; transform: translateY(-2px); }
.tool-card.lit { opacity: 1; border-color: var(--accent); background: var(--accent-soft); box-shadow: var(--glow); }
.tool-card .tc-name { font-family: var(--font-mono); font-size: 0.82rem; font-weight: 600; color: var(--text-1); }
.tool-card .tc-desc { font-size: 0.7rem; color: var(--text-3); }

/* ============================================================
   S8 类型即证明 · Curry-Howard与可计算性
   ============================================================ */
.cmp-curry-howard { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.ch-mode-toggle { display: flex; gap: var(--sp-2); justify-content: center; }
.ch-mode-btn {
  padding: var(--sp-2) var(--sp-4); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 0.82rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1);
}
.ch-mode-btn:hover { border-color: var(--curry-gold); }
.ch-mode-btn.active { background: var(--ch-epiphany-soft); border-color: var(--curry-gold); color: var(--curry-gold); box-shadow: var(--glow); }
.ch-correspondence { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.ch-correspondence h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.ch-pairs { display: grid; grid-template-columns: 1fr 1fr; gap: var(--sp-2); }
.ch-pair {
  display: flex; align-items: center; gap: var(--sp-2); padding: var(--sp-2); border: 1px solid var(--glass-line);
  border-radius: var(--r-sm); background: var(--bg-elev); cursor: pointer;
  transition: all 300ms cubic-bezier(0.22,1,0.36,1); min-height: 50px;
}
.ch-pair:hover { border-color: var(--curry-gold); transform: translateY(-1px); }
.ch-pair.matched { border-color: var(--curry-gold); background: var(--ch-epiphany-soft); box-shadow: 0 0 10px var(--ch-epiphany-soft); }
.ch-pair .cp-prop { color: var(--proposition); font-family: var(--font-mono); font-size: 0.82rem; flex: 1; }
.ch-pair .cp-arrow { color: var(--text-3); font-size: 0.78rem; }
.ch-pair .cp-type { color: var(--type); font-family: var(--font-mono); font-size: 0.82rem; flex: 1; text-align: right; }
.ch-pair .cp-status { font-size: 0.7rem; color: var(--text-3); }
.ch-pair.matched .cp-status { color: var(--curry-gold); }
.dep-editor { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.dep-editor h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.dep-output { font-family: var(--font-mono); font-size: 0.78rem; color: var(--text-1); padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-xs); background: var(--bg-sunk); white-space: pre; line-height: 1.6; min-height: 80px; }
.dep-output .dep-ok { color: var(--curry-gold); }
.dep-output .dep-err { color: var(--ch-warn); }
.dep-cmds { display: flex; gap: var(--sp-1); flex-wrap: wrap; margin-top: var(--sp-2); }
.dep-cmd {
  padding: 4px 10px; border: 1px solid var(--glass-line); border-radius: var(--r-xs);
  background: var(--bg-elev); cursor: pointer; font-family: var(--font-mono); font-size: 0.75rem;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1);
}
.dep-cmd:hover { border-color: var(--curry-gold); }
.dep-cmd.used { opacity: 0.4; cursor: default; }
.halting-zone { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1); }
.halting-zone h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.halting-steps { display: flex; flex-direction: column; gap: var(--sp-1); margin-bottom: var(--sp-2); }
.halting-step {
  padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-xs);
  background: var(--bg-elev); font-family: var(--font-mono); font-size: 0.78rem; color: var(--text-2);
  cursor: pointer; transition: all 300ms cubic-bezier(0.22,1,0.36,1); opacity: 0.5;
}
.halting-step:hover { border-color: var(--halting-ring); opacity: 1; }
.halting-step.shown { opacity: 1; border-left: 3px solid var(--halting-ring); }
.halting-step.contradiction { border-left-color: var(--halting-break); color: var(--halting-break); }
.rice-theorem { padding: var(--sp-2) var(--sp-3); border: 1px solid var(--ch-epiphany); border-radius: var(--r-sm); background: var(--ch-epiphany-soft); font-size: 0.82rem; color: var(--ch-epiphany-ink); animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1); }
.safety-cards { width: 100%; display: grid; grid-template-columns: repeat(2, 1fr); gap: var(--sp-2); }
.safety-card {
  padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-sunk); transition: all 300ms cubic-bezier(0.22,1,0.36,1); min-height: 70px;
  display: flex; flex-direction: column; gap: 4px;
}
.safety-card.lit { border-color: var(--ch-epiphany); background: var(--ch-epiphany-soft); }
.safety-card .sc-name { font-family: var(--font-mono); font-size: 0.8rem; font-weight: 600; color: var(--text-1); }
.safety-card .sc-desc { font-size: 0.72rem; color: var(--text-3); }

/* ============================================================
   S9 Boss 战 · 状态爆炸之雾三问
   ============================================================ */
#s9-arena { border-color: var(--ch-boss-line); box-shadow: var(--shadow), 0 0 32px var(--ch-boss-soft); }
.boss-figure { width: 100%; display: flex; justify-content: center; margin-bottom: var(--sp-2); }
#s9-boss-canvas { width: 100%; max-width: 480px; height: auto; border: 1px solid var(--ch-boss-line); border-radius: var(--r-sm); background: var(--bg-elev); }
.q-progress-bar { width: 100%; height: 6px; border: 1px solid var(--glass-line); border-radius: 3px; background: var(--bg-sunk); margin-bottom: var(--sp-2); overflow: hidden; }
.q-progress-fill { height: 100%; width: 0; background: var(--accent); transition: width 600ms cubic-bezier(0.22,1,0.36,1); }
.fog-ledger {
  width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--ch-boss-line);
  border-radius: var(--r-sm); background: var(--ch-boss-soft);
  font-size: 0.8rem; color: var(--text-2); margin-bottom: var(--sp-2);
}
.fog-ledger .fl-line { margin: var(--sp-1) 0; font-style: italic; }
.fog-ledger .fl-line b { color: var(--ch-boss-ink); font-style: normal; }
.q-panel { width: 100%; padding: var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); margin-bottom: var(--sp-2); }
.q-text { font-size: 0.95rem; color: var(--text-1); margin-bottom: var(--sp-2); }
.q-evidence { font-size: 0.78rem; color: var(--ch-boss-ink); font-style: italic; padding: var(--sp-1) var(--sp-2); border-left: 2px solid var(--ch-boss-line); }
.option-grid { display: grid; grid-template-columns: 1fr 1fr; gap: var(--sp-2); margin-bottom: var(--sp-2); }
.q-option {
  padding: var(--sp-2) var(--sp-3); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-elev); cursor: pointer; font-size: 0.85rem; text-align: center;
  transition: all 200ms cubic-bezier(0.22,1,0.36,1); min-height: 50px;
  display: flex; align-items: center; justify-content: center;
}
.q-option:hover { border-color: var(--accent); transform: translateY(-1px); }
.q-option.correct { border-color: var(--answer-correct); background: rgba(16,185,129,0.12); color: var(--answer-correct); box-shadow: 0 0 12px rgba(16,185,129,0.2); }
.q-option.wrong { border-color: var(--answer-wrong); background: rgba(239,68,68,0.10); color: var(--answer-wrong); }
.q-option.eliminated { opacity: 0.3; cursor: default; text-decoration: line-through; border-color: var(--answer-eliminated); background: rgba(75,85,99,0.16); transform: none; }
.q-feedback {
  padding: var(--sp-2) var(--sp-3); border-radius: var(--r-sm); font-size: 0.85rem; min-height: 32px;
  margin-bottom: var(--sp-2); animation: riftOpen 400ms cubic-bezier(0.22,1,0.36,1);
}
.q-feedback.right { border-color: var(--answer-correct); background: rgba(16,185,129,0.10); color: var(--answer-correct); }
.q-feedback.wrong { border-color: var(--answer-wrong); background: rgba(239,68,68,0.10); color: var(--answer-wrong); font-style: italic; }
.scar-projection {
  width: 100%; margin-top: var(--sp-2); padding: var(--sp-2) var(--sp-3);
  border: 1px solid var(--scar-projection); border-radius: var(--r-sm);
  background: var(--ch-indigo-soft); animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1);
}
.scar-projection h4 { font-size: 0.85rem; color: var(--ch-indigo-ink); margin-bottom: var(--sp-2); }
.scar-projection .sp-item {
  padding: var(--sp-1) var(--sp-2); margin-bottom: var(--sp-1);
  border: 1px solid var(--glass-line); border-radius: var(--r-xs);
  background: var(--bg-elev); font-size: 0.78rem;
  transition: all 300ms cubic-bezier(0.22,1,0.36,1);
}
.scar-projection .sp-item.lit {
  border-color: var(--scar-projection); color: var(--ch-indigo-ink);
  background: var(--ch-indigo-soft); box-shadow: 0 0 8px var(--ch-indigo-soft);
}
.fog-thickness { width: 100%; margin-top: var(--sp-2); }
.thickness-label { font-size: 0.75rem; color: var(--text-3); margin-bottom: 4px; }
.thickness-bar { width: 100%; height: 10px; border: 1px solid var(--ch-boss-line); border-radius: 5px; background: var(--bg-sunk); overflow: hidden; }
.thickness-fill { height: 100%; width: 0; background: var(--fog-body); transition: width 600ms cubic-bezier(0.22,1,0.36,1); }
.mentor-hint {
  width: 100%; padding: var(--sp-2) var(--sp-3); border: 1px solid var(--mentor-hint); border-radius: var(--r-sm);
  background: rgba(139,92,246,0.10); font-size: 0.82rem; color: var(--mentor-hint); font-style: italic;
  animation: riftOpen 500ms cubic-bezier(0.22,1,0.36,1);
}
.fog-collapse {
  width: 100%; padding: var(--sp-3); border: 1px solid var(--breakthrough); border-radius: var(--r-sm);
  background: var(--ch-epiphany-soft); text-align: center; font-style: italic; color: var(--ch-epiphany-ink);
  animation: shatterIn 800ms cubic-bezier(0.22,1,0.36,1);
}

/* ============================================================
   S10 知识图谱点亮 + 证明链剪影
   ============================================================ */
.cmp-finale { width: 100%; display: flex; flex-direction: column; gap: var(--sp-3); }
.puzzle-area { display: grid; grid-template-columns: repeat(4, 1fr); gap: var(--sp-2); }
.puzzle-piece {
  padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-sm);
  background: var(--bg-sunk); text-align: center; cursor: default;
  transition: all 400ms cubic-bezier(0.22,1,0.36,1); min-height: 60px;
  display: flex; flex-direction: column; align-items: center; justify-content: center; gap: 4px;
  opacity: 0.3;
}
.puzzle-piece.lit { opacity: 1; border-color: var(--accent); background: var(--accent-soft); box-shadow: var(--glow); }
.puzzle-piece .pp-name { font-family: var(--font-mono); font-size: 0.75rem; font-weight: 600; color: var(--text-1); }
.puzzle-piece .pp-tag { font-size: 0.65rem; color: var(--text-3); }
.chain-silhouette { width: 100%; padding: var(--sp-2); border: 1px solid var(--glass-line); border-radius: var(--r-sm); background: var(--bg-sunk); }
.depth-readout { padding: var(--sp-2); font-family: var(--font-mono); font-size: 0.82rem; color: var(--accent-ink); text-align: center; min-height: 28px; }
.depth-readout.warn { color: var(--ch-warn); }
.system-map h4 { font-size: 0.85rem; color: var(--accent-ink); margin-bottom: var(--sp-2); }
.map-grid { display: grid; grid-template-columns: repeat(4, 1fr); gap: 4px; }
.map-node {
  padding: var(--sp-1) 4px; border: 1px solid var(--glass-line); border-radius: var(--r-xs); font-size: 0.7rem;
  background: var(--bg-elev); color: var(--text-3); text-align: center; opacity: 0.4;
  transition: all 300ms cubic-bezier(0.22,1,0.36,1); min-height: 44px;
  display: flex; align-items: center; justify-content: center;
}
.map-node.lit { opacity: 1; border-color: var(--accent); background: var(--accent-soft); color: var(--accent); }
.map-node.lit.center { border-color: var(--ch-epiphany); background: var(--ch-epiphany-soft); color: var(--ch-epiphany-ink); box-shadow: 0 0 12px var(--ch-epiphany-soft); }
.realm-achieved {
  margin-top: var(--sp-3); text-align: center; padding: var(--sp-3);
  border: 1px solid var(--ch-epiphany); border-radius: var(--r-sm);
  background: var(--ch-epiphany-soft);
}
.realm-glow {
  font-family: var(--font-mono); font-size: 1.1rem; color: var(--ch-epiphany-ink); letter-spacing: 0.2em;
}
@keyframes realmGlow {
  0%, 100% { box-shadow: 0 0 18px var(--accent-soft); }
  50% { box-shadow: 0 0 32px rgba(99,102,241,0.4); }
}
.realm-achieved { animation: realmGlow 3s ease-in-out infinite; }

/* ============================================================
   响应式 · 移动端适配
   ============================================================ */
@media (max-width: 640px) {
  .op-title { font-size: clamp(2rem, 12vw, 3.5rem); }
  .op-sub { letter-spacing: 0.3em; }
  .case-gallery { grid-template-columns: 1fr 1fr; }
  .bet-opts { grid-template-columns: 1fr; }
  .predict-opts { grid-template-columns: 1fr; }
  .invariant-opts { grid-template-columns: 1fr; }
  .tv-comparison { grid-template-columns: 1fr; }
  .tl-comparison { grid-template-columns: 1fr; }
  .mitigation-row { grid-template-columns: 1fr 1fr; }
  .option-grid { grid-template-columns: 1fr; }
  .fdiv-table { grid-template-columns: repeat(3, 1fr); }
  .tool-cards { grid-template-columns: 1fr; }
  .ch-pairs { grid-template-columns: 1fr; }
  .safety-cards { grid-template-columns: 1fr; }
  .puzzle-area { grid-template-columns: repeat(2, 1fr); }
  .map-grid { grid-template-columns: repeat(2, 1fr); }
  .quantifier-opts { flex-wrap: wrap; }
  .knob-row { flex-direction: column; align-items: stretch; }
}

@media (prefers-reduced-motion: reduce) {
  .realm-achieved { animation: none; }
  .predict-feedback, .exclude-mark, .case-reveal, .fog-account, .truth-feedback, .quantifier-result,
  .truth-table-zone, .quantifier-zone, .state-canvas-zone, .mitigation-panel, .prediction-panel,
  .formula-zone, .semantics-zone, .tool-binding, .tool-editor, .fdiv-zone, .collapse-zone, .wound-display,
  .coq-terminal, .four-color-note, .scar-heal-zone, .dep-editor, .halting-zone, .rice-theorem,
  .fog-collapse, .crack-projection, .scar-projection, .fog-ledger, .mentor-hint, .verify-result,
  .tool-card, .formula-target, .proof-step, .halting-step { animation: none; }
  .case-card:hover, .op-block:hover, .mitigation-card:hover { transform: none; }
}