proof-checker

Proof Checker：厳密な数学的検証と修正

🔒 このスキルを/loop、/schedule、またはCronCreateでラップしないでください。 このスキルは判定を伴います。ラウンドをまたいで証明の妥当性を判定し、Phase 1 から Phase 3 までレビュアーの記憶をcodex-reply経由で引き継ぐことで、修正が指摘された欠落を実際に解消したか確認します。外部タイマーで各ティックごとに最初から再実行すると、新しいスレッドが開始され、その記憶が失われます。判定ではなく、その前に行う外部待機をスケジュールしてください。詳しくは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-5.5+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）。Oracle MCPを使用するには— reviewer: oracle-pro、Manual Review MCPを使用するには— reviewer: manualで上書きします。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. すべての big-O/Θ/o の記述が、宣言されたパラメータ依存性と一様性の適用範囲を持つ
4. 反例パスがすべての主要な補題で実行されている（見つからなくても候補を記録する）

問題の分類体系（20 カテゴリ、4 グループ）

グループ A：論理と証明の構造

カテゴリ	説明	例
UNJUSTIFIED_ASSERTION	証明または参照なしに主張が述べられている	「ヘッセ行列はグラムブロックに分解する」
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	微分可能性・リプシッツ性・凸性が用いられているが確立されていない
STOCHASTIC_MODE_CONFUSION	a.s.／確率収束／L²／期待値収束を混同している

グループ C：モデルとパラメータの追跡

カテゴリ	説明	例
MISSING_DERIVATION	ある量が用いられているがモデルから一度も導出されていない	B、W が未定義のリスク汎関数
HIDDEN_ASSUMPTION	証明が定理にない条件を暗黙に用いている	ガウス性が仮定されているが明記されていない
INSUFFICIENT_ASSUMPTION	仮定が証明には弱すぎる（反例が存在する）	2 点分布を許容するモーメント条件
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 積分公式	被積分関数の連続性 + 導関数に対する優関数
陰関数定理	連続微分可能性 + 非特異なヤコビアン
剰余項付きテイラーの定理	十分な微分可能性 + 剰余項の形式（ラグランジュ型／積分型）
Jensen の不等式	関数の凸性 + 可積分性
Cauchy-Schwarz の不等式	適切な内積空間 + 両因子の可積分性
Weyl/Davis-Kahan	対称性／エルミート性 + 摂動境界の条件
解析接続	定義域の連結性 + 恒等定理の条件
一般性を失わない（WLOG）簡約	主張された対称性の下での不変性 + 簡約の可逆性

ワークフロー

フェーズ 0：準備

1. 証明を特定する：主要な .tex ファイルを見つけます。
2. 証明全体を読む：すべての定理／補題／命題／系／定義／仮定の一覧を抽出します。
3. 参考資料を読む：参考論文や先行研究を確認します。
4. セクションマップを作成する：行番号と重要な主張を含む構成化された一覧を作成します。
5. 主要な定理を特定する：中心となる結果、仮定、主張を確認します。

フェーズ 0.5：証明義務台帳

ファンアウト（ティア対応）— 台帳の作成は並行して行い、判定は決して並行して行わないでください。 複数の定理を含む大規模な論文では、台帳の作成は独立した節を対象に並行して行います。ティア 1（ワークフロー）：節／定理ごとに Claude サブエージェントを 1 つ起動し、その単位の記号、仮定、微小主張、局所的な量化文を抽出させ、それぞれ構造化された台帳の断片を返させます。 ティア 2：Agent ツールを使って同じサブエージェントを実行します。ティア 3：節を順番に処理します。これは shared-references/fan-out-pattern.mdに従った方法です。

2 つの厳守事項：

1. シャードは抽出を行います。裁定は行いません。 台帳の作成（証明義務の一覧化、記号の型付け、明示的な量化子を用いた言い換え）は構造的な抽出です。証明のステップが有効かどうか、すなわち証明義務が実際に果たされているかどうかは、フェーズ 1／フェーズ 3 のクロスモデル審査会（codex または手動、ultra）に委ねられる Type-B の正当性判定です。Claude のシャードは、微小主張に「証明済み」や「健全」と記してはいけません。記録するのは証明義務と、論文がそれを果たしたと主張する箇所だけです。acceptance-gate.mdを参照してください。ループによる自己検証が許されるのは、台帳が完全であることであり、証明が正しいことではありません。
   • 以下の台帳仕様の文言にも、このルールが適用されます。 成果物に「それぞれが検証される箇所」、「または未検証と記す」、「条件が証明された箇所」とある場合、シャードが記録するのは場所を示すポインター（論文が証明義務を果たしたと主張する file:line）です。シャード自身が、その証明義務の充足が数学的に有効だと判断してはいけません。シャードの UNVERIFIED は「論文が充足箇所を示していない」という意味であり、「シャードが数学を確認し、誤りだと判断した」という意味ではありません。健全性を判断するのは審査会であり、シャードではありません。

