Proof Checker

Proof Checker: Rigorous Mathematical Verification & Fixing

🔒 Do not wrap this skill in /loop, /schedule, or CronCreate. It is verdict-bearing — it judges proof validity across rounds, threading the reviewer's memory from Phase 1 → Phase 3 (via codex-reply/manual_review_reply, or an explicit carried issue list for self) so the reviewer can check whether a fix actually closed the gap it flagged. An external timer re-enters from the top each tick, losing that memory. Schedule the external wait that precedes it, not the verdict. See shared-references/external-cadence.md.

Systematically verify a mathematical proof via adversarial review — cross-model when a second model is available, Claude self-review otherwise — fix identified gaps, re-review until convergence, and generate a detailed audit report with proof-obligation accounting.

Context: $ARGUMENTS

Constants

• MAX_REVIEW_ROUNDS = 3
• REVIEWER_MODEL = gpt-5.6-sol — Default model for the Codex backend, reasoning effort ultra (deep-audit tier; capability fallback gpt-5.6-sol+xhigh → gpt-5.5+xhigh per shared-references/reviewer-routing.md, capability errors only — never below xhigh). Manual backend uses a model the user chooses, but it must be a non-Claude model ARIS can classify (OpenAI, Google, DeepSeek, Moonshot/Kimi, Qwen) — the executor is Claude, so routing the proof review into any Claude product makes Claude judge Claude and voids the cross-model invariant (see shared-references/reviewer-routing.md). The self backend has no REVIEWER_MODEL — it is Claude reviewing Claude's own proof by construction, which is exactly the configuration the cross-model invariant above exists to avoid; it's used only when no non-Claude model is reachable at all, and its verdicts should be read with that caveat.
• REVIEWER_BACKEND = codex — Default: Codex MCP (ultra). Override with — reviewer: oracle-pro for Oracle MCP, — reviewer: manual for Manual Review MCP, or — reviewer: self when no external model/API is configured at all. If neither Codex, Oracle, nor manual-review MCP is available, fall back to self rather than stopping — proof review is too central to this skill to silently skip. See shared-references/reviewer-routing.md.

Reviewer Calling Convention

When calling the reviewer, branch on REVIEWER_BACKEND:

If REVIEWER_BACKEND = codex: Use mcp__codex__codex for new review threads (model: gpt-5.6-sol, config: {"model_reasoning_effort": "ultra"}). Use mcp__codex__codex-reply for follow-up rounds (reuse threadId).

If REVIEWER_BACKEND = manual: Use mcp__manual_review__review for new review threads with: prompt: [exact same prompt that would go to Codex] config: {"model_reasoning_effort": "xhigh", "executor_model": "", "require_reviewer_model": true} Save the returned threadId. Use mcp__manual_review__review_reply for follow-up rounds with: threadId: [saved manual-review threadId] prompt: [follow-up prompt] config: {"model_reasoning_effort": "xhigh", "executor_model": "", "require_reviewer_model": true}

If REVIEWER_BACKEND = self: No second model is available. Follow auto-review-loop's "Self-Review Backend (No Second Model)" for the full protocol: re-read the proof fresh from disk (not from memory of writing/fixing it), apply the identical Phase 1/Phase 3 checklists below, actively try to break each theorem before accepting it, and flag any theorem you're too invested in to judge impartially. Use the same prompt content as the codex route (Phase 1's mandatory checklist, Phase 3's re-review) as the rubric Claude answers itself. There is no threadId; "follow-up round" for self just means re-reading the fixed proof fresh again rather than reasoning from the fix you just applied. This backend carries no independence guarantee — see the honest tradeoff in auto-review-loop — so treat a self PASS as weaker evidence than a codex/manual PASS, and prefer codex or manual whenever either is actually available.

Prompt fidelity: the manual prompt must be exactly the same text that Codex would receive; the self route uses the same prompt content as its own checklist. Review tracing applies equally to all backends.

