/* ============================================================================
   theme-paper.css —— 「学术论文风 · 亮色」标注面板主题(v1,独立文件)
   由 index-paper.html 独家加载(不与 app.css 并存),故此表**自包含**:
   既承载全部功能性布局(flex / grid / --nlfr / sticky —— 与 app.js 契约一致),
   也重做全部美术层。类名/ #id 沿用 app.js 生成的既有 hook(见 app.css 对照)。
   离线约束:字体只用系统栈,零外链 / 零 CDN / 零 @font-face 远程。
   语义色 = display_state.main(服务端算),色值可微调、语义不变(research.md:51)。
   ============================================================================ */

:root{
  /* —— 字族:标题/自然语言=衬线,界面=无衬线,形式化/代码=等宽 —— */
  --serif:Georgia,"Times New Roman","Songti SC","STSong","Noto Serif CJK SC","Source Han Serif SC",serif;
  --sans:-apple-system,BlinkMacSystemFont,"Segoe UI","Noto Sans CJK SC","PingFang SC","Microsoft YaHei",system-ui,sans-serif;
  --mono:"SF Mono","JetBrains Mono","Cascadia Code",ui-monospace,"Sarasa Mono SC",Menlo,Consolas,monospace;
  /* —— 纸感底色 / 墨色 / 发丝线 —— */
  --paper:#faf7f0; --paper-raise:#fffdf8; --paper-sink:#f3eee2;
  --ink:#242018; --ink-soft:#5f574a; --ink-faint:#8f8676;
  --rule:#e7e0d0; --rule-2:#d9d0bc;
  --accent:#33506e; --accent-soft:#e9eef3;   /* 深青蓝:链接/当前/聚焦 */
  /* —— R4 语义色(学术亮色板)+ 各自浅化底 —— */
  --s-perfect:#3f7a5e;   --s-perfect-bg:#edf4ef;
  --s-minor:#a9781a;     --s-minor-bg:#f6efda;
  --s-major:#b4552d;     --s-major-bg:#f7e9df;
  --s-uncertain:#6b5f96; --s-uncertain-bg:#efedf6;
  --s-mok:#6d88a3;       --s-mok-bg:#eef2f5;
  --s-mfail:#a23b34;     --s-mfail-bg:#f6e8e5;
  --s-mnone:#a9a295;     --s-mnone-bg:#f1efe8;
}

*{box-sizing:border-box}
body{font-family:var(--sans);color:var(--ink);background:var(--paper);
     margin:0;display:flex;flex-direction:column;height:100vh;
     font-size:15px;line-height:1.5;-webkit-font-smoothing:antialiased}

/* ============================== 报头 masthead ============================== */
#topbar{display:flex;align-items:center;gap:20px;flex-shrink:0;
        padding:12px 28px;background:var(--paper);
        border-bottom:3px double var(--rule-2)}       /* 论文标题线 */
.masthead{display:flex;flex-direction:column;line-height:1.15}
.brand{font-family:var(--serif);font-size:19px;font-weight:600;letter-spacing:.01em;color:var(--ink)}
.brand-sub{font-size:11.5px;color:var(--ink-faint);letter-spacing:.02em;margin-top:3px}
#topbar .spacer{flex:1}
#stats{font-size:12.5px;color:var(--ink-soft);letter-spacing:.01em}
#stats b{font-weight:700;color:var(--ink);font-variant-numeric:tabular-nums}
#topbar button{font-family:var(--sans);font-size:12px;letter-spacing:.06em;text-transform:uppercase;
        padding:5px 14px;border-radius:3px;border:1px solid var(--rule-2);
        background:var(--paper-raise);color:var(--ink-soft);cursor:pointer;transition:.15s}
#topbar button:hover{border-color:var(--accent);color:var(--accent);background:var(--accent-soft)}
.sw{display:inline-block;width:10px;height:10px;border-radius:2px;margin-right:4px;vertical-align:-1px}