シャードの出力（fan-out-pattern.mdに従う抽出スキーマ）：各シャードは {shard_id: "<section/theorem id>", entries: [...]} を返します。内容は、その単位に属する型付きの台帳項目（記号、仮定、微小主張、標準的な文、極限の順序に関する事実）で、それぞれ標準 ID（例：MC-17、記号名）を dedup_key として持ちます。説明文のみの項目は禁止です。有効性を判定するフィールドも含めてはいけません。 2. グローバル成果物は、各シャードではなく、結合済みの台帳に対して計算するバリアです。 依存関係 DAG とその循環検出（意味上の循環を含む）、および節をまたぐ記号型の整合性を確認するには、論文全体を見渡す必要があります。まずすべてのシャードの断片を結合し、結合した全体に対してこれらを計算してください。シャードごとに 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]

定理をこれほど厳密に書き換えられない場合は、不明確 — 明確化が必要と記します。

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 は不要です。レビュアー間の合意や、反例探索で反例が見つからなかったことは、証明義務を解消しません。

Phase 1: 初回レビュー（レビュアーバックエンド、ultra 推論）

選択したバックエンドを使用し、以下のチェックリストとともに完全な証明内容を提出します。

codex の場合は、mcp__codex__codex を呼び出し、必ず model: gpt-6-astra と config: {"model_reasoning_effort": "ultra"}（詳細監査ティア）を指定します。manual の場合は、上記の Reviewer Calling Convention にある、ID を含む設定を使って 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]

Phase 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 には、このセッションで実際に動作しているモデルを渡します。ID がない、不明、または同じファミリーの ID の場合、その判定は認められません。推測せず、REVIEW_UNAVAILABLE を出力してください。executor モデルの名前を特定できない場合、manual review における異なるファミリーであるという主張は立証できません。その旨をレポートに記載し、断定しないでください。

threadId を保存します。 構造化された課題リストに解析します。PROOF_AUDIT.md に書き込みます。

Phase 1.5: 反例レッドチーム

各 CRITICAL または MAJOR の課題、および以下を導入するすべての主要な補題について、反例の構成を体系的に試みます。

• 新たな不等式の境界
• 識別可能性／一意性の主張
• 曲率／PSD／強凸性の主張
• パラメーターに関する一様性の主張
• 収束モードの格上げ（各点収束 → 一様収束、確率収束 → 高確率収束）

戦略	説明
次元の崩壊	d=1 または 2、K=2、n は小さい値に設定
退化	特異共分散、小さな重み、平均の重なり、同一成分
極端な分布	±a の二点分布、劣サブガウス分布、重い裾
敵対的なパラメーターのスケーリング	無視された項が支配的になるようパラメーターを選ぶ
数値的な反証	補題を関数に変換し、小さな定義域上で総当たり最適化する

ルール：「反例が見つかった」と記録するのは、代数的に検証できた場合に限ります。それ以外は「反例候補 — 検証が必要」として記録します。

成功したものも失敗したものも含め、試みをすべて PROOF_AUDIT.md に記録します。

Phase 2: 修正の実装

各課題について、重大度の高い順（FATAL → CRITICAL → MAJOR → MINOR）に対応します。

ステップ 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: 再レビュー（レビュアーバックエンド、超推論）

選択したバックエンドで続行します。codex の場合は、保存された threadId を指定して mcp__codex__codex-reply を使用します。manual の場合は、保存された threadId を指定して mcp__manual_review__review_reply を使用します。修正の要約を含めます。同じ必須チェックリストを要求します。

受け入れゲートを確認します。満たされていない場合は、フェーズ 2〜3 を繰り返します（MAX_REVIEW_ROUNDS まで）。