• AUDIT_DOC: PROOF_AUDIT.md at the paper directory root, alongside main.tex (cumulative log; when invoked via /paper-writing, this is paper/PROOF_AUDIT.md)
• REPORT_TEX: proof_audit_report.tex (formal before/after PDF)
• STATE_FILE: PROOF_CHECK_STATE.json (for recovery)
• SKELETON_DOC: PROOF_SKELETON.md (micro-claim inventory)
• RENDER_HTML = true — When true (default), auto-render PROOF_AUDIT.md to HTML at workflow end via /render-html. Uses full review gate matching the active REVIEWER_BACKEND (audit-class artifact — math-heavy content; render-fidelity check protects against MathJax breakage and matches the skill's audit invariant). Set false to skip, or pass — render html: false.

Acceptance Gate (objective, replaces subjective scoring)

The proof passes when ALL of the following hold:

1. Zero open FATAL or CRITICAL issues
2. Every theorem/lemma has: (i) explicit hypotheses, (ii) proof with all interchanges justified, (iii) every application discharges hypotheses in the ledger
3. All big-O/Θ/o statements have declared parameter dependence and uniformity scope
4. Counterexample pass executed on all key lemmas (log candidates even if none found)

Issue Taxonomy (20 categories, 4 groups)

Group A: Logic & Proof Structure

Group B: Analysis & Measure Theory

Group C: Model & Parameter Tracking

Group D: Scope & Claims

Two-Axis Severity System

Axis A — Proof Status (what is wrong)

Axis B — Impact (how much breaks)

Severity Labels (derived)

Side-Condition Checklists for Common Theorems

When the proof invokes any of the following, require explicit verification of ALL listed conditions:

Workflow

Phase 0: Preparation

1. Locate the proof: Find the main .tex file(s).
2. Read the entire proof: Extract list of all theorems/lemmas/propositions/corollaries/definitions/assumptions.
3. Read reference materials: Reference papers, prior results.
4. Build a section map: Structured list with line numbers and key claims.
5. Identify the main theorem: Central result, assumptions, claims.

Phase 0.5: Proof-Obligation Ledger

Fan-out (Tier-aware) — build the ledger in parallel; never judge in parallel. For a large multi-theorem paper, ledger construction is breadth over independent sections. Tier 1 (Workflow): spawn one Claude subagent per section/theorem to extract that unit's symbols, assumptions, micro-claims, and local quantified statements, each returning a structured ledger fragment. Tier 2: the same subagents via the Agent tool. Tier 3: walk the sections sequentially. This follows shared-references/fan-out-pattern.md.

Two hard rules:

1. The shards EXTRACT, they do not ADJUDICATE. Building the ledger (inventorying obligations, typing symbols, restating with explicit quantifiers) is structural extraction. Whether a proof step is valid — whether an obligation is actually discharged — is a Type-B correctness verdict reserved for the Phase 1 / Phase 3 reviewer jury (codex or manual at ultra, or self when neither is available — see the Reviewer Calling Convention). A Claude shard MUST NOT mark a micro-claim "proved" or "sound"; it only records the obligation and where the paper claims to discharge it. See acceptance-gate.md — the loop may self-verify that the ledger is complete, never that the proofs are correct.
   • This governs the ledger spec wording below. Where the artifacts say "WHERE each is verified", "or mark UNVERIFIED", or "where conditions are proven", a shard records a location pointer (file:line the paper claims discharge) — never its own judgment that the discharge is mathematically valid. A shard's UNVERIFIED means "the paper cites no discharge location", NOT "the shard checked the math and it fails". Soundness is the jury's verdict, not the shard's.

Shard output (extraction schema, per fan-out-pattern.md): each shard returns {shard_id: "<section/theorem id>", entries: [...]} — the typed ledger items (symbols, assumptions, micro-claims, canonical statements, limit-order facts) for that unit, each carrying its canonical id (e.g. MC-17, the symbol name) as dedup_key. Never prose-only; never a validity verdict field. 2. Global artifacts are a barrier, computed on the merged ledger, not per-shard. The Dependency DAG and its cycle detection (incl. semantic circularity), and cross-section symbol-type consistency, require the whole paper in view. Merge all shard fragments first, then compute these on the union — a per-shard DAG would miss exactly the cross-section cycles this phase exists to catch.

Build formal accounting artifacts. Save to PROOF_SKELETON.md:

1. Dependency DAG

Nodes = Definitions / Assumptions / Lemmas / Theorems. Edges = "uses". Detect cycles (including semantic circularity where Lemma A uses a corollary that quietly depends on A).

2. Assumption Ledger

For each theorem/lemma, list every hypothesis with WHERE each is verified — i.e. the location pointer the paper claims discharges it (file:line), not a judgment that the discharge is valid; mark "UNVERIFIED" when the paper cites no discharge location (not when you believe the math fails — that is the jury's call). Track usage-minimal assumption sets — which assumptions were actually used vs merely stated.

3. Typed Symbol Table

Each symbol must have a type signature:

κ : 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

Flag any symbol whose meaning changes or whose type is inconsistent across uses.

4. Canonical Quantified Statements

For each theorem/lemma, rewrite the statement with explicit quantifiers, domains, and limit order:

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

If you cannot restate a theorem this precisely, mark it UNCLEAR — needs disambiguation.

5. Micro-Claim Inventory

Every nontrivial step becomes a numbered micro-claim in sequent form:

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)

Each micro-claim has: justification rule name + required conditions + where conditions are proven (a location pointer to where the paper claims to discharge them, not a validity judgment).

6. Limit-Order Map

Track every asymptotic statement's limit order and uniformity scope:

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]