/* ============================== 主区三栏 ============================== */
#content{display:flex;flex:1;min-height:0}

/* 侧栏 = 目录(TOC) */
#side{width:322px;flex-shrink:0;min-height:0;display:flex;flex-direction:column;
      background:var(--paper-sink)}
/* 侧栏↔卡片 分栏手柄:填满 8px 抓取区,视觉为居中 1px 线(接管原 #side 右边框),hover 加粗 */
#sidesplit{flex-shrink:0;width:8px;cursor:col-resize;touch-action:none;
           background:linear-gradient(var(--rule-2),var(--rule-2)) center/1px 100% no-repeat}
#sidesplit:hover,#sidesplit:active{background:linear-gradient(var(--accent),var(--accent)) center/2px 100% no-repeat}
#tabs{display:flex;gap:16px;flex-shrink:0;padding:10px 16px;border-bottom:1px solid var(--rule);font-size:12.5px}
#tabs .tab{color:var(--ink-faint);text-decoration:none;padding:2px 0;letter-spacing:.02em;
           border-bottom:2px solid transparent}
#tabs .tab:hover{color:var(--ink-soft)}
#tabs .tab.cur{color:var(--ink);border-bottom-color:var(--accent);font-weight:600}
#search{margin:9px 12px 4px;padding:6px 10px;font-family:var(--sans);font-size:13px;
        box-sizing:border-box;flex-shrink:0;color:var(--ink);background:var(--paper-raise);
        border:1px solid var(--rule-2);border-radius:3px;letter-spacing:.01em}
#search::placeholder{color:var(--ink-faint)}
#search:focus{outline:none;border-color:var(--accent);box-shadow:0 0 0 2px var(--accent-soft)}
#list{flex:1;overflow-y:auto;padding:8px 8px 24px}
.listempty{color:var(--ink-faint);padding:8px 12px;font-size:12.5px;font-style:italic}
mark.shl{background:var(--s-minor-bg);color:inherit;border-radius:2px;padding:0 1px;
         box-shadow:inset 0 0 0 1px var(--s-minor)}

/* 目录条 */
.item{padding:7px 12px;margin-bottom:1px;border-radius:3px;cursor:pointer;font-size:13px;
      border-left:2px solid transparent;color:var(--ink-soft);contain:layout paint style}
.item:hover{background:var(--paper-raise)}
.item.cur{background:var(--paper-raise);border-left-color:var(--accent);color:var(--ink)}
.item small{color:var(--ink-faint);font-size:11.5px}
.vdot{display:inline-block;width:8px;height:8px;border-radius:50%;margin-right:6px;vertical-align:0}
.vdot.review-pending{background:var(--accent)}
.vdot.review-in-progress{background:#4d8792}
.vdot.review-stale{background:var(--s-mfail)}
.vdot.review-na{background:var(--s-mnone)}
.vdot.review-complete,.vdot.review-Perfect{background:var(--s-perfect)}
.vdot.review-Minor{background:var(--s-minor)}
.vdot.review-Major{background:var(--s-major)}
.vdot.review-Uncertain{background:var(--s-uncertain)}
.hv{color:var(--s-perfect);font-weight:700;font-size:11px;margin-left:5px;border:1px solid var(--s-perfect);
    border-radius:50%;display:inline-block;width:13px;height:13px;line-height:12px;text-align:center;vertical-align:1px}
.stalemark{color:var(--s-major);font-weight:700;font-size:11px;margin-left:5px;border:1px dashed var(--s-major);
    border-radius:50%;display:inline-block;width:13px;height:13px;line-height:12px;text-align:center;vertical-align:1px}

/* 阅读栏:宽栏居中、宽松留白(纸张感)。NL|FL 内含 Lean 代码需要横向空间 →
   加宽阅读栏(原 900 太窄、代码被横向截断)。注意:padding 的 % 基准是包含块
   (#content=整视口,含 322px 侧栏),故阈值取 1600 抵消侧栏,内容栏在 ~1550 屏
   有效约 1150px、宽屏封顶约 1280px。
   底部 padding 必须为 0:#judgebar 是 position:sticky;bottom:0,其吸附基准是本
   滚动容器的 content box —— 任何 padding-bottom 都会把判定条整体上抬同等距离
   (原 128px 正是「判定条悬在半空、遮住正文」的根因)。改用 scroll-padding-bottom
   给键盘选原子(scrollIntoView)留出条高空间,既不上抬判定条又不被其遮挡。 */
#main{flex:1;min-width:0;width:auto;overflow-y:auto;background:var(--paper);scroll-padding-bottom:150px;
      padding:24px 24px 0}
