proof-checker

证明检查器：严谨的数学验证与修复

每个审阅环节开始前，请遵循 可选审阅者： 解析调用 → .aris/reviewer.json → Claude Code 默认值（Codex MCP）， 并通过规范的辅助解析器调用 reviewer_route.py，保留此环节的层级、新上下文、源文件／图像输入和确定性门控。 下方的 Codex 示例／固定配置仅适用于 backend=codex；其他路由使用各自的首次调用／回复约定。保存路由和实际返回的身份； 不可用的选项记为 REVIEW_UNAVAILABLE。根据实际的系列／完成状态／范围判定是否接受。 将调用中的审阅者／模型／推理强度覆盖项传递给包含审阅者的子任务。生成工作线程保持不变。

🔒 不要将此技能包装在 /loop、/schedule 或 CronCreate 中。 它会给出判定结果——在多轮审阅中判断证明是否有效，并通过 codex-reply 将审阅者的记忆从阶段 1 传递到阶段 3，以便审阅者检查修复是否确实弥补了它指出的缺陷。外部计时器每次触发都会从头开始，建立新的线程并丢失这些记忆。应安排它之前的外部等待，而不是安排判定过程。请参阅 shared-references/external-cadence.md。

通过跨模型对抗性审阅，系统地验证数学证明，修复已发现的缺陷，反复审阅直至达成一致，并生成包含证明义务核算的详细审计报告。

上下文：$ARGUMENTS

常量

• MAX_REVIEW_ROUNDS = 3
• REVIEWER_MODEL = gpt-6-astra — Codex 后端的默认模型，推理强度为 ultra（深度审计层级；根据 shared-references/reviewer-routing.md，能力回退顺序为 gpt-6-astra+xhigh，然后从 gpt-6.1-sol+xhigh 开始的模型能力回退，仅限能力错误——绝不低于 xhigh）。手动后端使用用户选择的模型，但必须是 ARIS 能够分类的非 Claude 模型（OpenAI、Google、DeepSeek、Moonshot/Kimi、Qwen）——执行者是 Claude，因此将证明审阅路由到任何 Claude 产品都会导致 Claude 审阅 Claude，违反跨模型不变量（参见 shared-references/reviewer-routing.md）。
• REVIEWER_BACKEND = codex — 默认值：Codex MCP（ultra）。通过 — reviewer: oracle-pro 覆盖为 Oracle MCP，或通过 — reviewer: manual 覆盖为 Manual Review MCP。如果 manual-review MCP 不可用，则停止并打印安装命令；不要回退到 Codex。参见 shared-references/reviewer-routing.md。

审稿调用约定

调用审稿器时，根据 REVIEWER_BACKEND 进行分支：

如果 REVIEWER_BACKEND = codex： 对新的审稿线程使用 mcp__codex__codex （model: gpt-6-astra，config: {"model_reasoning_effort": "ultra"}）。 对后续轮次使用 mcp__codex__codex-reply（复用 threadId）。

如果 REVIEWER_BACKEND = manual： 对新的审稿线程使用 mcp__manual_review__review，并提供： prompt: [与将发送给 Codex 的提示词完全相同] config: {"model_reasoning_effort": "xhigh", "executor_model": "", "require_reviewer_model": true} 保存返回的 threadId。 对后续轮次使用 mcp__manual_review__review_reply，并提供： threadId: [已保存的 manual-review threadId] prompt: [后续提示词] config: {"model_reasoning_effort": "xhigh", "executor_model": "", "require_reviewer_model": true}

提示词一致性：发送给人工审稿器的提示词必须与 Codex 收到的文本完全相同。 审稿追踪同样适用于这两种后端。

• AUDIT_DOC：论文目录根目录下的 PROOF_AUDIT.md，与 main.tex 同级（通过 /paper-writing 调用时，此文件位于 paper/PROOF_AUDIT.md，且为累积日志）
• REPORT_TEX：proof_audit_report.tex（正式的前后对比 PDF）
• STATE_FILE：PROOF_CHECK_STATE.json（用于恢复）
• SKELETON_DOC：PROOF_SKELETON.md（微型论断清单）
• RENDER_HTML = true — 当为 true（默认值）时，在工作流结束时通过 /render-html 将 PROOF_AUDIT.md 自动渲染为 HTML。使用完整 Codex 审查门槛（审计类文档——数学内容密集；渲染一致性检查可防止 MathJax 渲染错误，并符合该技能的跨模型审计不变量）。设为 false 可跳过，或传入 — render html: false。

验收门槛（客观标准，取代主观评分）

满足以下所有条件时，证明即通过：

1. 没有未解决的 FATAL 或 CRITICAL 问题
2. 每个定理/引理都具备：(i) 明确的假设；(ii) 对所有交换操作均给出论证的证明；(iii) 在清单中核实每次应用均满足假设
3. 所有大 O/Θ/o 陈述均声明参数依赖性和一致性范围
4. 对所有关键引理执行反例检查（即使未找到反例，也记录候选项）

问题分类（20 个类别，分为 4 组）

A 组：逻辑与证明结构

类别	描述	示例
UNJUSTIFIED_ASSERTION	未经证明或引用便提出论断	“Hessian 分解为 Gram 块”
UNPROVEN_SUBCLAIM	“显然”/“由此可得”掩盖了非平凡引理	未经核查便声称“由对称性可知交叉项为零”
QUANTIFIER_ERROR	∀/∃ 的顺序错误，遗漏“对充分小的 κ”	“对所有 π，存在 ε”与“存在 ε，使其对所有 π 成立”
IMPLICATION_REVERSAL	将 (A⇒B) 当作 (B⇒A) 使用，或仅证明一个方向却声称等价
CASE_INCOMPLETE	遗漏边界/退化情形	奇异协方差、权重为零、argmin 不唯一
CIRCULAR_DEPENDENCY	引理依赖于反过来依赖该引理的定理
LOGICAL_GAP	某一步骤缺乏前文依据	未分析 W，便从 B=Θ(1) 推出 β_K=0

B 组：分析与测度论

类别	描述	示例
ILLEGAL_INTERCHANGE	未使用 DCT/MCT/Fubini 定理便交换极限/期望/导数/积分	在没有支配条件的情况下对 E 求导
NONUNIFORM_CONVERGENCE	将逐点收敛当作一致收敛使用	交换 sup 与极限
MISSING_DOMINATION	引用了 DCT，却未给出支配函数
INTEGRABILITY_GAP	使用 E	X
REGULARITY_GAP	使用了可微性/Lipschitz 性/凸性，却未予以确立
STOCHASTIC_MODE_CONFUSION	混淆几乎必然收敛/依概率收敛/L² 收敛/期望收敛

C 组：模型与参数跟踪