Flag any statement where limit order is ambiguous or uniformity is unclear.

Phase 1: First Review (reviewer backend, ultra reasoning)

Submit the complete proof content with the checklist below, using the selected backend.

For codex, call mcp__codex__codex and always pin model: gpt-5.6-sol + config: {"model_reasoning_effort": "ultra"} (deep-audit tier). For manual, call mcp__manual_review__review with the identity-bearing config from the Reviewer Calling Convention above — model, sandbox and cwd are Codex-only. For self, there is no tool call: re-read the proof fresh from disk and work through the checklist below exactly as an external reviewer would, per the Reviewer Calling Convention above.

Use this exact prompt/checklist for all backends:

    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 addendum — --deep-fix opt-in

If the user passed --deep-fix on invocation, append the following block to the reviewer prompt after the OUTPUT FORMAT block above (do not modify the original block; the new fields are additive). Default invocations skip this block entirely and emit the original output schema unchanged.

    ## 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.

A verdict-bearing manual response MUST begin with Reviewer-Model: <exact-model-id> — pass the model THIS session is actually running as in executor_model. Missing, unknown, or same-family identity cannot acquit; emit REVIEW_UNAVAILABLE rather than guessing. If the executor model cannot be named, manual review's cross-family claim is unprovable — say so in the report instead of asserting it.

Save the threadId. Parse into structured issue list. Write to PROOF_AUDIT.md.

Phase 1.5: Counterexample Red Team

For each CRITICAL or MAJOR issue, and for every key lemma that introduces:

• a new inequality bound
• an identifiability/uniqueness claim
• a curvature/PSD/strong convexity assertion
• a uniform-in-parameter claim
• a convergence mode upgrade (pointwise → uniform, in prob → w.h.p.)

Systematically attempt to construct counterexamples using:

Rule: Label "counterexample found" ONLY if algebraically verified. Otherwise log as "candidate counterexample — needs verification."

Record all attempts (successful or not) in PROOF_AUDIT.md.

Phase 2: Fix Implementation

For each issue, ordered by severity (FATAL → CRITICAL → MAJOR → MINOR):

Step 2a: Choose fix strategy

For each issue, explicitly choose one of:

• ADD_DERIVATION: Write missing proof steps
• STRENGTHEN_ASSUMPTION: Add conditions to theorem statement
• WEAKEN_CLAIM: Reduce conclusion scope
• ADD_REFERENCE: Cite known result + verify its conditions apply

Log this choice — it is a scope-changing decision when it alters theorem statements.

Step 2b: Derive the fix mathematically