フェーズ 3.5: グローバルクロージャと独立検証

グローバルクロージャチェック

すべての修正後、証明全体を検証します：

• 主張と結論の一致: 証明は定理が主張する内容（量化子、定数、一様性）で正確に終わっていますか？
• すべての義務の解消: 義務 DAG のすべてのノードが証明されているか、明示的に仮定されていますか（そして定理の主張にそれが含まれていますか）。
• 場合分けの網羅性: 場合分けが領域を分割しており、かつ境界・退化ケースを含んでいますか。
• 帰納法の正確性（該当する場合）: 基底ケース、帰納ステップ、帰納法の仮定の正しい使用、帰納尺度が厳密に減少すること。
• WLOG 還元: 各「一般性を失うことなく」が、還元が損失なしであることを証明するマイクロ主張を生み出していますか。
• 暗黙の仮定強化の不在: 仮定を強化した修正が、主定理の主張に反映されていますか。

FATAL/CRITICAL 修正に対する独立した第二レビュー

FATAL または CRITICAL な問題を解決した修正については、修正後のセクションのみを（以前の批評を示さずに）選択したバックエンドを使用して新しいレビュースレッドに提出します。返信ツールを使用しないでください — このステップはブラインドでなければなりません。

codex の場合: 新しい mcp__codex__codex スレッドを開始します。 manual の場合: 新しい mcp__manual_review__review スレッドを開始します。

ブラインドレビューのプロンプト：

[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} の呼び出しと、候補となる再記述の文脈として、その前後2文。
   • ラベル、定理の略式名称、または定数に言及する表（\begin{tabular} … \end{tabular}）の行。
   • 「Key Contributions」 / 「Summary」 / 「Main Results」のリスト内の箇条書き。
   • 定理を言い換えている、要旨と序論の文。

3. 正規化差分。 各 (canonical_statement, restatement_context) ペアについて、以下を行います。

   • \, \; \! ~ を除去し、空白を正規化し、数式モードの区切り（$..$、\(..\)、ディスプレイ数式とインライン数式）を正規化します。
   • 次のドリフトの特徴を検出します（1つ以上）。
     • conditional_loss — 正準的な記述では「\Cref{ass:X} のもとで」または「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. 検出結果を出力します。 検出したドリフトごとに、「Submission Artifact Emission」で説明されている details.restatement_drift に項目を追加します。重大度は既定で MAJOR（UNDERSTATED/OVERSTATED + GLOBAL）です。ドリフトが純粋に表記上のものである場合（例：\, の配置）、レビュー担当者は MINOR に引き下げることができ、再記述が正準的な記述であるかのように後続処理で使われている場合に限り、CRITICAL に引き上げることができます。

このフェーズで行わないこと

• ドリフトを自動的に修正しません。出力は参考情報であり、書き換えは実行担当者または後続の --deep-fix 実行で処理します。
• details.issues は変更しません。再記述のドリフトは兄弟フィールドとして報告されるため、issues[] を読み取る既存のコンシューマーにスキーマ変更はありません。
• トップレベルの verdict 判定ルールは変更しません。証明義務がすべて別途満たされていれば、restatement_drift が空でない論文でも PASS を出力することがあります。ドリフトは証明の正しさとは独立しています。（再記述が正準的な記述であるかのように後続処理で使われている場合など、レビュー担当者は独自の判断で、CRITICAL の重大度を持つドリフトを通常の問題として issues リストに反映できます。ただし、これは問題ごとの判断であり、自動ルールではありません。MAJOR または MINOR のドリフトが issues に反映されることはありません。）

失敗時の動作

--restatement-check が設定されているものの、複数箇所にまたがるスキャンを完了できない場合は、理由を説明する1行の注記とともに details.restatement_drift: [] および details.restatement_check_status: "unavailable" を出力します。検証ゲートおよび後続のスキルは "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 軸の重大度、カテゴリ、修正方針、ステータスを含むすべての問題
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：Research 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）を使って解決します。 まず（監査を実行した場所である）cwd で 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）です。省略してはいけません。

Deep-Fix モード（オプトイン）

デフォルト：無効です。Phase 1 のレビュアーは minimal_fix（1〜2 文の指摘）を含む問題を出力します。既存の呼び出し側に変更はありません。