类别	描述	示例
MISSING_DERIVATION	使用了某个量，但从未由模型推导得出	风险泛函中的 B、W 未定义
HIDDEN_ASSUMPTION	证明中暗中使用了定理中未列出的条件	假设具有高斯性，但未说明
INSUFFICIENT_ASSUMPTION	假设不足以支持证明（存在反例）	允许二点分布的矩条件
DIMENSION_TRACKING	未明确说明参数（d、n、K 等）如何影响结果	d 仅通过 κ 进入
NORMALIZATION_MISMATCH	坐标或缩放约定不一致	重缩放坐标与原始坐标
CONSTANT_DEPENDENCE_HIDDEN	“C”依赖于 d、n、K，但却被视为通用常数

D 组：范围与结论

类别	描述	示例
SCOPE_OVERCLAIM	结论的表述范围超出证明所能支持的范围	仅有一般重叠时却声称“β_K=0”
REFERENCE_MISMATCH	在引用定理的应用位置，未验证其假设

双轴严重性体系

轴 A — 证明状态（问题所在）

状态	含义
INVALID	按当前表述，该陈述为假（存在反例或矛盾）
UNJUSTIFIED	该陈述可能为真，但当前证明未能证明它
UNDERSTATED	只有加强假设后才为真
OVERSTATED	只有弱化结论或添加限定条件后才为真
UNCLEAR	符号含义或定义发生变化，导致表述含糊（本身不一定有错）

轴 B — 影响（影响范围）

影响	含义
GLOBAL	破坏主定理或核心依赖链
LOCAL	影响次要结果，但不影响主定理
COSMETIC	仅影响表述

严重性标签（推导结果）

标签	定义
FATAL	INVALID + GLOBAL
CRITICAL	(INVALID + LOCAL) 或 (UNJUSTIFIED + GLOBAL)
MAJOR	(UNJUSTIFIED + LOCAL) 或 (UNDERSTATED/OVERSTATED + GLOBAL)
MINOR	清晰度、符号或维度记录方面的问题，不会改变结论

常见定理的附加条件检查清单

证明调用下列任一项时，必须明确验证列出的所有条件：

定理	所需条件
DCT（控制收敛定理）	几乎处处逐点收敛 + 可积的控制函数
MCT（单调收敛定理）	单调递增 + 非负
Fubini/Tonelli	乘积可测性 + 可积性（Fubini）或非负性（Tonelli）
Leibniz 积分法则	被积函数连续 + 导数存在控制函数
隐函数定理	连续可微 + 雅可比矩阵非奇异
带余项的 Taylor 展开	充分可微 + 余项形式（Lagrange 型/积分型）
Jensen 不等式	函数凸性 + 可积性
Cauchy-Schwarz	内积空间正确 + 两个因子均可积
Weyl/Davis-Kahan	对称性/厄米性 + 满足扰动界条件
解析延拓	定义域连通 + 满足恒等定理条件
不失一般性（WLOG）约化	所声称的对称性下具有不变性 + 约化可逆

工作流

阶段 0：准备

1. 定位证明：找到主要的 .tex 文件。
2. 通读证明：提取所有定理、引理、命题、推论、定义和假设的列表。
3. 阅读参考资料：参考论文、先前结果。
4. 构建章节映射：带行号和关键结论的结构化列表。
5. 确定主定理：核心结果、假设和结论。

阶段 0.5：证明义务台账

限制扇出——并行构建台账；绝不并行判定。 派发前，冻结可通过机械方式枚举的源单元 ID：文件片段、 章节、定理／引理／命题块，或带有稳定源锚点的证明环境。按源顺序 排序，并将其划分为不超过 max_shards: 8 个分片。每轮运行不超过 max_concurrency: 4 个分片，每个叶节点最多运行 max_turns: 8 轮。 先从这些单元中发现义务，再仅在提取后为其分配确定性 ID；ID 由源单元 ID 加稳定序号或锚点构成（例如 THM-3:OB-004）。

• Tier 1（工作流）：为每个分片显式选择 aris-fanout-leaf。
• Tier 2（Agent）：仅调用 Agent(aris-fanout-leaf)。
• Tier 3：按顺序处理同一批冻结分片。失败、格式错误或超时的分片， 执行端最多允许进行一次顺序回退，绝不使用替代 Agent。

这遵循 shared-references/fan-out-pattern.md。 叶节点提示词会重复指定分配的 ID、禁止委派、只读、不得下结论以及输出架构等规则，因为工作节点不会继承此技能。

两条硬性规则：

1. 分片负责提取，不负责裁定。 构建台账（盘点义务、标注符号类型、用显式量词重述）属于结构化提取。某个证明步骤是否有效，属于 B 类正确性判定，应由第 1 阶段／第 3 阶段的跨模型评审团负责。叶节点不得将微型主张标记为“已证明”或“可靠”；它只记录该义务，以及论文声称已解决该义务的位置。分片标注的 UNVERIFIED 表示论文未引用解决位置，而不是叶节点检查了数学内容并予以否定。

**分片输出：**每个叶节点返回 {shard_id, assigned_unit_ids, covered_unit_ids, status, entries, errors}。 assigned_unit_ids 和 covered_unit_ids 包含源单元 ID。条目包含在这些单元中发现的带类型台账项，每项均以确定性的提取后义务 ID 或符号键作为 dedup_key。不得只输出散文；不得包含有效性判定字段。

覆盖回执：在唯一一次允许的顺序回退后，将合并后的 covered_unit_ids 与冻结的源单元集核对。记录计划、已完成、失败和未覆盖的 ID，以及 coverage_complete。此回执仅证明源单元执行覆盖情况；它不能证明所有相关义务均已发现，也不能证明提取出的台账在数学上完整。任何源单元未覆盖，都会使证明检查结果变为 INCOMPLETE/BLOCKED，并阻止给出完整的有效性判定。

2. 全局工件是屏障检查，必须基于合并后的提取台账计算，不得逐分片计算。 只有在覆盖回执显示 coverage_complete: true 后，才运行依赖 DAG、循环检测和跨章节符号一致性检查。完整的源单元覆盖是进行这些检查的必要条件，但本身并不代表义务完整或证明有效。

构建形式化核算工件。保存到 PROOF_SKELETON.md：

1. 依赖 DAG

节点 = 定义／假设／引理／定理。边 =“使用”。检测循环（包括语义循环，即引理 A 使用了某个推论，而该推论暗中依赖 A）。

2. 假设台账

对于每个定理／引理，列出每条假设及其验证位置——也就是论文声称已解决该假设的位置指针（file:line），而不是对解决是否有效作出判断；论文未引用解决位置时标记为“UNVERIFIED”（并非在你认为数学推导失败时标记——这是评审团的职责）。追踪使用最小假设集——哪些假设实际用到了，哪些只是陈述了。

3. 类型化符号表

每个符号都必须有类型签名：

κ : scalar ∈ (0,1), depends on (d, α_t, Σ, μ)
u* : vector ∈ ℝ^d, u* = C^{-1}m
B^even : matrix ∈ ℝ^{(L+1)×(L+1)}, symmetric PSD
Ψ_v : function ℝ → ℝ, analytic in (ζ,κ), parity determined by v