• Complete mathematical derivation, not just a claim
• If new proposition/lemma needed, write in full theorem-proof style

Step 2c: Implement in LaTeX

• Edit the .tex file
• Preserve existing \label references where possible

Step 2d: Record the fix

### 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]

Step 2e: Compile check

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

Phase 3: Re-Review (reviewer backend, ultra reasoning)

Continue with the selected backend. For codex, use mcp__codex__codex-reply with the saved threadId. For manual, use mcp__manual_review__review_reply with the saved threadId. For self, re-read the fixed proof fresh from disk (not from memory of the fix you just applied) alongside the Phase 1 issue list, and re-apply the same checklist as a skeptical check on whether the fix actually closed the gap. Include fix summaries. Request the same mandatory checklist.

Check acceptance gate. If not met, repeat Phases 2-3 (up to MAX_REVIEW_ROUNDS).

Phase 3.5: Global Closure & Independent Verification

Global closure checks

After all fixes, verify the proof as a whole:

• Statement–conclusion match: Does the proof end with EXACTLY what the theorem claims (quantifiers, constants, uniformity)?
• All obligations discharged: Every node in the obligation DAG is proven or explicitly assumed (and the theorem statement includes it).
• Case analysis coverage: Cases partition the domain AND include boundary/degenerate cases.
• Induction correctness (if applicable): Base case, inductive step, correct use of IH, induction measure strictly decreases.
• WLOG reductions: Each "without loss of generality" spawns a micro-claim proving the reduction is lossless.
• No silent assumption strengthening: Any fix that strengthened assumptions has propagated to the main theorem statement.

Independent second review for FATAL/CRITICAL fixes

For any fix that resolved a FATAL or CRITICAL issue, submit the fixed section alone (without showing the previous critique) to a fresh reviewer thread using the selected backend. Do NOT use a reply tool — this step must be blind.

For codex: start a fresh mcp__codex__codex thread. For manual: start a fresh mcp__manual_review__review thread. For self: this is the one Phase 3.5 sub-step where blindness matters most and self-review is weakest — Claude cannot fully un-know the prior critique it wrote. Mitigate as best possible: review only the fixed section text with no visible issue list or prior discussion open, as if it were handed to you with zero context. Flag this round's verdict as the lowest-confidence check in the audit (see the honest tradeoff in auto-review-loop's Self-Review Backend) and weight a FATAL/CRITICAL fix's real acceptance more on the Phase 3 re-review and Phase 3.5's other closure checks than on this sub-step alone.

The blind review prompt/checklist:

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]

If the blind reviewer finds new issues, re-enter Phase 2.

Regression proof-audit

After fixes, re-run:

• DAG acyclicity check (no new cycles introduced)
• Counterexample suite on all DOWNSTREAM lemmas of modified results
• Assumption-delta report: what became stronger/weaker due to fixes?

Phase 3.6: Theorem Restatement Regression (opt-in)

Default: skipped. Existing callers see no change.

Opt-in: pass --restatement-check on invocation. The skill then runs a cross-location consistency pass after Phase 3.5 (Global Closure) and before Phase 3.9 (Unrecoverable Protocol).

This phase catches a specific class of bugs that Phase 3.5's "Statement-conclusion match" check does NOT catch: drift between the canonical theorem statement and its restatements elsewhere in the paper (summary tables, "Key Contributions" / "Summary" sections, abstract, discussion, captions). Common drift patterns observed in practice:

• Main theorem makes a partly-conditional claim (e.g., "regime A unconditional, regime B conditional on assumption X") but a later summary cites it as the fully unconditional version.
• Main theorem κ exponent is O(d²K²) but a constants table writes O(K²).
• Main theorem regime condition is squared envelope, but a remark elsewhere still shows the first-order envelope.
• Restatement quietly drops a quantifier ("for $n \ge n_0$") that the proof relied on.

Algorithm

1. Build canonical statement table. Scan all *.tex files in the paper for \begin{theorem} / \begin{lemma} / \begin{proposition} / \begin{corollary} blocks with a \label{...}. For each: record (label, full_statement_text, file:line_range).