.card-loading{max-width:1100px;margin:0 auto;padding-top:8px}
.card-loading-title{font:600 17px var(--sans);color:var(--ink-soft);margin-bottom:17px}
.card-loading-line,.card-loading-pane{position:relative;overflow:hidden;background:var(--paper-sink);
  border:1px solid var(--rule);border-radius:3px}
.card-loading-line{height:14px;margin-bottom:15px}.card-loading-line.wide{width:62%}
.card-loading-columns{display:grid;grid-template-columns:1fr 1fr;gap:16px}
.card-loading-pane{height:180px}
.card-loading-line::after,.card-loading-pane::after{content:"";position:absolute;inset:0;
  transform:translateX(-100%);background:linear-gradient(90deg,transparent,var(--paper-raise),transparent);
  animation:card-loading-shimmer 1.1s ease-in-out infinite}
@keyframes card-loading-shimmer{to{transform:translateX(100%)}}
.semantic-v10-box,.proof-trust-v10,.reviewbox{content-visibility:auto;contain-intrinsic-size:auto 240px}
.meta{color:var(--ink-faint);font-size:12.5px}
.nonl{color:var(--ink-faint);font-style:italic}

/* kind 徽章 = 定理环境标签 */
.kindbadge{display:inline-block;font-family:var(--sans);font-size:10.5px;font-weight:700;
           text-transform:uppercase;letter-spacing:.08em;color:var(--ink-soft);
           background:transparent;border:1px solid var(--rule-2);border-radius:2px;
           padding:1px 8px;vertical-align:3px}

/* NL|FL 对开双栏(保留 --nlfr/--flfr 与 8px 分隔柄) */
.pairbox{display:grid;align-items:start;gap:16px 0;margin-top:4px;
         grid-template-columns:minmax(0,var(--nlfr,1fr)) 8px minmax(0,var(--flfr,1fr))}
/* 填满 grid 预留的 8px 轨道当抓取区(元素本身 8px 宽),视觉仍是居中 1px 细线;
   hover 时线加粗到 2px 给「可拖」反馈。旧版把元素缩成 width:1px → 人手抓不住。 */
.vsplit{cursor:col-resize;align-self:stretch;min-height:40px;touch-action:none;
        background:linear-gradient(var(--rule-2),var(--rule-2)) center/1px 100% no-repeat}
.vsplit:hover,.vsplit:active{background:linear-gradient(var(--accent),var(--accent)) center/2px 100% no-repeat}
.pane{background:var(--paper-raise);border:1px solid var(--rule);border-radius:3px;padding:12px 16px;min-width:0}
.panehead{font-family:var(--sans);font-size:10.5px;font-weight:700;letter-spacing:.1em;text-transform:uppercase;
          color:var(--ink-faint);margin-bottom:8px;border-bottom:1px solid var(--rule);padding-bottom:5px}
/* 自然语言 = 衬线;形式化/代码 = 等宽(对开的关键对比) */
#nl,#nlproof,.clonl{font-family:var(--serif);font-size:15px;line-height:1.72;color:var(--ink)}
.chip{display:inline-block;font-size:10.5px;border-radius:2px;padding:1px 8px;margin-left:6px;font-weight:600}
.chip.ok{background:var(--s-perfect-bg);color:var(--s-perfect);border:1px solid var(--s-perfect)}
.chip.fail{background:var(--s-mfail-bg);color:var(--s-mfail);border:1px solid var(--s-mfail)}