标记任何含义发生变化或在不同用法中类型不一致的符号。

4. 规范化的量化陈述

对于每个定理／引理，使用显式量词、定义域和极限次序重写陈述：

∀K ≥ 3, ∀π ∈ Π_K^{ms,∘} \ E_K, ∃κ_0 > 0 such that ∀κ ∈ (0, κ_0):
  h_act^{(K,π)} = Θ(κ^{α_K^act})  [uniform in π on compact subsets]

如果无法如此精确地重述某个定理，请标记为 UNCLEAR — needs disambiguation。

5. 微主张清单

每个非平凡步骤都要改写为带编号的序贯形式微主张：

MC-17: Context: [Lemma 3.1, κ < κ_0, Z_κ has bounded moments up to order 2m+2]
       ⊢ Goal: P̂_0 is positive definite
       Rule: monomials linearly independent on support of continuous distribution
       Side-conditions: positive density near origin — claimed discharge: §B.2 (paper argues via GMM weak convergence; validity is the jury's call, not the shard's)

每个微主张都必须包含：论证规则名称 + 所需条件 + 条件据称已满足之处（指向论文声称已完成验证的位置，而非判断其有效性）。

6. 极限次序图

追踪每个渐近陈述的极限次序和一致性范围：

h_act = Θ(κ^α)  [as κ→0, uniform in π on compact subsets of Π_K, for fixed K]
τ_act ~ (b/a)n   [as n→∞, for fixed κ,K,π with x_K ≪ 1]

标记任何极限次序含糊或一致性不明确的陈述。

可选的 Lean 验证

当用户请求 Lean，或某项具体义务需要正式检查时， 将该义务及其原始假设委派给 /lean-formalize。记录检查范围、导出的 声明、陈述对齐证据、构建输出和传递依赖公理 审计，然后继续此审计。已证明的子引理只能解决对应的义务。完整的证明审计、 验收决定和规范 wiki 产物均保留在此处；嵌套的 Lean 任务仅返回证据，不会启动另一次 proof-checker 运行。常规证明检查不需要 Lean。审阅者意见一致以及未能找到反例，都不能免除证明义务。

阶段 1：首次审查（审阅者后端，超高推理强度）

使用选定的后端，提交完整证明内容以及以下检查清单。

对于 codex，调用 mcp__codex__codex，并始终固定 model: gpt-6-astra + config: {"model_reasoning_effort": "ultra"}（深度审计级别）。对于 manual，调用 mcp__manual_review__review，并使用上文审阅者调用约定中包含身份信息的配置——model、sandbox 和 cwd 仅适用于 Codex。

对两个后端都使用以下确切提示词：

    You are performing a rigorous mathematical proof review. For EVERY theorem,
    lemma, and proposition, check ALL of the following:

    ## MANDATORY CHECKS

    A. DEFINITIONS: List any symbol whose meaning is ambiguous or changes.
    B. HYPOTHESIS DISCHARGE: For each lemma/theorem APPLICATION (not statement),
       list each hypothesis and whether it was verified, with location.
    C. INEQUALITY AUDIT: For each inequality chain, verify direction, missing
       absolute values, missing conditions (convexity, PSD, integrability).
    D. INTERCHANGE AUDIT: Flag every limit/derivative/expectation/integral
       interchange. State which theorem justifies it (DCT/MCT/Fubini/Leibniz)
       and which conditions are verified/missing.
    E. PROBABILITY MODE: Track whether claims are a.s./in prob./in expectation/
       w.h.p. Ensure transitions are justified.
    F. UNIFORMITY & CONSTANTS: For every O(·), o(·), Θ(·), ≲, state whether
       it is uniform over all parameters. List hidden parameter dependence.
    G. EDGE/DEGENERATE CASES: Attempt to break each key lemma with a 1D,
       low-rank, or extreme-parameter construction.
    H. DEPENDENCY CONSISTENCY: Detect cycles or forward references to unproven
       results.

    ## OUTPUT FORMAT (per issue)
    For each issue found, provide:
    - id: sequential number
    - status: INVALID / UNJUSTIFIED / UNDERSTATED / OVERSTATED / UNCLEAR
    - impact: GLOBAL / LOCAL / COSMETIC
    - category: [from taxonomy]
    - location: section/equation/line
    - statement: what the proof claims
    - why_invalid: why this is wrong or unjustified
    - counterexample: YES (describe) / NO / CANDIDATE (describe attempt)
    - affects: which downstream results break if this is wrong
    - minimal_fix: how to fix it

    [FULL PROOF CONTENT HERE]

阶段 1 附录——--deep-fix 可选启用

如果用户在调用时传入了 --deep-fix，请在上述提示词的 OUTPUT FORMAT 区块之后追加以下区块（不要修改原始区块；新增字段仅作补充）。默认调用完全跳过此区块，并保持原始输出架构不变。

    ## DEEP-FIX OUTPUT (opt-in, only when --deep-fix is set)

    For EACH issue listed above, additionally provide a `deep_fix_plan`
    that is repair-grade — sufficient for an executor to apply the fix
    in one Edit pass without spawning a follow-up review thread:

    - issue_id: same as the issue id above
    - corrected_statement: the theorem/lemma statement as it should
      read after the fix, with explicit quantifiers, regime conditions,
      and uniformity scope (LaTeX, paste-ready)
    - changed_equations: list of {before: <LaTeX>, after: <LaTeX>}
      pairs for each equation that needs replacement
    - downstream_labels: list of \label{...} keys whose statements or
      proofs depend on this fix and must be re-checked or rewritten
    - minimal_tex_patch_plan: ordered list of concrete edits, each as
      {file: <path>, anchor_old: <unique LaTeX snippet to find>,
       replacement_new: <LaTeX to insert>}; the executor will pass
      these directly to its file-editing tool
    - closure_tests: 2-5 sanity checks the executor must run after
      applying the fix (e.g., "verify constant_dependence_diff matches
      computed value", "limit case γ→0 reduces to identity",
      "dimension count matches before/after")

    ## ALGEBRA / TYPE SANITY PASS (opt-in, only when --deep-fix is set)

    If any issue invokes Schur test, Young's inequality, Cauchy-Schwarz,
    Hölder, quadratic form, operator norm, or power counting, the
    deep_fix_plan for that issue MUST also include an `algebra_sanity`
    object:

    - dimension_table: map of {symbol: type_signature}, e.g.
      {"K(i,α)": "scalar ≥ 0",
       "‖K‖_{2→2}": "scalar ≥ 0",
       "Σ_i V_i^rem": "scalar quadratic in w"}
    - power_count: number of times each operator-norm or Schur factor
      appears on each side; flag mismatch as INVALID
    - zero_coupling_check: evaluate the expression at γ=0 (or the
      analogous degenerate point); confirm it reduces to the expected
      identity / vanishing case
    - constant_dependence_diff: list of constants whose dependence on
      (d, K, n, ...) changes between BEFORE and AFTER, with the new
      explicit dependence written out

    Be precise. The executor will apply this plan literally; vague
    prose ("strengthen the bound", "redo the Schur step") is not
    acceptable in deep-fix mode. If you cannot produce a precise plan
    for an issue, omit that issue's deep-fix block and signal the
    deep-fix path is unavailable — do NOT emit a vague plan, and do
    NOT add a deep-fix-only category (e.g. UNCLEAR_DEEP_FIX) into the
    standard issue list, since that contaminates default-call output.