オプトイン：呼び出し時に --deep-fix を渡します。Phase 1 のレビュアープロンプトには、上記の「DEEP-FIX OUTPUT」および「ALGEBRA / TYPE SANITY PASS」ブロックが置き換えではなく追加されるため、レビュアーは各問題について、修正後の記述、変更した方程式、下流のラベル一覧、最小限の LaTeX パッチ計画、完了テストを含む deep_fix_plan も返します。Schur／Young／Cauchy-Schwarz／Hölder／二次形式／作用素ノルム／べき乗の計数を用いる問題には、さらに algebra_sanity ブロック（次元表＋べき乗の計数＋結合定数をゼロにした場合のチェック＋定数依存性の差分）が含まれます。

オプトインにする理由

デフォルトの minimal_fix の説明は意図的に短くしています。これは、エグゼキューターが概要レベルの指摘を求め、パッチは別途導き出す一般的なケースに適しています。すべての実行で deep_fix_plan を必須にすると、（a）レビュアーへの呼び出しが毎回 2〜5 倍に増え、（b）エグゼキューターがすでに弱めるか保留すると決めた問題について再レビューのループが発生し、（c）既存のすべての呼び出し側で details.issues の構造が変わってしまいます。このフラグを使えば、デフォルトの呼び出しでは動作を一切変えずに、修正をすぐ適用する場合はエグゼキューターが修正作業に使える出力を要求できます。

有効にした場合の効果

• Phase 1 のレビュアープロンプトに deep-fix ブロックと algebra-sanity ブロックが追加されます。元の必須チェックリストや出力形式が削除されることはありません。
• PROOF_AUDIT.json の details に、兄弟フィールド deep_fix_plans（details.issues に対応）が追加されます。以下の「提出アーティファクトの出力」を参照してください。
• トップレベルの verdict、reason_code、summary の構造と判定ルールは変わりません。deep-fix の出力はエグゼキューター向けの補助ツールであり、判定を左右するシグナルではありません。
• 検証ゲートと下流のスキル（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 に1行の注記を添えます）、標準の issue リスト、トップレベルの判定、reason_code、summary は変更しません。

• 修正に、レビュー担当者が判断したくない選択が必要となるため、レビュー担当者が修正に十分な計画の作成を拒否する。
• Phase 1 のレビュー担当者呼び出しが、切り詰められた、または不正な深い修正出力を返す（拡張セクションの解析に失敗する）。
• 拡張された Phase 1 呼び出しが、深い修正ブロックを生成する前にタイムアウトする。ただし、それ以外では有効な通常の証明レビューを返している。

検証ゲートでは、unavailable をフィールドが存在しない場合と同じように扱わなければなりません。ブロックしてはいけません。details.issues に UNCLEAR_DEEP_FIX（または深い修正のみに関する項目）を追加してはいけません。details.issues はデフォルトスキーマの issue リストであり、そこに深い修正固有の失敗を追加すると、フラグなしで利用する呼び出し元のデフォルト動作が変わってしまうためです。

拡張された Phase 1 呼び出しが、通常の証明レビューを復元できないほど深刻に失敗した場合（例：レビュー担当者のスレッド自体がエラーになった場合）は、そのエラーによって呼び出しが実行されなかったことが証明される場合に限り、拡張していないプロンプトで1回だけ再試行します（reviewer-routing.md のフォールバックチェーンに記載されているスキーマ／検証エラー、または明示的な機能エラー）。タイムアウト、レート制限、トランスポートエラー、サーバーエラーの場合は、やみくもに再試行してはいけません（レビューがすでに実行された可能性があり、二重実行すると二重に課金されます）。その場合は、既存のレビュー担当者失敗処理に直接進み、トップレベルの ERROR 判定にマッピングします。

重要なルール

数学的な厳密性