/* 证明双栏 + 折叠 */
.proofrow{display:grid;gap:16px;margin-top:12px;align-items:start;
          grid-template-columns:minmax(0,var(--nlfr,1fr)) minmax(0,var(--flfr,1fr))}
details.fold{background:var(--paper-raise);border:1px solid var(--rule);border-radius:3px;padding:7px 14px;min-width:0}
details.fold summary{cursor:pointer;font-family:var(--sans);font-size:11px;font-weight:700;letter-spacing:.06em;
                     text-transform:uppercase;color:var(--ink-faint);user-select:none}
details.fold[open] summary{margin-bottom:8px;color:var(--ink-soft)}
details.fold pre{overflow-x:auto}

/* 节点状态卡 / 语义闭包卡 / 复核卡 = 注记框(figure/note) */
.statusbox,.closurebox,.reviewbox{border:1px solid var(--rule-2);border-radius:3px;
          background:var(--paper-raise);padding:14px 16px;margin-top:16px}
.reviewbox{background:var(--paper)}
.strow{font-size:13px;padding:3px 0;display:flex;align-items:baseline;gap:8px}
.stlabel{display:inline-block;min-width:9.5em;color:var(--ink-faint);font-size:11.5px;font-weight:600;
         letter-spacing:.02em;text-transform:uppercase}
.stok{color:var(--s-perfect);font-weight:700}
.stbad{color:var(--s-mfail);font-weight:700}
.stwarn{color:var(--s-major);font-weight:700}
.stna{color:var(--ink-faint);font-weight:700}

.clolink{font-family:var(--mono);font-size:13px;font-weight:600;color:var(--accent);cursor:pointer}
.clolink:hover{text-decoration:underline}
/* 闭包气泡:左粗边=判定状态染色,内层 NL|FL 对照 */
.clositem{border:1px solid var(--rule);border-left:4px solid var(--rule-2);border-radius:3px;
          padding:9px 12px;margin:9px 0;background:var(--paper-raise)}
.clositem.ext{border-style:dashed;opacity:.62}
.clositem.state-machine-ok{border-left-color:var(--s-mok);background:var(--s-mok-bg)}
.clositem.state-machine-fail{border-left-color:var(--s-mfail);background:var(--s-mfail-bg)}
.clositem.state-machine-none{border-left-color:var(--s-mnone)}
.clositem.state-Perfect{border-left-color:var(--s-perfect);background:var(--s-perfect-bg)}
.clositem.state-Minor{border-left-color:var(--s-minor);background:var(--s-minor-bg)}
.clositem.state-Major{border-left-color:var(--s-major);background:var(--s-major-bg)}
.clositem.state-Uncertain{border-left-color:var(--s-uncertain);background:var(--s-uncertain-bg)}
.clohead{display:flex;align-items:center;gap:6px}
.clohead .kindbadge{font-size:9.5px;padding:0 6px;vertical-align:0}
.clopair{display:grid;gap:12px;margin-top:8px;align-items:start;
         grid-template-columns:minmax(0,var(--nlfr,1fr)) minmax(0,var(--flfr,1fr))}
.clopane{background:rgba(255,255,255,.6);border:1px solid var(--rule);border-radius:3px;
         padding:7px 10px;font-size:13px;min-width:0;overflow-x:auto}