带有评审结论的 manual 响应必须以 Reviewer-Model: <exact-model-id> 开头——将本会话实际运行的模型作为 executor_model 传入。缺少模型身份、身份未知或属于同一系列，都无法证明结论成立；请输出 REVIEW_UNAVAILABLE，而不是猜测。如果无法给出执行器模型的名称，则无法证明 manual 评审的跨系列声明——请在报告中说明这一点，而不要断言其成立。

保存 threadId。 解析为结构化问题列表。写入 PROOF_AUDIT.md。

阶段 1.5：反例红队测试

对于每个严重或主要问题，以及每个引入以下内容的关键引理：

• 新的不等式界
• 可识别性／唯一性声明
• 曲率／半正定（PSD）／强凸性断言
• 关于参数的一致性声明
• 收敛模式升级（逐点 → 一致，依概率 → 高概率）

系统性地尝试构造反例，方法如下：

策略	说明
维度坍缩	设 d=1 或 2，K=2，n 较小
退化情况	奇异协方差、极小权重、均值重叠、相同分量
极端分布	两点分布 ±a、有界但非次高斯分布、重尾分布
对抗性参数缩放	选取参数，使被忽略的项占主导
数值证伪	将引理转化为函数，在较小定义域上进行暴力优化

规则：仅当经过代数验证后，才标注为“已找到反例”。否则记录为“候选反例——需要验证”。

将所有尝试（无论成功与否）记录在 PROOF_AUDIT.md 中。

阶段 2：修复实现

针对每个问题，按严重程度排序（致命 → 严重 → 主要 → 次要）：

步骤 2a：选择修复策略

针对每个问题，明确选择以下策略之一：

• ADD_DERIVATION：补充缺失的证明步骤
• STRENGTHEN_ASSUMPTION：为定理陈述添加条件
• WEAKEN_CLAIM：缩小结论的适用范围
• ADD_REFERENCE：引用已知结果，并验证其条件是否适用

记录此选择——若改变定理陈述，这属于改变范围的决策。

步骤 2b：从数学上推导修复

• 完整的数学推导，而不只是断言
• 如果需要新的命题／引理，须按完整的定理—证明格式撰写

步骤 2c：用 LaTeX 实现

• 编辑 .tex 文件
• 尽可能保留现有的 \label 引用

步骤 2d：记录修复

### Fix N: [SHORT TITLE]
**Issue**: [id] [CATEGORY] — [description]
**Severity**: FATAL / CRITICAL / MAJOR / MINOR
**Status**: INVALID / UNJUSTIFIED / UNDERSTATED / OVERSTATED
**Impact**: GLOBAL / LOCAL / COSMETIC
**Fix strategy**: ADD_DERIVATION / STRENGTHEN_ASSUMPTION / WEAKEN_CLAIM / ADD_REFERENCE
**Location**: Section X, Lines Y-Z

**BEFORE**: [what the proof originally did]
**WHY WRONG**: [mathematical problem, with counterexample if applicable]
**AFTER**: [what the fix does]
**KEY EQUATION**: [central new equation]
**PROOF OBLIGATIONS ADDED**: [new conditions/lemmas introduced]
**DOWNSTREAM EFFECTS**: [which results now need re-checking]

步骤 2e：编译检查

pdflatex -interaction=nonstopmode <file>.tex 2>&1 | grep -E "Error|Warning|undefined"

阶段 3：重新审查（reviewer backend，超强推理）

继续使用选定的后端。对于 codex，使用保存的 threadId 调用 mcp__codex__codex-reply。对于 manual，使用保存的 threadId 调用 mcp__manual_review__review_reply。附上修复摘要。要求使用相同的强制检查清单。

检查验收门槛。若未达标，则重复阶段 2–3（最多 MAX_REVIEW_ROUNDS 次）。

阶段 3.5：全局闭环与独立验证

全局闭环检查

完成所有修复后，整体验证证明：

• 陈述与结论相符：证明结尾是否与定理声明完全一致（量词、常数、一致性）？
• 所有证明义务均已履行：义务 DAG 中的每个节点是否都已证明或明确假设（且定理陈述中包含该假设）？
• 情形分析覆盖完整：各情形是否划分了整个定义域，并包括边界／退化情形？
• 归纳正确性（如适用）：基础情形、归纳步骤、IH 的正确使用，以及归纳度量是否严格递减。
• 不失一般性（WLOG）归约：每个“不失一般性”是否都附带一个微型论证，证明该归约不会造成信息损失？
• 没有静默强化假设：任何强化假设的修复是否都已同步到主定理陈述中？

对致命／严重问题的修复进行独立二次审查

对于解决了致命或严重问题的任何修复，使用选定的后端，将仅包含修复后的章节（不展示此前的评审意见）提交到一个全新的审查线程。不要使用回复工具——这一步必须盲审。

对于 codex： 启动一个全新的 mcp__codex__codex 线程。 对于 manual： 启动一个全新的 mcp__manual_review__review 线程。

盲审提示词：

请先解决此审查槽；以下是 backend=codex 的示例。

[Codex:]
mcp__codex__codex:
  model: gpt-6-astra
  config: {"model_reasoning_effort": "ultra"}
  prompt: |
    Blind review of the following proof section. You have NOT seen any prior
    review or discussion. Check every step for correctness, hidden assumptions,
    illegal interchanges, and counterexamples.
    [FIXED SECTION ONLY]

如果盲审发现新问题，则重新进入阶段 2。

回归证明审计

修复后，重新运行：

• DAG 无环性检查（未引入新环）
• 对已修改结果的所有下游引理运行反例测试套件
• 假设差异报告：修复导致哪些条件变得更强或更弱？

阶段 3.6：定理重述回归检查（选择启用）

默认：跳过。现有调用方不会看到任何变化。

选择启用：调用时传入 --restatement-check。随后，该技能会在阶段 3.5（全局闭合）之后、阶段 3.9（不可恢复协议）之前运行跨位置一致性检查。

此阶段用于捕获一类特定错误，这类错误不会被阶段 3.5 的“陈述与结论匹配”检查捕获：规范定理陈述与论文其他位置的重述内容之间出现偏差（摘要表、“主要贡献”／“总结”部分、摘要、讨论、图注）。实践中常见的偏差模式包括：