• 証明のステップを鵜呑みにしてはいけません。「明らかに」「したがって」「標準的な議論により」は危険信号です。それぞれにマイクロ主張を設ける必要があります。
• 仮定の適用確認：補題を適用するたびに、その時点で仮定を1つずつ確認してください。上記の付帯条件チェックリストを使用してください。
• 交換の規律：極限／期待値／微分／積分を入れ替える場合は、定理（DCT/MCT/Fubini/Leibniz）を明記し、支配関数または可積分性の証明を示して、その条件を満たすことを確認してください。
• 一様性の規律：すべての O(·)/Θ(·) について、一様性が成り立つパラメーターを明記してください。d,n,K に暗黙に依存する「O(1)」は、CONSTANT_DEPENDENCE_HIDDEN の問題です。
• 量化子の規律：∀/∃ の順序を確認してください。「κ が十分小さいとき」は、κ₀ が K、π、d のどれに依存するかを明記する必要があります。
• 反例を先に考える：ギャップの修正を試みる前に、まず反例を探してください。
• WLOG の禁止：「一般性を失わずに」とする場合は必ず、その簡約を証明するマイクロ主張を明示してください。根拠のない WLOG は認められません。
• 仮定を暗黙に強化しない：条件を追加する修正を行う場合は、その条件を定理の記述にも反映してください。

モデル間プロトコル

• 実行側が分析し、レビュー側が批評する：Claude が証明を読み、質問をまとめ、修正を実装します。外部レビュー担当者は敵対的なレビューを行います。
• レビュー担当者の推論は常に ultra（deep-audit tier）とします。xhigh を下回ってはいけません。明示的な機能エラーの場合に限り、reviewer-routing.md の機能フォールバックチェーンを使って段階を下げられます。
• 内容をすべて送る：要約せず、行ごとの確認ができるよう実際の数式を送ってください。
• 1回の実行内では 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 はオプトインのみ：Phase 3.6 は --restatement-check が設定されている場合にのみ実行します。このフラグを指定しない場合、既存の呼び出し元から見たレビュアーの出力と JSON スキーマは同一でなければなりません。
• Phase の順序を変更しない：Phase 3.6 を有効にすると、3.5 と 3.9 の間にのみ挿入されます。他の Phase を省略したり、その動作を変更したりすることはありません。
• 判定の干渉を起こさない：deep-fix の出力も restatement_drift も、トップレベルの verdict や reason_code を変更することはありません。ドリフトが空でない場合や deep-fix プランがある場合でも論文は合格することがあり、FAIL 判定の論文は、いずれかのフラグが設定されているかどうかにかかわらず FAIL のままです。

出力ファイル

ファイル	内容	生成タイミング
PROOF_SKELETON.md	依存関係 DAG ＋ 仮定台帳 ＋ マイクロ主張	Phase 0.5
PROOF_AUDIT.md	ラウンドごとの累積監査ログ	各ラウンドで更新
PROOF_AUDIT.json	機械可読な提出判定（下記参照）	常に生成
proof_audit_report.tex/.pdf	変更前／変更後の正式なレポート	Phase 4
PROOF_CHECK_STATE.json	復旧用の状態	Phase 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 の Phase 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 と1対1で対応します（各プランは issue_id で参照されます）。algebra_sanity は、Schur／Young／Cauchy-Schwarz／Hölder／二次形式／作用素ノルム／べき乗カウントの手順を用いる問題にのみ含まれます。
• フラグが設定されていても、レビューアーの出力が不正な形式または途中で切れている場合、deep_fix_status は "unavailable" となり、deep_fix_plans は [] になります。後続のコンシューマーは "unavailable" をフィールドが存在しない場合と同じように扱う必要があります（ブロックしません）。
• 後続のコンシューマーは、いずれかのフィールドが存在しない状態を唯一の有効なデフォルト状態として扱う必要があり、フィールドが欠落していてもエラーを発生させてはなりません。
• deep_fix_plans は実行担当者向けの参考ツールです。verify_paper_audits.sh と paper-writing Phase 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 には検出されたペアが列挙されます（該当するものがなければ空になる場合があります）。
• スキャンに失敗した場合（Phase 3.6 の「Failure mode」に従います）、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 を再利用しないでください。1回のトップレベル呼び出しの中では、適切な返信ツール（mcp__codex__codex-reply または mcp__manual_review__review_reply）を使って Phase 3 のフォローアップラウンドを同じスレッドで行います。修正によって実際に問題が解消されたか判断するには、レビュー担当者が以前の問題のコンテキストを把握している必要があり、上記の Phase 1→3 の流れもこれを明示的に前提としています。Phase 3.5 の「FATAL/CRITICAL の修正に対する独立した2回目のレビュー」サブステップは、1回の実行内で意図的に設けられた例外です。ブラインドレビュー担当者が元の批評に触れないよう、新しいスレッドを開始する必要があります。

別々の呼び出しの間で、以前の監査結果（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