.clopane pre{font-size:12px}
.alignment-intro{max-width:78em;margin:0 0 14px;color:var(--ink-soft);line-height:1.7}
.card-technical{margin:0 0 11px;color:var(--ink-faint);font-size:12px}
.card-technical summary{cursor:pointer;user-select:none}
.card-technical .meta{padding:7px 0 2px;overflow-wrap:anywhere}
.alignment-item{min-width:0;padding:4px 0}
.alignment-item+.alignment-item{border-top:1px solid var(--rule);margin-top:13px;padding-top:15px}
.alignment-item-head{display:flex;align-items:center;flex-wrap:wrap;gap:7px;margin-bottom:10px;min-width:0}
.alignment-item-head .kindbadge{vertical-align:0}
.alignment-item-head>b{font-size:12px;overflow-wrap:anywhere}
.alignment-location{margin-left:auto;color:var(--ink-faint);font:11px var(--mono);overflow-wrap:anywhere}
.alignment-natural-text{font-family:var(--serif);line-height:1.75}
.alignment-formal-code{max-height:none;line-height:1.5}
.alignment-proof{margin-top:10px}
.closure-explain{font-size:12.5px;line-height:1.55;color:var(--ink-faint);margin:4px 0 10px}
.closure-subhead{font-family:var(--sans);font-weight:700;font-size:11px;letter-spacing:.06em;
                 text-transform:uppercase;color:var(--ink-faint);border-top:1px solid var(--rule);
                 margin-top:16px;padding-top:13px}
.formal-object{border:1px solid var(--rule);border-radius:3px;margin:9px 0;background:var(--paper)}
.formal-object summary{display:flex;align-items:center;gap:7px;cursor:pointer;padding:9px 11px;
                       font-family:var(--sans);min-width:0}
.formal-object[open] summary{border-bottom:1px solid var(--rule)}
.source-index{font:600 10px var(--mono);color:var(--ink-faint)}
.rolebadge{font:600 9.5px var(--mono);padding:1px 6px;border-radius:10px;
           background:var(--accent-soft);color:var(--accent)}
.formal-fqn{font-family:var(--mono);font-size:12px;overflow-wrap:anywhere}
.formal-source-meta{padding:7px 11px 0;font:11px var(--mono);color:var(--ink-faint);overflow-wrap:anywhere}
.formal-source-code{max-height:none;overflow:auto;padding:10px 11px;margin:0;font-size:12px;line-height:1.5}
.source-missing{margin:8px 0;padding:9px 11px;border:1px dashed var(--s-major);border-radius:3px;
                color:var(--s-major);font-size:12px}
.semantic-closure>summary{cursor:pointer}
.binding-groups{display:grid;grid-template-columns:minmax(0,2fr) minmax(220px,1fr);gap:14px}
.binding-fqn{margin:7px 0;padding:7px 9px;border:1px solid var(--rule);border-radius:3px;background:var(--paper);overflow-wrap:anywhere}
.binding-group-evidence>summary,.semantic-external-group>summary,.proof-axioms>summary{cursor:pointer}
.semantic-v10-detail{padding:9px 11px;font-size:12px;line-height:1.7}.semantic-v10-detail code{overflow-wrap:anywhere}
.semantic-none{color:var(--ink-faint)}
.semantic-open-hint,.semantic-loading{padding:11px;color:var(--ink-faint);font-size:12px}
.semantic-comparison{padding:0 11px 11px;margin-top:0}
.semantic-pane-title{margin:-1px -3px 9px;padding-bottom:7px;border-bottom:1px solid var(--rule);
                     color:var(--ink-soft);font:700 11px var(--sans);letter-spacing:.05em;text-transform:uppercase}