• 主定理提出的是部分条件性结论（例如，“情形 A 无条件成立，情形 B 依赖假设 X”），但后面的总结却将其引用为完全无条件的版本。
• 主定理中的 κ 指数为 O(d²K²)，但常数表中写成了 O(K²)。
• 主定理的情形条件采用平方包络，但其他位置的注释仍显示一阶包络。
• 重述内容悄然省略了一个量词（“对于 $n \ge n_0$”），而证明依赖于该量词。

算法

1. 构建规范陈述表。 扫描论文中所有 *.tex 文件，查找带有 \label{...} 的 \begin{theorem} / \begin{lemma} / \begin{proposition} / \begin{corollary} 块。对于每个块，记录 (label, full_statement_text, file:line_range)。

2. 收集候选重述。 对于每个规范标签 thm:foo：

   • 每次 \Cref{thm:foo} / \ref{thm:foo} / \cref{thm:foo} 调用及其周围的两句话，作为候选重述上下文。
   • 表格（\begin{tabular} … \end{tabular}）中提及该标签、定理非正式名称或其常数的行。
   • “主要贡献”／“总结”／“主要结果”列表中的项目符号。
   • 摘要和引言中转述该定理的句子。

3. 归一化差异。 对每一组（canonical_statement, restatement_context）：

   • 移除 \, \; \! ~，规范化空白，并规范化数学模式定界符（$..$、\(..\)、行间公式与行内公式）。
   • 检测偏差特征（一个或多个）：
     • conditional_loss — 规范陈述写有“under \Cref{ass:X}”或“for w=1”，而重述省略了该条件。
     • scope_change — 大 O 指数或速率不同（O(K^2) 与 O(d^2K^2)；√n 与 n）。
     • quantifier_loss — 规范陈述中有量词（例如，“对于 $n \ge n_0$”、“对于充分小的 $\gamma$”），而重述中没有。
     • regime_envelope_change — 一阶泄漏 Cγ/(1-Δγ) 与平方包络 (Cγ/(1-Δγ))² 之间存在变化（或类似情况）。
     • constant_change — 所述数值常数不同，或参数依赖不同。
     • variable_rename — 论证中承担相同作用的符号名称不同，且没有明确说明别名。

4. 输出发现。 每个检测到的偏差都会成为 details.restatement_drift 中的一项（见下文“提交产物生成”）。严重程度默认为 MAJOR（低估／高估 + 全局）；如果偏差纯属表面形式（例如 \, 的位置），审阅者可将严重程度降为 MINOR；仅当重述内容被下游当作规范内容使用时（例如，另一处证明引用了重述版本），才可升级为 CRITICAL。

此阶段不会做什么

• 不会自动修复偏差。输出仅供参考；改写由执行者或后续的 --deep-fix 运行处理。
• 不会更改 details.issues；重述偏差会作为同级字段报告，因此读取 issues[] 的现有使用方不会遇到架构变更。
• 不会更改顶层 verdict 的判定规则。即使 restatement_drift 非空，只要其他所有证明义务均已履行，论文仍可能输出 PASS；偏差与证明正确性相互独立。（审查者可酌情将 CRITICAL 严重级别的偏差同步到 issues 列表中，作为常规问题——通常是在下游将重述版本当作规范版本使用时；但这属于针对单个问题的判断，绝非自动规则。MAJOR 或 MINOR 偏差绝不会同步到 issues。）

失败模式

如果设置了 --restatement-check，但无法完成跨位置扫描，则输出 details.restatement_drift: []，以及 details.restatement_check_status: "unavailable"，并附上一行说明原因。验证器关卡和下游技能 MUST 将 "unavailable" 与字段缺失同等处理：不阻塞。阶段 1 / 1.5 / 2 / 3 / 3.5 / 3.9 / 4 / 5 仍正常运行。以下情况会触发此回退：

• 无法读取 .tex（包含定理块的文件出现解析器 / 编码错误）。
• 标签解析不明确（例如，同一个 \label{thm:foo} 出现多次，且无法明确选出规范版本）。
• 未找到带标签的规范类定理块（算法只检查带有显式 \label{...} 的 \begin{theorem|lemma|proposition|corollary} 块；若不存在此类块，则没有可供比对的重述版本）。

阶段 3.9：不可恢复证明协议

如果在 MAX_REVIEW_ROUNDS 之后仍未达到验收关卡，则输出一份证明不可恢复报告：

1. 无法解决的阻塞性 FATAL/CRITICAL 问题最小集合
2. 按优先级排列的补救方案：(a) 弱化论断，(b) 加强假设，(c) 补充缺失的引理，(d) 重构论证
3. 证明中可能仍可复用的部分
4. 给作者的后续步骤建议

不要默默宣称成功。报告必须如实。

阶段 4：生成审计报告

生成 proof_audit_report.tex，其中包含：

1. 概览表：所有问题及其双轴严重程度、类别、修复策略和状态
2. 修复前后逻辑链：红色（修复前）→ 绿色（修复后）对比
3. 每项修复：原始证明 → 错误原因 → 反例（如有）→ 完整推导 → 剩余细节
4. 证明义务差异：之前哪些内容未经验证，现在已验证哪些内容
5. 总结：现已证明的内容 / 仍假设的内容 / 未解决的问题
6. 彩色框：修复前（红色）、修复后（绿色）、错误原因（橙色）、关键洞见（蓝色）、警告（黄色）

编译：pdflatex proof_audit_report.tex && pdflatex proof_audit_report.tex

阶段 5：状态持久化

写入 PROOF_CHECK_STATE.json：

{
  "status": "completed",
  "rounds": 2,
  "threadId": "...",
  "fatal_fixed": 0,
  "critical_fixed": 3,
  "major_fixed": 2,
  "minor_fixed": 1,
  "counterexamples_found": 1,
  "counterexample_candidates": 2,
  "acceptance_gate": "PASS",
  "timestamp": "..."
}

第 5.5 阶段：研究 Wiki 声明台账（增量功能；仅在启用 Wiki 时适用）

当且仅当存在 research-wiki/ 时，将每个顶层定理／标题记录为声明节点，以便 Wiki 的 PROVE/JUDGE 台账记录证明了什么，以及证明有多严谨。这是创建 Wiki 声明节点（claims/<slug>.md）的起点。它是仅用于检测的记录，绝非裁决：绝不会更改审计的 verdict／reason_code，不会阻止任何操作；当 verdict == NOT_APPLICABLE（无定理）或未找到 Wiki 时，则完全跳过。

声明的 status 仅表示证明状态（verified／sound-modulo-imports／refuted／unproven／drafted／retracted）。实验支持属于独立维度，由 /result-to-claim 创建的 supports／invalidates 边表示——绝不能将这些词写入 status 字段（research_wiki.py 验证器会拒绝）。

通过规范解析器（integration-contract §2）解析辅助工具。先检查 NOT_APPLICABLE（在审计运行的当前工作目录中），然后从项目根目录运行（Wiki 位于根目录；论文审计可能从 paper/ 子目录运行）。每项守卫检查失败时都会发出警告并跳过——审计已完成，不会受到影响：