2. Collect restatement candidates. For each canonical label thm:foo:

   • Every \Cref{thm:foo} / \ref{thm:foo} / \cref{thm:foo} invocation, with the surrounding 2 sentences as candidate restatement context.
   • Rows in tables (\begin{tabular} … \end{tabular}) that mention the label, the theorem's informal name, or its constants.
   • Bullets in "Key Contributions" / "Summary" / "Main Results" lists.
   • Sentences in the abstract and introduction that paraphrase the theorem.

3. Normalized diff. For each (canonical_statement, restatement_context) pair:

   • Strip \, \; \! ~, normalize whitespace, normalize math-mode delimiters ($..$, \(..\), display vs inline).
   • Detect drift signatures (one or more):
     • conditional_loss — canonical says "under \Cref{ass:X}" or "for w=1"; restatement omits the conditional.
     • scope_change — big-O exponent or rate differs (O(K^2) vs O(d^2K^2); √n vs n).
     • quantifier_loss — quantifier present canonically (e.g. "for $n \ge n_0$", "for sufficiently small $\gamma$") absent in restatement.
     • regime_envelope_change — first-order leakage Cγ/(1-Δγ) vs squared envelope (Cγ/(1-Δγ))² (or analogous).
     • constant_change — different numeric constant or different parameter dependence stated.
     • variable_rename — same role in argument played by differently-named symbol with no explicit alias.

4. Emit findings. Each detected drift becomes an entry in details.restatement_drift (see "Submission Artifact Emission" below). Severity defaults to MAJOR (UNDERSTATED/OVERSTATED + GLOBAL); reviewer may downgrade to MINOR if drift is purely cosmetic (e.g. \, placement) and upgrade to CRITICAL only if the restatement is used downstream as if it were the canonical (e.g. another proof cites the restated version).

What this phase does NOT do

• It does not fix drift automatically. The output is advisory; the executor or a follow-up --deep-fix run handles the rewrite.
• It does not alter details.issues; restatement drift is reported as a sibling field, so existing consumers reading issues[] see no schema change.
• It does not alter the top-level verdict decision rule. A paper with non-empty restatement_drift may still emit PASS if all proof obligations are otherwise discharged; the drift is independent of proof correctness. (The reviewer may at its discretion mirror a CRITICAL-severity drift into the issues list as a regular issue — typically when the restated version is used downstream as if it were canonical — but that is a per-issue judgment, never an automatic rule. MAJOR or MINOR drift never mirrors into issues.)

Failure mode

If --restatement-check is set but the cross-location scan cannot complete, emit details.restatement_drift: [] plus details.restatement_check_status: "unavailable" with a one-line note explaining why. Verifier gates and downstream skills MUST treat "unavailable" identically to the field being absent: not blocking. Phases 1 / 1.5 / 2 / 3 / 3.5 / 3.9 / 4 / 5 still run normally. Cases that trigger this fallback include:

• Unreadable .tex (parser / encoding error on a file that contains a theorem block).
• Ambiguous label resolution (e.g., the same \label{thm:foo} appears more than once with no clear canonical pick).
• No labeled canonical theorem-like block found (the algorithm only inspects \begin{theorem|lemma|proposition|corollary} blocks with an explicit \label{...}; if there is no such block, there is nothing to compare restatements against).

Phase 3.9: Unrecoverable Proof Protocol

If acceptance gate is not met after MAX_REVIEW_ROUNDS, output a Proof Unrecoverable Report:

1. Minimal set of blocking FATAL/CRITICAL issues that could not be resolved
2. Salvage options ranked: (a) weaken claim, (b) strengthen assumptions, (c) add missing lemmas, (d) restructure argument
3. Which parts of the proof are likely still reusable
4. Recommended next steps for the author

Do NOT silently declare success. The report must be honest.

Phase 4: Audit Report Generation

Generate proof_audit_report.tex with:

1. Overview table: All issues with two-axis severity, category, fix strategy, status
2. Before/After logic chain: Red (BEFORE) → Green (AFTER) comparison
3. For each fix: original proof → why wrong → counterexample (if any) → complete derivation → remaining subtleties
4. Proof-obligation diff: What was unverified before, what is verified now
5. Summary: Now proven / still assumed / open problems
6. Colored boxes: BEFORE (red), AFTER (green), WHY WRONG (orange), KEY INSIGHT (blue), WARNING (yellow)

Compile: pdflatex proof_audit_report.tex && pdflatex proof_audit_report.tex

Phase 5: State Persistence

Write PROOF_CHECK_STATE.json:

{
  "status": "completed",
  "rounds": 2,
  "reviewer_backend": "codex | manual | self",
  "threadId": "... (null when reviewer_backend is self)",
  "fatal_fixed": 0,
  "critical_fixed": 3,
  "major_fixed": 2,
  "minor_fixed": 1,
  "counterexamples_found": 1,
  "counterexample_candidates": 2,
  "acceptance_gate": "PASS",
  "timestamp": "..."
}

Phase 5.5: Research Wiki Claim Ledger (additive; only if a wiki is active)

If — and only if — a research-wiki/ exists, persist each top-level theorem/headline as a claim node so the wiki's PROVE/JUDGE ledger records what was proven and with what honesty. This is the birth point for wiki claim nodes (claims/<slug>.md). It is a detect-only record, never a verdict: it never changes the audit's verdict/reason_code, never blocks, and is skipped entirely when verdict == NOT_APPLICABLE (no theorems) or no wiki is found.

The claim's status is the PROOF axis only (verified / sound-modulo-imports / refuted / unproven / drafted / retracted). Empirical experiment support is a separate axis carried by supports / invalidates edges from /result-to-claim — those words are NEVER written into this status field (the research_wiki.py validator rejects them).

Resolve the helper via the canonical resolver (integration-contract §2). Check NOT_APPLICABLE first (in cwd, where the audit ran), then run from the project root (the wiki sits at root; a paper audit may run from a paper/ subdir). Every guard warn-and-skips — the audit is already complete and is never affected:

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; }

For each top-level theorem/headline in PROOF_SKELETON.md (the main theorem + the key lemmas the headline depends on — NOT every micro-claim), map the audit outcome to an honest claim status:

Never invent a status: a plain proof gap is unproven — never refuted (which asserts falsity) and never verified/drafted. Then record (idempotent):

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 lets a re-audit refresh a claim's status (an unproven claim becomes verified once the gap closes). --provenance is the honesty receipt (the trace_path); never omit it.

Deep-Fix Mode (opt-in)

Default: disabled. The Phase 1 reviewer emits issues with minimal_fix (a 1-2 sentence pointer); existing callers see no change.

Opt-in: pass --deep-fix on invocation. The Phase 1 reviewer prompt is augmented (not replaced) with the "DEEP-FIX OUTPUT" and "ALGEBRA / TYPE SANITY PASS" blocks above, so the reviewer also returns a deep_fix_plan per issue: corrected statement, changed equations, downstream label list, minimal LaTeX patch plan, and closure tests. Issues invoking Schur / Young / Cauchy-Schwarz / Hölder / quadratic forms / operator norms / power counting additionally carry an algebra_sanity block (dimension table + power count + zero-coupling check + constant-dependence diff).

Why opt-in

The default minimal_fix prose is intentionally short — it suits the common case where the executor wants high-level pointers and will derive the patch separately. Forcing deep_fix_plan on every run would (a) inflate every reviewer call by 2-5×, (b) trigger re-review thrash for issues the executor has already decided to weaken or defer, and (c) change the shape of details.issues for every existing caller. The flag preserves zero behavior change for default invocations while letting the executor request repair-grade output when the fix is going to be applied immediately.

Effect when enabled

• The Phase 1 reviewer prompt is augmented with the deep-fix and algebra-sanity blocks; nothing in the original mandatory checklist or output format is removed.
• PROOF_AUDIT.json details gains a sibling field deep_fix_plans (parallel to `d

…(truncated)