.semantic-nl-pane,.semantic-lean-pane{height:100%}
.semantic-nl-head{display:flex;align-items:baseline;justify-content:space-between;gap:10px;margin-bottom:6px}
.semantic-node-link{appearance:none;border:0;background:none;padding:0;text-align:left}
.semantic-nl-loc{color:var(--ink-faint);font:10.5px var(--mono)}
.semantic-nl-text{font-family:var(--serif);line-height:1.7}
.semantic-lean-pane .formal-source-meta{padding:0 0 7px}
.semantic-lean-pane .formal-source-code{max-height:480px;padding:9px;margin:0;background:var(--paper-sink)}
.semantic-external-group{margin-top:13px;border-top:1px solid var(--rule);padding-top:11px;color:var(--ink-faint);font-size:12px}
.semantic-external-list{display:grid;gap:5px;max-height:240px;overflow:auto;padding:4px 0}
.semantic-external-list code{display:block;overflow-wrap:anywhere}
.proof-trust-summary{display:flex;align-items:center;gap:9px;padding:9px 11px;border-radius:3px;background:var(--paper-sink);font-size:13px}
.proof-trust-summary>span{display:grid;place-items:center;width:20px;height:20px;border-radius:50%;font-weight:800}
.proof-trust-summary.clean{background:var(--s-perfect-bg);color:var(--s-perfect)}.proof-trust-summary.clean>span{background:var(--s-perfect);color:#fff}
.proof-trust-summary.risk{background:var(--s-mfail-bg);color:var(--s-mfail)}.proof-trust-summary.risk>span{background:var(--s-mfail);color:#fff}
.proof-trust-summary.pending{color:var(--ink-soft)}.proof-trust-summary.pending>span{background:var(--ink-soft);color:#fff}
.proof-axioms{margin-top:10px;font-size:12px}.proof-axiom{display:flex;gap:8px;align-items:center;padding:6px 0;border-top:1px solid var(--rule)}.proof-axiom code{flex:1;overflow-wrap:anywhere}.axiom-proof-decision{font:600 11px var(--mono)}
@media (max-width:900px){.binding-groups,.semantic-comparison{grid-template-columns:1fr}}
.semantic-nl-item+.semantic-nl-item{border-top:1px solid var(--rule);margin-top:9px;padding-top:9px}
.comment-candidate-label{font:700 11px var(--sans);color:var(--s-major);margin-bottom:6px}

/* 底部打档条(固定) */
#judgebar{position:sticky;bottom:0;z-index:5;display:flex;flex-wrap:wrap;align-items:center;gap:8px;
          margin-top:20px;padding:10px 14px;border-radius:3px;
          background:var(--paper-sink);border:1px solid var(--rule-2);border-top-width:2px;
          box-shadow:0 -6px 16px -12px rgba(60,50,30,.28)}
#judgebar b{font-family:var(--mono);font-size:12px;color:var(--ink-soft);margin-right:6px}
#judgebar textarea{flex:1 1 100%;min-height:36px;margin-top:2px}
#jb-status{min-width:6em;font-size:12px;font-weight:650}
#jb-status.saving{color:var(--accent)}
#jb-status.save-ok{color:var(--s-perfect)}
#jb-status.save-fail{color:var(--s-mfail)}
#judgebar.is-saving{cursor:progress}
#judgebar.is-saving button.v{cursor:progress;opacity:.68}
.review-help{font-size:13px;line-height:1.65;color:var(--ink-soft);margin-bottom:10px}

/* 四档判定按钮:选中即填对应语义色 */
button.v{font-family:var(--sans);margin:2px 4px 2px 0;padding:5px 14px;border-radius:3px;cursor:pointer;
         border:1px solid var(--rule-2);background:var(--paper-raise);color:var(--ink-soft);
         letter-spacing:.03em;transition:.12s}
button.v:hover{border-color:var(--ink-faint);color:var(--ink)}
button.v.sel{color:#fff;font-weight:600}
button.v[data-v=Perfect].sel{background:var(--s-perfect);border-color:var(--s-perfect)}
button.v[data-v=Minor].sel{background:var(--s-minor);border-color:var(--s-minor)}
button.v[data-v=Major].sel{background:var(--s-major);border-color:var(--s-major)}
button.v[data-v=Uncertain].sel{background:var(--s-uncertain);border-color:var(--s-uncertain)}
textarea{width:100%;min-height:40px;margin-top:6px;font-family:var(--sans);font-size:13.5px;
         color:var(--ink);background:var(--paper-raise);border:1px solid var(--rule-2);
         border-radius:3px;padding:8px 10px;line-height:1.55;resize:vertical}
textarea:focus{outline:none;border-color:var(--accent);box-shadow:0 0 0 2px var(--accent-soft)}
.saved{color:var(--s-perfect);font-size:12px;margin-left:8px}

/* 原子块 + 历史 */
.atom{border:1px solid var(--rule);border-radius:3px;padding:12px;margin:12px 0;background:var(--paper-raise)}
.atom.active{border-color:var(--accent);box-shadow:0 0 0 2px var(--accent-soft)}
.atom b{font-family:var(--mono);color:var(--ink)}
.hist{font-size:12px;color:var(--ink-faint);margin-top:8px;border-top:1px dashed var(--rule-2);padding-top:5px}
.hist .eff{color:var(--ink);font-weight:600}
.hist .stale{text-decoration:line-through;opacity:.55}
.stalebadge{font-size:10px;color:var(--s-major);border:1px solid var(--s-major);border-radius:3px;
            padding:0 4px;margin-left:3px;text-decoration:none;display:inline-block}
.h-Perfect{color:var(--s-perfect)}.h-Minor{color:var(--s-minor)}
.h-Major{color:var(--s-major)}.h-Uncertain{color:var(--s-uncertain)}

/* ============================== 代码 / Lean / TeX ============================== */
pre{font-family:var(--mono);background:var(--paper);border:1px solid var(--rule);
    padding:10px 12px;border-radius:3px;overflow-x:auto;font-size:12.5px;line-height:1.5;margin:0;color:var(--ink)}
.lean{font-family:var(--mono)}
.lean .k{color:var(--accent);font-weight:600}          /* 关键字 */
.lean .c{color:#8a8471;font-style:italic}              /* 注释 */
.lean .s{color:#4b7355}                                /* 字符串 */
.lean .n{color:#9a5b2e}                                /* 数字 */
.lean .t{color:var(--s-uncertain)}                     /* 类型 */
.lean .bad{color:var(--s-mfail);font-weight:700}       /* sorry/错误 */
.lean .mk{color:#8a5a8f;font-weight:600}               /* 标记 */
.env{border-left:3px solid var(--rule-2);margin:10px 0;padding:8px 14px;
     background:var(--paper-raise);border-radius:0 3px 3px 0}
.env-proof{border-left-color:var(--rule);background:var(--paper);color:var(--ink-soft)}
.envlabel{font-family:var(--serif);font-variant:small-caps;font-weight:600;color:var(--ink-soft);margin-right:8px}
.noderef{font-family:var(--mono);font-size:.9em;background:var(--paper-sink);
         border:1px solid var(--rule);border-radius:3px;padding:0 4px;color:var(--ink-soft)}

/* ============================== DAG 图视图 ============================== */
/* 注:节点填充色内联在 app.js(v1 未 fork,保持旧色),此处只主题化能主题化的部分:
   底色 / 边 / 描边 / 文字。节点色待 app-paper.js 落地后统一切换。 */
#graphwrap{flex:1;display:flex;flex-direction:column;min-width:0}
#graphwrap[hidden]{display:none}
#graphbar{flex-shrink:0;display:flex;align-items:flex-start;gap:8px 18px;flex-wrap:wrap;
          padding:8px 16px;font-size:12px;color:var(--ink-soft);
          background:var(--paper-sink);border-bottom:1px solid var(--rule-2)}
.graph-guide{display:flex;flex-direction:column;gap:2px;min-width:min(100%,470px)}
#graph-summary{font-weight:650;color:var(--ink)}
.graph-controls{display:flex;align-items:center;gap:5px}
.graph-controls button{padding:3px 9px!important;min-width:30px}
.glegend{display:flex;align-items:center;gap:7px 14px;flex-wrap:wrap}
.gl{display:inline-flex;align-items:center;gap:5px;white-space:nowrap}
.gshape{display:inline-block;width:16px;height:11px;border:1.5px solid var(--ink-soft);
        background:var(--paper-raise);box-sizing:border-box}
.gshape.axiom{width:11px;height:11px;transform:rotate(45deg)}
.gshape.definition{border-radius:1px}
.gshape.provable{border-radius:50%}
.gshape.helper{border-radius:6px}
.gmatch{display:inline-grid;place-items:center;width:17px;height:17px;border-radius:50%;
        box-sizing:border-box;font:700 11px/1 var(--sans);font-style:normal}
.gmatch.matched{color:#1f7a50;background:#e8f6ee;border:1px solid #63a986}
.gmatch.missing{color:#9a6416;background:#fff4d9;border:1px solid #c49545}
#graph{flex:1;overflow:hidden;cursor:grab;background:var(--paper)}
#graph:active{cursor:grabbing}
#graph svg{display:block;width:100%;height:100%}
.gnode{cursor:default}
.gnode.reviewable{cursor:pointer}
.gnode text{font-family:var(--mono);font-size:11px;pointer-events:none;fill:var(--ink)}
.gnode .match-badge.matched{fill:#e8f6ee;stroke:#2d8a5d;stroke-width:1.2}
.gnode .match-badge.missing{fill:#fff4d9;stroke:#a87320;stroke-width:1.2}
.gnode .match-symbol{font-family:var(--sans);font-size:11px;font-weight:750}
.gnode .match-symbol.matched{fill:#1f7a50}
.gnode .match-symbol.missing{fill:#925d10}
.gnode .judgment-symbol{font-family:var(--sans);font-size:10px;font-weight:750}
.gnode.checksbad .shape{stroke:var(--s-mfail)!important;stroke-width:2.5}
.gnode.cur .shape{stroke:var(--accent)!important;stroke-width:3}
.gnode.reviewable:focus{outline:none}
.gnode.reviewable:focus .shape{stroke:var(--accent)!important;stroke-width:2.5}
.gedge{fill:none;stroke:var(--rule-2);stroke-width:1.2}
.gedge-arrow{fill:var(--rule-2)}
.gedge.hot{stroke:var(--accent);stroke-width:2}
.gedge.dim{opacity:.08}.gnode.dim{opacity:.18}.gnode.context .shape{stroke-width:2}
.glayer rect{fill:var(--paper-sink);opacity:.42}
.glayer.odd rect{fill:var(--paper-raise);opacity:.62}
.glayer text{font:600 11px var(--sans);fill:var(--ink-faint);letter-spacing:.04em}

/* ============================== 帮助浮层 ============================== */
/* z-index 必须高于 #judgebar(z-5):判定条现吸底铺满 #main,会盖住右下角提示;
   抬到 z-20 让提示/面板始终浮于判定条之上,可见且可点。做成小药丸按钮以明确「可点」。 */
#helphint{position:fixed;right:18px;bottom:16px;z-index:20;color:var(--ink-soft);font-size:12px;
          cursor:pointer;user-select:none;padding:3px 10px;border-radius:14px;
          background:var(--paper-raise);border:1px solid var(--rule-2);
          box-shadow:0 2px 10px -5px rgba(60,50,30,.4)}
#helphint:hover{color:var(--accent);border-color:var(--accent);background:var(--accent-soft)}
#help{position:fixed;right:18px;bottom:16px;display:none;z-index:20;cursor:pointer;
      background:var(--paper-raise);color:var(--ink);border:1px solid var(--rule-2);
      border-radius:4px;padding:14px 18px;font-size:13px;line-height:1.85;
      box-shadow:0 8px 30px -10px rgba(60,50,30,.35)}
#help b{font-family:var(--serif)}
kbd{font-family:var(--mono);font-size:11.5px;background:var(--paper-sink);color:var(--ink-soft);
    border:1px solid var(--rule-2);border-bottom-width:2px;border-radius:3px;padding:0 5px}

/* ============================== 窄屏:双栏塌成单栏 ============================== */
@media (max-width:1100px){
  .pairbox{grid-template-columns:1fr}.vsplit{display:none}
  .proofrow,.clopair{grid-template-columns:1fr}
  #main{padding:20px 16px 0}   /* 底部 0:同上,勿抬 sticky 判定条 */
}