grep -q '"verdict"[[:space:]]*:[[:space:]]*"NOT_APPLICABLE"' PROOF_AUDIT.json 2>/dev/null \
  && { echo "verdict NOT_APPLICABLE (no theorems); skipping claim ledger" >&2; exit 0; }
cd "$(git rev-parse --show-toplevel 2>/dev/null || pwd)" || exit 0
[ -d research-wiki ] || { echo "no research-wiki/ at project root; skipping claim ledger (audit complete)" >&2; exit 0; }
if [ -z "${ARIS_REPO:-}" ] && [ -f .aris/installed-skills.txt ]; then
    ARIS_REPO=$(awk -F'\t' '$1=="repo_root"{print $2; exit}' .aris/installed-skills.txt 2>/dev/null) || true
fi
if [ -z "${ARIS_REPO:-}" ] && [ -f "$HOME/.aris/repo" ]; then
    ARIS_REPO=$(cat "$HOME/.aris/repo" 2>/dev/null) || true
fi
WIKI_SCRIPT=".aris/tools/research_wiki.py"
[ -f "$WIKI_SCRIPT" ] || WIKI_SCRIPT="tools/research_wiki.py"
[ -f "$WIKI_SCRIPT" ] || { [ -n "${ARIS_REPO:-}" ] && WIKI_SCRIPT="$ARIS_REPO/tools/research_wiki.py"; }
[ -f "$WIKI_SCRIPT" ] || { echo "WARN: research_wiki.py not resolved; skipping claim ledger (audit unaffected)" >&2; exit 0; }

对于 PROOF_SKELETON.md 中的每个顶层定理／标题（主定理及其标题所依赖的关键引理——而非每个微小声明），将审计结果映射到诚实的声明状态：

审计结果（PROOF_AUDIT.json 的 verdict 与第 1.5 阶段的反例）	--status
verdict=PASS／all_proofs_complete，且没有标记的导入结果	verified
证明已完成，但依赖带有 [unverified-axiom] 标记的公理／导入结果	sound-modulo-imports
找到反例（第 1.5 阶段）或审阅者判定陈述为假	refuted
存在未解决的缺口（未解决的 FATAL／CRITICAL／UNJUSTIFIED，且没有反例）	unproven

绝不臆造状态：普通证明缺口应标为 unproven——绝不能标为 refuted（这会断言其为假），也不能标为 verified／drafted。然后记录（操作幂等）：

python3 "$WIKI_SCRIPT" add_claim research-wiki/ \
  --slug "<stable-theorem-id, e.g. thm-main-ub>" --name "<theorem headline>" \
  --status "<mapped status>" --provenance "<trace_path from PROOF_AUDIT.json>" \
  --statement "<canonical theorem statement>" \
  --scope "<what it does NOT say; any flagged imports>" \
  --evidence "<PROOF_AUDIT.json verdict + counterexample / obligation pointers>" \
  --update-on-exist \
  || echo "WARN: add_claim failed for <slug> (audit unaffected; fix wiki/status and re-run)" >&2

--update-on-exist 可让重新审计更新声明状态（缺口弥补后，unproven 声明会变为 verified）。--provenance 是诚信凭据（即 trace_path）；绝不能省略。

深度修复模式（选择启用）

默认：禁用。第 1 阶段审阅者会输出带有 minimal_fix 的问题（1—2 句的修复指引）；现有调用方不会看到任何变化。

选择启用：调用时传入 --deep-fix。第 1 阶段审阅者提示词会增补（而非替换）上文的 “DEEP-FIX OUTPUT” 和 “ALGEBRA / TYPE SANITY PASS” 区块，因此审阅者还会针对每个问题返回一个 deep_fix_plan：修正后的陈述、变更后的方程、下游标签列表、最小 LaTeX 补丁计划，以及闭合测试。涉及 Schur／Young／Cauchy-Schwarz／Hölder／二次型／算子范数／幂次计数的问题，还会附带一个 algebra_sanity 区块（维数表、幂次计数、零耦合检查，以及常数依赖差异）。

为何采用选择启用

默认的 minimal_fix 说明刻意保持简短——这适合常见情形：执行者只需要高层次的指引，并会另行推导补丁。若强制每次运行都生成 deep_fix_plan，会（a）使每次审阅调用的开销增加 2—5 倍；（b）导致执行者已决定弱化或延期处理的问题反复触发重新审阅；（c）改变所有现有调用方所见的 details.issues 结构。此标志可确保默认调用的行为完全不变，同时让执行者在即将立即应用修复时，能够请求可直接用于修复的输出。

启用后的效果

• Phase 1 审阅者提示词会增加深度修复和代数合理性检查模块；原有的强制检查清单或输出格式不会被删除。
• PROOF_AUDIT.json 的 details 会新增一个同级字段 deep_fix_plans（与 details.issues 并列）；请参阅下文“提交工件生成”。
• 顶层的 verdict、reason_code 和 summary 的结构和判定规则均保持不变：深度修复输出是供执行者使用的辅助工具，不会影响判定结果。
• 验证器关卡和下游技能（paper-writing Phase 6、verify_paper_audits.sh）必须将缺少 deep_fix_plans 视为唯一有效的默认状态，且不得因其存在或内容而阻止流程。

适合选择加入的情况

• 执行者打算在同一会话中应用修复，并希望跳过后续的“给我一个具体补丁”对话。
• 先前以默认模式运行时发现了一个 CRITICAL 或 MAJOR 问题，但其 minimal_fix 含糊到无法据此采取行动（例如，只说“重做 Schur 步骤”，却没有说明修正后的算子范数界）。
• 涉及大量代数推导的证明，其中包含 Schur、二次型或算子范数步骤，而审阅者在初步审查中一贯给出说明不充分的修复建议。

失败模式

仅深度修复失败绝不能污染默认的证明检查输出。以下所有情况都会输出 details.deep_fix_status: "unavailable" + details.deep_fix_plans: []（并在 details.deep_fix_note 中添加一行说明），且标准问题列表、顶层 verdict、reason_code 和 summary 均保持不变：

• 审阅者因修复需要作出其不愿作出的选择，而拒绝生成可直接用于修复的计划。
• Phase 1 审阅者调用返回的深度修复输出被截断或格式错误（无法解析增强部分）。
• 增强后的 Phase 1 调用在生成深度修复模块前超时，但除此之外返回了有效的常规证明审查结果。

验证器关卡必须将 unavailable 与字段缺失同等对待：不阻止流程。不要在 details.issues 中添加 UNCLEAR_DEEP_FIX（或任何仅与深度修复相关的）条目，因为 details.issues 是默认架构的问题列表；向其中添加深度修复专属的失败会改变未启用该标志的调用方所观察到的默认行为。

如果增强后的 Phase 1 调用严重失败，导致无法恢复常规证明审查结果（例如，审阅者线程本身出错），则仅当错误能证明调用从未执行时，才使用未增强的提示词重试一次（根据 reviewer-routing.md 中的回退链，错误须为架构／验证错误或明确的能力错误）；遇到超时、速率限制、传输错误或服务端错误时，不要盲目重试（审查可能已经运行，再次运行会重复计费），应直接进入现有的审阅者失败处理路径，并映射为顶层 ERROR 判定。

关键规则

数学严谨性

• 绝不轻信任何证明步骤。“显然”“由此可得”“由标准论证可知”都是危险信号——每一处都必须拆解成一个微主张。
• 核验假设：每次应用引理时，都要核验该处引理的每一条假设。使用上述前提条件检查清单。
• 运算交换规范：每次交换极限、期望、导数或积分的次序时，都必须引用相应定理（DCT/MCT/Fubini/Leibniz），并通过明确的控制函数或可积性证明核验其条件。
• 一致性规范：每个 O(·)/Θ(·) 都必须声明其一致适用的参数范围。暗中依赖 d、n、K 的 “O(1)” 属于 CONSTANT_DEPENDENCE_HIDDEN 问题。
• 量词规范：检查 ∀/∃ 的顺序。“当 κ 足够小时”必须说明：κ₀ 是否依赖于 K？是否依赖于 π？是否依赖于 d？
• 反例优先：在尝试弥补漏洞前，先尝试推翻它。
• 禁止 WLOG：每个“无损一般性”都必须包含证明该化简成立的明确微主张。不得无条件使用 WLOG。
• 不得静默强化假设：任何增加条件的修正，都必须将这些条件纳入定理陈述。

跨模型协议

• 执行者分析，审阅者批判：Claude 阅读证明、提出问题并实施修正。外部审阅者负责对抗性审查。
• 审阅者推理始终使用 ultra（deep-audit 层级）：不得低于 xhigh；只有 reviewer-routing.md 中的能力回退链可以降级，且仅限遇到明确的能力错误时。
• 发送完整内容：不要概述——发送实际的数学内容，以便逐行检查。
• 在单次运行中保留 threadId：在同一次顶层 /proof-checker 调用中的 Phase 3 后续轮次，使用适当的回复工具（mcp__codex__codex-reply 或 mcp__manual_review__review_reply），以便审阅者在判断修正是否弥补漏洞时保留此前问题的上下文。不同的顶层调用之间，始终开启新线程（见下文“线程独立性”）。

修正质量

• 最小修正：只修正有问题之处，不做其他改动。
• 完整推导：每项修正都必须包含完整的数学论证。
• 明确范围决策：每项修正都必须标记为 ADD_DERIVATION / STRENGTHEN_ASSUMPTION / WEAKEN_CLAIM / ADD_REFERENCE。
• 每次修正后编译：LaTeX 必须成功编译，不得有错误。

范围诚实性

• 不得夸大结论：如果修正使结果变为有条件成立，就要明确说明。
• 区分“已证明”与“假设”：审计报告必须设有明确的章节进行区分。
• 记录未解决的问题：需要后续处理的问题必须列出，不得隐瞒。

可选标志规范

• 仅在选择启用时使用 Deep-fix：绝不自动启用；绝不因 deep_fix_plans 的内容而阻塞；未传入 --deep-fix 时，现有调用方必须观察到完全相同的审阅者输出和 JSON 架构。
• 审阅者提示词扩充须为增量式：deep-fix 区块必须附加到 Phase 1 提示词中，而不能替换其中任何内容。原有的强制检查清单（A-H）和原有的逐问题 OUTPUT FORMAT 必须原样保留。
• 仅在选择启用时运行 Restatement check：只有设置了 --restatement-check 时才运行 Phase 3.6；未传入该标志时，现有调用方必须观察到完全相同的审阅者输出和 JSON 架构。
• 不得调整 Phase 顺序：启用 Phase 3.6 时，必须严格将其插入 Phase 3.5 与 3.9 之间；不得跳过其他 Phase，也不得改变其语义。
• 禁止 verdict 串扰：deep-fix 输出和 restatement_drift 均不得更改顶层 verdict 或 reason_code。存在非空 drift 或 deep-fix 计划的论文仍可通过；无论是否设置任一标志，FAIL verdict 的论文仍然为 FAIL。

输出文件

文件	内容	时间
PROOF_SKELETON.md	依赖 DAG + 假设台账 + 微型主张	阶段 0.5
PROOF_AUDIT.md	累积的逐轮审计日志	每轮更新
PROOF_AUDIT.json	机器可读的提交判定（见下文）	始终生成
proof_audit_report.tex/.pdf	正式的前后对照报告	阶段 4
PROOF_CHECK_STATE.json	用于恢复的状态	阶段 5
PROOF_AUDIT.html（及 .review.json 旁置文件）	通过 /render-html "PROOF_AUDIT.md" --json "PROOF_AUDIT.json" 自动渲染的 PROOF_AUDIT.md 单文件 HTML 视图。不阻塞——如果 /render-html 失败，审计仍视为完成；PROOF_AUDIT.{md,json} 是规范输出。	工作流结束时（当 RENDER_HTML = true，默认值）

设置 --restatement-check 时，PROOF_AUDIT.json 还会包含 details.restatement_drift 和 details.restatement_check_status；未设置该标志时会省略这两个字段。参见下文的“提交产物生成”。

提交产物生成

此技能始终会在论文目录根目录写入 PROOF_AUDIT.json（即从 /paper-writing 调用且 paper-dir 为 paper/ 时写入 paper/PROOF_AUDIT.json；独立调用时写入 <your-paper-dir>/PROOF_AUDIT.json），无论调用方是谁，也无论论文是否包含定理。不包含 \begin{theorem} / \begin{lemma} / \begin{proof} 的论文会生成判定 NOT_APPLICABLE；禁止静默跳过。paper-writing 阶段 6 和 verify_paper_audits.sh 均依赖此产物存在于 <paper-dir>/PROOF_AUDIT.json。

此产物符合 shared-references/assurance-contract.md 中的架构：

{
  "audit_skill":      "proof-checker",
  "verdict":          "PASS | WARN | FAIL | NOT_APPLICABLE | BLOCKED | ERROR",
  "reason_code":      "all_proofs_complete | minor_gaps | critical_gap | no_theorems | ...",
  "summary":          "One-line human-readable verdict summary.",
  "audited_input_hashes": {
    "main.tex":                 "sha256:...",
    "sections/4.theory.tex":    "sha256:..."
  },
  "trace_path":       ".aris/traces/proof-checker/<date>_run<NN>/",
  "thread_id":        "<codex mcp thread id>",
  "reviewer_model":   "<resolved — the model that actually ran (target: gpt-6-astra)>",
  "reviewer_reasoning": "<resolved — the effort that actually ran (target: ultra)>",
  "generated_at":     "<UTC ISO-8601>",
  "details": {
    "theorems_audited": <int>,
    "issues": [ { "id": "T1-H3", "severity": "FATAL|CRITICAL|MAJOR|MINOR",
                  "category": "quantifier|domination|...",
                  "location": "sections/4.theory.tex:L182",
                  "note": "..." }, ... ]
  }
}

可选：details.deep_fix_plans（仅在设置 --deep-fix 时）

"details": {
  ...
  "deep_fix_plans": [
    {
      "issue_id": "T1-H3",
      "corrected_statement": "<LaTeX, paste-ready>",
      "changed_equations": [{"before": "<LaTeX>", "after": "<LaTeX>"}, ...],
      "downstream_labels": ["thm:convergence", "cor:minimax", ...],
      "minimal_tex_patch_plan": [
        {"file": "sections/4.theory.tex",
         "anchor_old": "<unique LaTeX snippet>",
         "replacement_new": "<LaTeX to insert>"},
        ...
      ],
      "closure_tests": [
        "verify constant_dependence_diff matches computed value",
        "limit case γ→0 reduces to identity",
        ...
      ],
      "algebra_sanity": {
        "dimension_table": {"<symbol>": "<type_signature>", ...},
        "power_count": "<one-line check>",
        "zero_coupling_check": "<one-line check>",
        "constant_dependence_diff": "<before vs after>"
      }
    }
  ],
  "deep_fix_status": "ok" | "unavailable"
}

字段语义：

• 未设置该标志时，deep_fix_plans 和 deep_fix_status 均完全省略。默认架构不包含这两个键。
• 设置该标志且审阅者返回格式正确的计划时，deep_fix_status 为 "ok"，且 deep_fix_plans 与 details.issues 一一对应（每个计划都通过 issue_id 引用）；只有对于涉及 Schur / Young / Cauchy-Schwarz / Hölder / 二次型 / 算子范数 / 幂次计数步骤的问题，才会包含 algebra_sanity。
• 设置该标志但审阅者的输出格式错误或被截断时，deep_fix_status 为 "unavailable"，且 deep_fix_plans 为 []。下游使用方必须将 "unavailable" 与字段缺失视为相同状态：不阻塞。
• 下游使用方必须将任一字段缺失视为唯一有效的默认状态，且不得因缺失而报错。
• deep_fix_plans 是供执行器使用的辅助工具；verify_paper_audits.sh 和 paper-writing 阶段 6 不会因其内容或结构而阻塞。

可选：details.restatement_drift（仅在设置 --restatement-check 时）

"details": {
  ...
  "restatement_drift": [
    {
      "label": "thm:main",
      "canonical_location": "sections/2.setup.tex:117",
      "restatement_location": "sections/appendix.tex:1614",
      "drift_type": "conditional_loss" | "scope_change" | "quantifier_loss" |
                    "regime_envelope_change" | "constant_change" | "variable_rename",
      "canonical_excerpt": "<short LaTeX>",
      "restatement_excerpt": "<short LaTeX>",
      "severity": "MAJOR" | "MINOR" | "CRITICAL",
      "note": "..."
    }
  ],
  "restatement_check_status": "ok" | "unavailable"
}

字段语义：

• 未设置该标志时，restatement_drift 和 restatement_check_status 均完全省略。默认架构不包含这两个键。
• 设置该标志且跨位置扫描完成时，restatement_check_status 为 "ok"，restatement_drift 列出检测到的配对（未发现时可能为空）。
• 扫描失败时（见阶段 3.6 中的“失败模式”），restatement_check_status 为 "unavailable"，且 restatement_drift 为 []。
• 下游使用方必须将字段缺失或状态为 "unavailable" 视为相同的默认状态，且不得因缺失而报错。
• restatement_drift 不会更改 details.issues，也不会更改顶层 verdict 的判定规则。审阅者可以自行决定是否将严重级别为 CRITICAL 的偏差作为常规问题镜像到 details.issues 中，但这是针对单个问题的判断，并非由架构自动触发的规则。

audited_input_hashes 的范围

对实际审阅的已声明输入集进行哈希处理——即传入本次调用、包含定理的 .tex 文件——而不是整个仓库的文件并集，也不是审阅者自行报告已打开的文件子集。外部验证器会重新计算这些条目的哈希；任何不匹配都会标记为 STALE。

路径约定（必须与 verify_paper_audits.sh 一致）：键必须是相对于论文目录的路径（不要加 paper/ 前缀——验证器会以论文目录为基准解析；添加前缀会产生 paper/paper/...，导致误报为 STALE）。论文目录外的文件请使用绝对路径。

判定表

输入状态	判定	reason_code 示例
论文中没有定理／引理／证明	NOT_APPLICABLE	no_theorems
有定理，但引用的文件无法读取	BLOCKED	source_unreadable
所有证明义务均已履行，没有缺漏	PASS	all_proofs_complete
只有 MINOR 问题（符号／表述）	WARN	minor_gaps
存在任何 FATAL 或 CRITICAL 问题（逻辑缺漏、错误主张）	FAIL	critical_gap
审阅者调用失败（网络／格式错误）	ERROR	reviewer_error

仅有 MAJOR 问题时，由审阅者酌情判定为 WARN 或 FAIL，并且必须在 summary 和 details.issues 中明确说明理由。

线程独立性

每次顶层 /proof-checker 调用都会启动一个全新的审阅者线程。对于 codex，使用 mcp__codex__codex；对于 manual，使用 mcp__manual_review__review。不要在此技能的不同调用之间复用已保存的 threadId。在一次顶层调用内，使用相应的回复工具（mcp__codex__codex-reply 或 mcp__manual_review__review_reply）进行 Phase 3 后续轮次的对话——审阅者需要先前问题的上下文，才能判断修复是否确实弥补了缺漏；上述 Phase 1→3 流程也明确依赖这一点。Phase 3.5“对 FATAL／CRITICAL 修复进行独立二次审查”子步骤是单次运行中的特意例外：它必须启动一个全新线程，确保盲审者不会接触原始批评意见。

不要将先前审计的输出（PAPER_CLAIM_AUDIT、CITATION_AUDIT、EXPERIMENT_LOG）作为不同调用之间的输入——跨运行的新鲜度正是通过 shared-references/reviewer-independence.md 保持审阅者独立性的关键。

此技能本身不会阻止流程；paper-writing Phase 6 和验证器会根据 assurance 级别决定该判定是否会阻止最终定稿。

调用示例

/proof-checker "neurips_2025.tex"
/proof-checker "check the GMM generalization proof, focus on dimension dependence"
/proof-checker "verify proof in paper.tex — difficulty: nightmare"
/proof-checker "paper/main.tex --deep-fix"            # opt-in: ask reviewer to also emit repair-grade deep_fix_plans
/proof-checker "paper/main.tex --restatement-check"   # opt-in: run Phase 3.6 to detect cross-location theorem-statement drift
/proof-checker "paper/main.tex --deep-fix --restatement-check"   # both opt-ins, independent