Proofcheck

ProofCheck — Mathematical Proof Verification for Statistics/ML Theory Papers

🔬 Model Recommendation: Run this skill on Claude Opus for best results. Mathematical proof verification requires deep reasoning. If your session is not on Opus, run /model opus before invoking. The skill will also delegate heavy reasoning to Opus sub-agents internally when the Agent tool is used.

Systematically check proofs in long technical appendices using a structured, evidence-based methodology with multi-pass verification.

Based on: https://github.com/maweiruc/proofcheck-stat-paper

Context: $ARGUMENTS

Core Objective

Given the paper's stated assumptions, definitions, and cited results, does each claimed theorem follow with the stated constants, rates, quantifiers, probability levels, domains, and edge cases?

Goal: Find correctness issues — NOT summarize the proof. Never silently repair proofs.

---

Operating Principles

1. Evidence First: Every conclusion cites exact page/section/equation/line numbers. No vague references.
2. Small Proof Units: One definition, one lemma, one proof at a time. Never verify 20+ pages at once.
3. Separate Facts/Inferences/Suspicions: Verified (checked + referenced), Inferred (likely but unchecked), Suspect (possible gap).
4. No Silent Repairs: If proof proves B but claims A, record the mismatch explicitly.
5. Human Owns Final Judgment: Agent indexes, cross-checks, and reconstructs. Human reviews all S0/S1 issues.

Severity System, Verification Statuses, and Provability Triage

The S0-S3 severity system, the five verification statuses (Verified / Conditionally verified / Gap found / Incorrect / Not checked), and the three-class provability triage (PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED) are defined in ../stat-shared-references/proof-closure-machinery.md. That file is the single source of truth shared with proof-repair and proof-writer.

Operational note for this skill:

• Apply the severity system in Pass 5 (Final Report) when assigning severity to each open issue.
• Apply the provability triage at the start of each unit's deep-check (per Pass 1 Step 3, "Sketch-vs-Complete classification" + this triage).
• Set verification statuses on each unit's local check file in audit/04_local_checks/.

Proof Strategy Classification (per unit)

Identify the proof technique BEFORE step-by-step checking — different strategies have different failure modes:

Strategy	Common failure modes to watch
Direct	Missing case, unjustified step, wrong inequality direction
Contradiction	Negation error, unconsidered third case, vacuous hypothesis
Induction	Missing base case, hypothesis used outside valid range, wrong induction variable
Construction	Object may not satisfy all requirements, uniqueness not checked
Reduction to known result	Cited result used outside its conditions, notation mismatch
Coupling / probabilistic	Independence assumed, coupling fails at boundary, measurability
Optimization / variational	Existence of minimizer, local vs global, compactness missing
Epsilon-delta / approximation	Quantifier order, uniformity, limit exchange

---

Workflow

0. Setup Workspace

Parse $ARGUMENTS to locate the paper's LaTeX source file.

# Create workspace structure
PAPER_DIR="papers/$(basename "$PAPER_PATH" .tex)"
mkdir -p "$PAPER_DIR/audit"/{01_index,02_ledgers,03_dependencies,04_local_checks,05_adversarial,06_reports}

If $ARGUMENTS is a directory, look for paper.tex inside it. If it's a .tex file path, use it directly.

Detect Reference Mode (one-file vs two-file submission)

Before any cross-reference audit, detect whether the paper is:

• Mode A: single-file — one .tex compiles to one PDF (arXiv, NeurIPS/ICML)
• Mode B: two-file — paper.tex + supplement.tex (or similar) compile separately (typical for JASA, AoS, JRSS-B, Biometrika, Econometrica, JBES, JOE)

# Count top-level .tex files (excluding files that are \input by others)
find "$(dirname "$PAPER_PATH")" -maxdepth 1 -name "*.tex" -type f
# Look for explicit supplement files
ls "$(dirname "$PAPER_PATH")"/{supp*,supplement*,appendix*,SI*}.tex 2>/dev/null
# Look for S-prefix labels — strong signal of Mode B
grep -l 'label{[^}]*:S[._]\|label{S' "$(dirname "$PAPER_PATH")"/*.tex 2>/dev/null

Record in CHECK_PLAN.md:

## Reference Mode
Mode: [A: single-file / B: two-file]
Files: [list]
Cross-file convention (if Mode B): hard-coded numbers (e.g., "Lemma S.3", 
       "Theorem 2.1 of the main text") — NOT \ref{} across files

This mode affects Pass 0's cross-reference audit (Step 2B) — see below.

1. Bootstrap — Generate CHECK_PLAN.md + EXECUTION_ORDER.md

Read the paper and extract the proof architecture. Do NOT check any proofs yet — only map the terrain.

1A. Extract Proof Architecture (→ CHECK_PLAN.md Part A)

Read these sections of the LaTeX source:

1. Introduction — contributions subsection, look for TikZ dependency diagrams
2. Proof strategy section — "Proof Strategy", "Proof Outline", "Overview of Proofs"
3. Appendix structure section — the appendix's own roadmap
4. Main theorem statements

Produce:

• Core Proof Strategy (≤5 sentences): the fundamental challenge, the solution, the key innovation
• Dependency Diagram (ASCII art): reconstruct from paper's figures or theorem statements
• Critical Proof Chains (3-5 chains): base lemmas → main theorems
• Key Definitions Table: notation appearing across multiple sections

1B + 1C. Index the architecture (script)

Run the mechanical indexer instead of hand-running grep and a manual topological sort:

python ../stat-shared-references/scripts/proof_index.py \
  --main paper.tex \
  --supplement supplement.tex \
  --supplement-mode separate-self-contained \
  --json-out audit/proof_index.json \
  --md-out audit/01_index/PROOF_INDEX.md

The script is authoritative for the mechanical parts of Step 1B/1C and Pass 0 Task 2B:

• Proof unit inventory: every theorem-like environment (theorem, lemma, proposition, corollary, definition, assumption, condition, remark, claim, fact) with type, label, line, and statement summary.
• Dependency graph: for each unit's proof block, the indexed labels it \refs.
• Topological layers: a valid check order (Layer 0 = no internal deps; Layer k = deps in layers < k), with cycle detection (a dependency_cycle FAIL means the proof order is not well-founded).
• Cross-reference integrity: \ref targets with no \label (FAIL), and cross-file leaks under separate-self-contained (FAIL — the canonical two-file submission bug).
• Reference mode: single-file vs two-file detection.

Exit code 1 means at least one structural FAIL (undefined ref or dependency cycle); fix those before deep-checking. Provenance (script_version, rules_version, rules_digest) is in the report header.

What the script does NOT produce, and you still supply by judgment:

• The core proof strategy narrative (1A): the fundamental challenge, the key innovation. Read the introduction and proof-strategy section for this.
• Critical proof chains: which base lemmas feed which main theorems, and which units are load-bearing. The topological layers are the raw material; deciding the critical path is judgment.
• Per-unit assumption strength and regime (Task 2A judgment columns below).

2. Pass 0 — Indexing (Map the Terrain)

Three parallel tasks:

Task 2A: Theorem Inventory → audit/01_index/theorem_inventory.md

ID	Type	Location	Short name	Statement summary	Depends on	Used by	Status

For each: label, exact location, mathematical objects, assumptions (explicit + inherited), claimed conclusion, probability/asymptotic regime, constants (universal vs problem-dependent), where used. If assumptions.lock.md exists, record each unit's assumptions as invoked registry IDs (A1, A3) resolved against the shared store, not as re-typed statements; an assumption in a proof with no matching registry ID is itself a finding (see Pass 3 check 3b).

Task 2B: Cross-Reference Audit — covered by the script in Step 1B/1C.

The undefined-ref and cross-file-leak checks are mechanical and are produced by proof_index.py (findings undefined_ref and cross_file_ref_leak). Read audit/01_index/PROOF_INDEX.md for them. The script auto-detects single-file vs two-file mode.

Two convention checks remain judgment and are not mechanized (the script flags the leak; you assess the phrasing fix):

• Hard-coded number convention: in two-file mode, each "of the supplement" / "of the main text" mention should be paired with a hard-coded number (e.g., "Lemma S.3 of the supplement"), since \ref cannot cross files. The script flags the broken \ref; you confirm the textual replacement reads correctly.
• Supplement numbering consistency: the supplement's theorem/equation counters should use S-prefix display numbers (e.g., \renewcommand{\thelemma}{S.\arabic{lemma}}). Verify this by inspection.

Task 2C: Notation Ledger → audit/02_ledgers/notation_ledger.md

Symbol	Meaning	First defined	Domain/type	Parameters	Later uses	Drift risk

Check for: symbols used before definition, same symbol for different objects, scalar/vector mismatch, random/deterministic mismatch, norm changes, constants with changed dependencies.

Also build:

• audit/02_ledgers/assumption_ledger.md — ID | Assumption | Location | Scope | Used by | Strength needed | Status
• audit/03_dependencies/dependency_graph.md — dependency table + circularity analysis

3. Pass 1 — Check Critical Path

Check the chain leading to the main theorem FIRST. Prioritize lemmas used by many later results.

MANDATORY first sub-step: Sketch-vs-Complete Classification

Before checking proof correctness, classify whether what the paper provides is ACTUALLY a proof, or only a sketch / outline. This is distinct from step-skipping (which is about individual missing steps within a proof) — this is about whether the entire proof body is rigorous derivation or just high-level summary.

Three-class classification:

Class	Definition	Action
COMPLETE	Rigorous step-by-step derivation; all transitions justified; cited results have prerequisites verified; edge cases handled	Proceed with normal step-by-step verification
PARTIAL-SKETCH	Some rigorous derivation but with substantial gaps (e.g., "the rest follows by similar arguments"; entire technical lemma deferred to supplement; proof of main step is one paragraph for a 1-page-claim theorem)	Treat each gap as an S1 issue; demand expansion before any "verified" verdict
SKETCH-ONLY	High-level outline without rigorous derivation. Title says "Proof Sketch" / "Sketch of Proof", or proof body is purely verbal narrative with no equation derivations, or proof says "we (1) bound X, (2) apply Y, (3) conclude" without actual algebra	The unit cannot be marked Verified — it's not a proof, it's a plan. Report as STATUS: SKETCH-ONLY — NO PROOF PROVIDED

Sketch indicators (any combination triggers PARTIAL-SKETCH or SKETCH-ONLY):

• Title or section explicitly says "Proof Sketch" / "Sketch of Proof" / "Outline of Proof"
• Body contains: "We sketch the proof", "Full details in the supplement", "Detailed proof is omitted"
• Proof length disproportionate to claim complexity (e.g., 5 lines for a 2-page theorem)
• Body is purely verbal narrative ("we first bound X using Y, then apply Z") with no derived equations
• "Similar to / follows from [Paper Z]" without showing the adaptation
• Heavy use of "it can be shown that" / "by standard arguments" / "after some algebra"
• "We omit the details for space"
• Technical core deferred entirely: "Lemma N is proved in Appendix X" but Appendix X is also sketch-only
• A theorem whose proof is a single paragraph + a citation to another paper

Crucially: a proof labeled "Proof Sketch" is NOT a sufficient verification of the claim. If the paper relies on this sketch as evidence for the theorem, the theorem's actual status is at best CONDITIONALLY VERIFIED pending the full proof. Reviewers at AoS / JASA / JRSS-B / Biometrika do not accept main-text sketches without full proofs in supplement.

Record in the unit check file:

### Sketch-vs-Complete Audit
- Class: [COMPLETE / PARTIAL-SKETCH / SKETCH-ONLY]
- Sketch indicators found: [list specific evidence]
- For PARTIAL-SKETCH: each gap recorded as an S1 issue requiring expansion
- For SKETCH-ONLY: STATUS is forced to "SKETCH-ONLY — NO PROOF PROVIDED"
- Supplement location (if proof is supposed to be elsewhere): [pointer + verify it IS complete there]
- **Expansion status**: [REQUIRED / IN-PROGRESS / COMPLETED] ← MANDATORY field
- **Expanded proof file**: [path, set once expansion is complete]

If the "real" proof is supposed to be in supplementary material, follow the link and audit the supplement proof; if the supplement proof is also a sketch, both get tagged SKETCH-ONLY.

HARD RULE: detection requires immediate expansion

A sketch detected during /proofcheck cannot remain unexpanded in the final audit output. The audit is NOT complete while sketches remain.

When SKETCH-ONLY or PARTIAL-SKETCH is found:

1. Mark the unit with Expansion status: REQUIRED
2. Immediately hand off to /proof-repair (Expand-Sketch-to-Proof repair class) which then invokes /proof-writer for the actual writing
3. /proof-writer must produce either:
   • A COMPLETE proof (Expansion status → COMPLETED)
   • An explicit NOT-CURRENTLY-JUSTIFIED blockage report (then the theorem itself is downgraded; the sketch is still removed)
4. After expansion, re-run the Sketch-vs-Complete classification on the new proof body — verify it now classifies as COMPLETE
5. The audit is blocked from "Pass 5: Final Report" until every detected sketch has Expansion status of either COMPLETED or BLOCKAGE-REPORT-WRITTEN

The Final Report's executive summary MUST contain a row:

Sketches detected: N
├── Expanded to complete proof: M
├── Determined to be unprovable as stated (blockage report): K
└── Outstanding (NOT ALLOWED in final state): 0

If any sketch remains in "REQUIRED" or "IN-PROGRESS" state when the audit attempts to finalize, the skill REFUSES to mark the audit complete and returns to expansion.

For EACH proof unit, create one file: audit/04_local_checks/section_X/{ID}_{name}_check.md

Each file follows this template:

## Proof Unit: [ID / Name]
- Location:
- Type: [definition / lemma / proposition / theorem / proof segment]
- **Sketch class**: [COMPLETE / PARTIAL-SKETCH / SKETCH-ONLY]   ← from Sketch-vs-Complete audit
- Proof Strategy: [direct / contradiction / induction / construction / reduction / coupling / optimization / epsilon-delta]
- Provability: [PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED]
- Status:
- Confidence:

### Claim Normalization
**Original statement**: [exact copy from paper]
**Normalized form**: [rewritten with all quantifiers, domains, types explicit]
**Interpretation notes**: [any ambiguity resolved, notation clarified]

If the normalized form is stronger/different from the original, flag this explicitly.

### Explicit Assumptions
- [Assumption 1]

### Inherited / Implicit Assumptions
- [Standing assumption]
- [Hidden assumption detected: ...]

### Dependencies
| Dependency | Location | Required form | Available? | Verified? | Notes |
|------------|----------|---------------|------------|-----------|-------|

### Step-by-Step Verification
| Step | Location | Claim | Justification | Verdict | Notes |
|------|----------|-------|---------------|---------|-------|
| 1 | Eq.(42)→(43) | Triangle ineq | Same norm | Valid | None |
| 2 | Eq.(43)→(44) | Lemma A.2 | Needs boundedness | Gap | Missing assumption |

**Anti-fabrication checklist** — flag ANY instance of:
- "clearly" / "obviously" / "it is easy to see" hiding a nontrivial step
- "by standard arguments" without specifying WHICH standard argument
- "similarly" referring to a non-analogous situation
- A step justified only by "by the above" without exact reference
- Unmarked use of a stronger assumption than what is stated

### Edge Cases & Boundary Analysis
- [Boundary case checked: what happens when parameter = 0/1/∞?]
- [Degenerate case: what if matrix is singular / set is empty / dimension = 1?]
- [Domain boundary: does the result hold at the boundary of Θ?]

### Issues
| Severity | Confidence | Description | Evidence | Proposed repair |

### Final Verdict
[Verified / Conditionally verified / Gap found / Incorrect / Unclear]

### If Gap Found: Blockage Report
- **Exact blocker**: [which step fails and why]
- **What would fix it**: [minimal extra assumption / lemma / technique needed]
- **Weaker claim that IS provable**: [if applicable]
- **Candidate literature**: [known results that might bridge the gap — to be expanded by /proof-repair]

Key checks for each step:

• Every equation transition and inequality direction
• Every quantifier and probability statement
• Every constant, rate, domain, dimension
• Every boundary case
• Conclusion vs. statement match
• Conclusion matches EXACTLY what was proved (not a stronger restatement)
• Every nontrivial implication is justified — no "clearly" or "obviously" allowed

Step Completeness Audit (sub-step within each unit check)

This audit is mandatory for every proof unit. Going beyond passive anti-fabrication word-flagging, it ACTIVELY identifies step jumps and reconstructs them.

A. Skip-point detection

For each proof unit, scan for skip indicators in three categories:

Category 1: Verbal skip phrases

• "clearly" / "obviously" / "it is easy to see" / "trivially"
• "by standard arguments" / "as is well-known" / "it is well-known"
• "after some algebra" / "after simplification" / "by direct calculation"
• "by symmetry" / "similarly" / "the same argument applies"
• "the rest follows" / "the conclusion is now immediate" / "we omit the details"
• "as before" / "by the above" / "in an analogous manner"

Category 2: Equation-number jumps

• Eq.(k) appears, then Eq.(k+m) for m ≥ 2 without intermediate equations
• A displayed equation followed by ≥2 lines of unjustified manipulation
• Use of an unstated identity to transform one expression to another

Category 3: Implicit logical jumps

• A conclusion drawn from a previous claim without stating the inference rule
• A bound used as both upper and lower without separate justification
• An optimization step where existence of optimizer is assumed but not shown
• A limit/sum/integral exchanged without naming the convergence theorem

B. Reconstruction attempt

For EACH detected skip, attempt to fill in the missing steps:

1. List what is being claimed before the skip (the input state)
2. List what is being claimed after the skip (the output state)
3. Reconstruct the bridging steps explicitly (using paper assumptions + cited results + standard mathematical facts only — no fabrication)
4. Count the reconstructed steps and assess the techniques used

C. Skip classification (for each detected skip)

Based on the reconstruction:

Class	Reconstruction needed	Verdict	Action
TRIVIAL	≤1 line of standard manipulation (e.g., expand brackets, apply definition)	Legitimate skip	Note as TRIVIAL, no action
VERIFIABLE	2-5 lines of standard manipulation (e.g., chain of substitutions, named inequality applications)	Legitimate but author should write it	Suggest filling in (severity: S3)
NONTRIVIAL	Requires a non-obvious idea, a hidden lemma, or a specific technique	MUST be filled in by the author	Record as S1 issue; downstream /proof-repair will need to insert
UNRECONSTRUCTIBLE	Cannot bridge from input to output state using available assumptions + cited results	Possible error	Record as S0/S1 issue; demand author justification or counterexample

D. Step Completeness Table (per unit)

Add to each unit's check file:

### Step Completeness Audit

| Skip # | Location | Skip indicator | Input state | Output state | Reconstruction | Class | Severity |
|--------|----------|---------------|-------------|--------------|----------------|-------|----------|
| 1 | Line 152, "obviously" | verbal | f(x) ≥ 0 ∀x | ∫f dμ ≥ 0 | Apply monotonicity of integral (1 line) | TRIVIAL | — |
| 2 | Eq.(47)→(50) | equation jump | LHS of (47) | RHS of (50) | Algebraic expansion + Cauchy-Schwarz + bound on ‖∇f‖ (4 lines) | VERIFIABLE | S3 |
| 3 | "by symmetry" line 198 | verbal | Bound on E[XY] | Bound on E[X²]+E[Y²] | Symmetry NOT applicable here — X,Y not exchangeable | NONTRIVIAL | S1 |
| 4 | "after some algebra" line 220 | verbal | Eq.(60) | Eq.(61) | Cannot reconstruct — requires unstated identity for matrix inverse | UNRECONSTRUCTIBLE | S0 |

**Summary**: 4 skips found. 1 trivial, 1 verifiable, 1 nontrivial (S1), 1 unreconstructible (S0).

E. Reconstruction discipline (anti-fabrication for the checker)

When reconstructing steps, the checker itself must follow rigor rules:

• Use ONLY: paper's stated assumptions + cited results + named standard facts (e.g., Cauchy-Schwarz, Jensen, triangle inequality, Holder's)
• For named standard facts, cite the name explicitly ("by Cauchy-Schwarz")
• Do NOT invent intermediate inequalities or unstated lemmas
• If a reconstruction requires invoking a non-obvious lemma, classify as NONTRIVIAL and record what lemma is needed
• If reconstruction succeeds but uses techniques not in the paper's framework (e.g., heavy machinery from a different subfield), flag as suspect — the author probably intended a simpler bridge that we're missing

4. Pass 2 — Check Support Lemmas

After critical path confirmed, check remaining lemmas in parallel within each phase. Same per-unit template as Pass 1.

Also maintain:

• audit/02_ledgers/constants_ledger.md — track which constants are universal vs problem-dependent
• Event ledger — track probability events, their definitions, and how they compose

5. Pass 3 — Global Consistency

Cross-cutting checks after all local checks:

1. No circular dependencies — trace every chain to base assumptions
2. Notation consistent — no symbol drift between sections
3. Assumptions propagate — every cited assumption is in scope where used 3b. Shared assumption store (if assumptions.lock.md exists; schema in ../stat-shared-references/assumptions-lock-protocol.md) — resolve every theorem's invoked assumption IDs against the registry and run consistency triage, not satisfiability certification. Flag: (i) an assumption stated in a proof that is not a registry ID (unregistered — should be invoked or appended); (ii) two near-duplicate registry rows that are the same assumption under different short names (should be one ID); (iii) a theorem co-invoking IDs marked incompatible-with each other or two variant-of the same base; (iv) invoked-but-unused IDs (minimality — a theorem carrying an assumption its proof never consumes, which weakens its stated generality). Expand any profile alias (P-base = {A1,A2,A3}) before the unused check. Emit PASS: no direct contradiction found / FLAG: axis tension / FAIL: direct contradiction / UNKNOWN: common model not certified — never claim the full registry is jointly satisfiable (a framework may hold mutually exclusive regimes on purpose). Write findings to audit/03_dependencies/assumption_lock_triage.md.
4. Theorems assemble — each main theorem's transitive dependencies all proved
5. Quantifier consistency — check "for all ∃" vs "∃ for all", uniform vs pointwise, parameter-dependent vs universal constants
6. Probability/event consistency — events defined? Intersections handled? Failure probability accumulated correctly?
7. Constants/rates consistency — are O(·) terms hiding forbidden dependencies? Rates preserve all n, d, δ, ε?
8. Asymptotic-order consistency / negligibility closure — every disappearing term must have a recorded comparison scale and a recorded bridge. For each proof unit, build a local dropped-term ledger with columns Term dropped | Needed scale | Support source | Bridge | Verdict, where Support source is one of local bound, earlier proved lemma, or audited citation, and Bridge is the explicit calculation or one-line mode conversion that turns that support into the claimed o(·) / o_p(·) / negligible / dominated conclusion. Deterministic order arithmetic may pass trivially, but any uniformity, conditioning, dependence, Taylor-remainder, or parameter-dependent-constant claim requires an explicit derivation. If a unit drops a term without a filled bridge entry, proves only the wrong scale, or upgrades pointwise or on-event control to uniform or unconditional negligibility without justification, flag.

For the asymptotic-order check, each local check file should expose the bridge in a compact table:

### Dropped-Term / Negligibility Ledger
| Term dropped | Needed scale | Support source | Bridge | Verdict |
|--------------|--------------|----------------|--------|---------|

A missing row, wrong comparison scale, unsupported dominance claim, or unjustified pointwise-to-uniform / on-event-to-unconditional upgrade is a Global Consistency flag. See the Trap Catalogue item #9 and the Negligibility-Closure Trivial-Pass Tier in ../stat-shared-references/proof-strategy.md for the discriminator between Tier-1 (deterministic order arithmetic, free pass), Tier-2 (stochastic mode conversion, one-line bridge), and Tier-3 (uniformity / conditioning / dependence / Taylor / parameter-dependent constants, explicit derivation required).

6. Pass 4 — Adversarial Review

Deliberately try to break the proof:

Counterexample search: What happens with d=1, n=1, zero variance, singular matrix, boundary of parameter space, heavy tails, equal parameters, probability-zero events, flat/non-smooth functions?

Hidden assumption search: For each proof unit check:

• Division by zero? Matrix invertibility without proof?
• Limit/expectation/derivative/integral exchange without justification?
• Concentration without independence/tail checks?
• Compactness without compact domain?
• Minimizer existence assumed? Uniqueness used but not proved?
• High-probability statements used simultaneously without union bound?
• Uniform result claimed from pointwise proof?

External theorem misuse: Check exact prerequisites, finite-sample vs asymptotic, pointwise vs uniform, matching notation.

Stress assumptions: Remove each assumption → which step fails? Does proof use stronger version than stated? Are there unused assumptions?

Assumption load-bearing audit: For each load-bearing assumption (one a main theorem's critical chain actually consumes — skip unused/purely-technical conditions, which the "unused assumption" check above already covers), apply the four tests in ../stat-shared-references/assumption-loadbearing-audit.md: T1 Conclusion Restatement (S0, merges with the circularity gate), T2 Verification Target Assumed (S1), T3 Central Difficulty Pre-emption (S1, capped — escalates to S0 only as a vacuous-class / OVERSTATED statement-scope / silent-downstream defect), T4 Comparative Axis Reversal (S1 headline / S2 local). This needs the introduction's claimed central difficulty and the Task 2A inventory, not just the local proof — that is why it lives in Pass 4, not Pass 2. Absence of a finding is the expected result for a clean conditional theorem; proof length is never evidence. For any flagged assumption, produce the Original Assumption Challenge Ledger from that reference and route by repair type (T1 → proof-repair; relaxable T2/T3/T4 → theory-sharpen; oversold-but-correct → stat-polishing).

Write findings to audit/05_adversarial/hidden_assumptions.md and audit/05_adversarial/counterexamples.md. Put any load-bearing-audit findings and the Challenge Ledger in audit/05_adversarial/assumption_loadbearing.md.

Codex Adversarial Cross-Review (if Codex MCP available)

Follow ../stat-shared-references/codex-protocol.md — Codex is an adversarial reviewer to discuss with iteratively, not an oracle to defer to. Every Codex finding requires explicit ACCEPT / PUSH BACK / REQUEST CLARIFICATION with reasoning. Forbidden behaviors: silent wholesale acceptance, silent rejection, agreement without recording why. The skill must emit codex_discussion.md documenting the full round-by-round dialogue.

Use mcp__codex__codex to get an independent second opinion from a different model. The key design: Codex does NOT see Claude's findings — it forms its own judgment first.

For each S0/S1 issue found by Claude, send to Codex:

mcp__codex__codex:
  config: {"model_reasoning_effort": "high"}
  prompt: |
    You are an adversarial reviewer of mathematical proofs in statistics/ML theory.

    Here is a proof unit from a paper:
    [Paste: lemma statement + proof text + assumptions + dependencies]

    Claude (another AI) claims this proof has a SPECIFIC issue:
    [Paste: issue description, severity, evidence]

    Your tasks:
    1. INDEPENDENTLY verify: do you agree this is a genuine issue?
       - If YES: confirm and rate severity (S0 fatal / S1 major / S2 moderate / S3 minor)
       - If NO: explain why Claude's concern is invalid or overstated
    2. Find issues Claude MISSED: are there other problems in this proof unit?
    3. For each genuine issue: is there an obvious fix?

    Rules:
    - Cite exact equations, line references, or proof steps
    - Do not fabricate issues — "no additional issues found" is a valid answer
    - Be precise about severity: S0 means the main theorem breaks, not just a local gap

For each unit Claude marked "Verified", spot-check 20-30% via Codex:

mcp__codex__codex:
  config: {"model_reasoning_effort": "high"}
  prompt: |
    You are checking a mathematical proof for correctness.

    Here is a proof unit:
    [Paste: lemma statement + proof text + assumptions]

    Another reviewer marked this as "Verified — no issues."
    Your job: try to BREAK this verdict. Look for:
    - Hidden assumptions not listed
    - Inequality direction errors
    - Quantifier mistakes (pointwise vs uniform)
    - Missing edge cases
    - External theorems used outside their conditions

    If you find a genuine issue, describe it with severity and evidence.
    If the proof is indeed correct, say "Confirmed: no issues found" and briefly explain
    why the key steps are valid.

Reconciliation: After Codex responds, classify each finding:

Reconciliation	Meaning	Action
Both agree: issue	High confidence it's real	Keep, upgrade confidence to HIGH
Claude found, Codex disagrees	Possible false positive	Re-examine manually, add note
Codex found, Claude missed	Possible blind spot	Add to issue log, mark source = "Codex cross-review"
Both agree: verified	High confidence correct	Upgrade to "Verified (cross-confirmed)"

Write reconciliation to audit/05_adversarial/codex_cross_review.md.

7. Pass 5 — Final Report

Every generated artifact begins with the Artifact Manifest Header described in ../stat-shared-references/codex-protocol.md. The manifest lets downstream skills (proof-repair, --post-repair, theory-sharpen) load only what they need and detect staleness against the paper's current state.

Write audit/06_reports/FINAL_REPORT.md:

---
artifact: audit_final_report
scope: global
source_files: [paper.tex, supplement.tex if Mode B]
theorem_ids: [every theorem / lemma / proposition / corollary in the inventory]
assumption_ids: [every assumption in the assumption ledger]
issue_ids: [every issue in issue_log.md]
commit: [paper-repo short SHA at audit time, or content hash if not in git]
generated: [YYYY-MM-DD HH:MM]
generator: proofcheck v1.7.0 Pass 5
---

# Final Proof-Check Report: [Paper]

## Executive Summary
- Overall verdict:
- Main theorem support:
- Highest severity issue:
- Checked units: X / Y total
- Open issues: N (S0: _, S1: _, S2: _, S3: _)

## Checked Scope
- Sections checked:
- Results checked:
- Results NOT checked:

## Main Dependency Chain
[How main theorem depends on intermediate results]

## Verified Results
| Result | Status | Confidence | Notes |

## Open Issues (ranked by severity)
| ID | Severity | Confidence | Affected result | Summary |

## Conditional Results
| Result | Condition needed | Evidence |

## Recommended Repairs
1. [Repair]

## Final Judgment
[Correct / Correct modulo repairs / Incomplete / Incorrect]

Also write audit/06_reports/issue_log.md with all issues. Same manifest header (artifact: issue_log, scope: global).

Per-unit local check files in audit/04_local_checks/section_*/ carry their own manifest with scope: local, theorem_ids: [single unit being checked], and assumption_ids: [assumptions used in that unit's proof]. This lets downstream calls (and re-audit) skip loading the full FINAL_REPORT.md when they only need one unit's verdict.

audit/08_post_repair/RE-AUDIT_REPORT.md and audit/08_post_repair/diff_ledger.md likewise begin with manifest headers; their scope is usually dependency_expanded (the touched units plus their dependencies) and their commit field records the paper-repo SHA at re-audit time, allowing downstream consumers to detect whether the re-audit is fresh.

---

Common Failure Patterns (Diagnostic Checklist)

Logical

• Proving weaker statement than claimed
• Assuming the conclusion / circular dependency
• Missing induction base case
• Existence without compactness/coercivity
• Uniqueness used but not proved

Quantifier

• Pointwise result used as uniform
• Parameter-dependent constant claimed universal
• "∀ε ∃N" confused with "∃N ∀ε"
• High-prob for fixed object used over class without covering

Probability

• Missing independence
• Conditional probability mishandled
• Event intersection not adjusted
• Expectation bound used as high-prob bound
• Random index in fixed-index concentration

Analysis

• Limit/expectation exchanged without DCT/MCT/UI
• Derivative/integral exchanged without regularity
• Compactness assumed but not stated

Algebra & Inequality

• Wrong inequality direction
• Dropping absolute value
• E[XY] = E[X]E[Y] without independence
• Jensen in wrong direction
• Operator/Frobenius/vector norm confused

Asymptotic & Rate

• O_P used as deterministic O
• Constants in O(·) depend on n
• Dimension/log factors dropped
• Finite-sample theorem proved only asymptotically

Citation

• External theorem requires stronger assumptions
• External theorem conclusion weaker than needed
• Asymptotic theorem used for finite sample

---

Paper-Type Adaptations

Asymptotic Theory

• Check o_P, O_P, o, O usage correctness
• Verify CLT/Lindeberg conditions
• Watch uniform vs pointwise convergence

Concentration Inequalities

• Check tail conditions (sub-Gaussian, sub-exponential, bounded moment)
• Verify union bounds over infinite classes
• Check δ (failure probability) propagation

Optimization Theory

• Check convexity/smoothness assumptions
• Verify minima exist (compactness + continuity)
• Watch local vs global optimum confusion

Markov Chain Theory

• Check drift conditions uniform over parameter space
• Verify small set conditions simultaneous (not pointwise)
• Watch geometric vs plain ergodicity

M-Estimation

• Check identifiability (unique maximizer)
• Verify score function mean zero
• Check Hessian invertibility

---

Quick-Start Mode

If time is limited, do the minimal version:

1. Build theorem/lemma inventory
2. Identify main theorem's dependency chain
3. Check final theorem proof
4. Check each direct dependency
5. Track assumptions + notation while checking
6. Run hidden-assumption search on main chain
7. Run constants/rates check on main chain
8. Produce issue log with severity
9. State final confidence + unchecked scope

---

Session Management

After each checking session, update PROGRESS.md:

## Session Summary: [Date]
- Proof units checked:
- New verified results:
- New issues:
- Updated dependencies:
- Open blockers:
- Next targets:

Pipeline Integration

This skill is part of a 3-skill pipeline:

/proofcheck → /proof-repair → /proofcheck --post-repair → /proof-writer
  Find issues    Fix + literature    Convergence test         Write complete proofs

• Blockage reports in local checks feed directly into /proof-repair Step 1 (Issue Triage)
• Candidate literature hints in blockage reports give /proof-repair a head start on search
• Provability triage (PROVABLE AFTER WEAKENING) tells /proof-repair to use Weaken-Claim class
• After /proof-repair designs a fix, /proof-writer writes the complete corrected proof
• After patches are applied, /proofcheck --post-repair performs the convergence test (see Post-Repair Re-Audit Mode below)

To run the full pipeline:

/proofcheck papers/my-paper/paper.tex          # Step 1: find all issues (full 6-pass audit)
/proof-repair papers/my-paper/                 # Step 2: design repairs + find literature
/proofcheck --post-repair papers/my-paper/     # Step 2.5: convergence test (delta audit)
/proof-writer [specific claim to rewrite]      # Step 3: write corrected proof text

Post-Repair Re-Audit Mode (--post-repair)

Invoked as /proofcheck --post-repair papers/<paper-name>/. This is a focused delta audit, not a full 6-pass re-run. The goal is to verify that /proof-repair's output actually converged: every originally flagged issue is closed, no new fatal/major issue was introduced by the patches, and the global consistency of assumptions and dependencies still holds.

When to invoke

• Always after /proof-repair finishes a plan that touches any S0 or S1 issue. This is a HARD GATE: /proof-repair cannot mark REPAIR_PLAN.md complete until this mode has run and reports CONVERGED.
• Strongly recommended (not gated) after /proof-repair on S2/S3-only plans, because patches can still introduce silent regressions even when they target minor issues.
• After applying any human-authored patch to a paper that already has an audit/ directory, to verify the manual edit did not break a downstream proof.
• After stat-polishing --formal-statement-pass produces an EQUIVALENCE_LEDGER.md row whose proofcheck status is "required (on main chain)". A formalized assumption or statement on the dependency path to a headline theorem, rate theorem, or main-chain lemma is a semantic edit and gets the same re-audit as a proof-repair semantic edit. The ledger row is the entry point: its "touched axis" and "downstream consumers" columns scope the affected sub-DAG. See ../stat-shared-references/equivalence-ledger-protocol.md for the proofcheck depth split (targeted dependency check for off-chain rewrites; full --post-repair for on-chain).

Inputs

The mode reads, in order:

1. The original audit at papers/<paper-name>/audit/ — especially 06_reports/FINAL_REPORT.md, 06_reports/issue_log.md, 02_ledgers/{notation,assumption,constants}_ledger.md, and 03_dependencies/dependency_graph.md.
2. papers/<paper-name>/REPAIR_PLAN.md — the master repair roadmap, including the Repair Closure Matrix (see proof-repair Step 7A).
3. papers/<paper-name>/PATCHES.md — the ordered list of LaTeX modifications, including the Weaken-Claim Change Log for L5 repairs and the Assumption-Extension Change Log for L4 repairs (per the schemas in ../stat-shared-references/proof-closure-machinery.md).
4. The patched paper itself (papers/<paper-name>/paper.tex, plus supplement.tex if Mode B).
5. audit/07_repairs/codex_stress_test.md (if it exists from /proof-repair Step 5C) — the per-repair adversarial verdicts, to avoid re-litigating the same questions.
6. The per-issue repair files in audit/07_repairs/section_*/*_repair.md — these hold the Repair Ladder Defense blocks and the per-issue Assumption-Extension Change Log entries (L4 only).
7. papers/<paper-name>/EQUIVALENCE_LEDGER.md (if it exists, from stat-polishing --formal-statement-pass) — semantic formalization rewrites. Rows whose Touched axis is non-empty are treated like semantic edits: the re-audit verifies the formalized statement against the original on the recorded axis, confirms the "possible silent strengthening / weakening" column was honest, and checks that downstream consumers were propagated. A formalized statement that silently strengthened an assumption is a NEW-S0, exactly as an undocumented Weaken-Claim or Add-Assumption edit is. See ../stat-shared-references/equivalence-ledger-protocol.md.

What it does NOT do

This mode is a delta audit. It explicitly skips:

• The Pass 0 indexing of theorems and lemmas (already done; just reload).
• Step-by-step verification of proofs in units that the repair did not touch.
• Re-running the full hidden-assumption sweep across the whole paper.
• Re-running the proof-strategy classification across all units.
• Sketch detection on untouched units (already classified in the original audit).

If the user wants any of these, they should run full /proofcheck instead — but that should be rare for a normal repair cycle.

What it DOES

P1. Treat PATCHES.md as the semantic change log

For each entry in PATCHES.md, record what intentionally changed:

• Which unit was edited (lemma, theorem, assumption, definition)
• Whether the change is a STRUCTURAL EDIT (proof rewritten, new lemma inserted, missing step filled) or a SEMANTIC EDIT (claim weakened, assumption added, rate revised, quantifier tightened)
• For any SEMANTIC EDIT, read the Weaken-Claim change-log table (ORIGINAL CLAIM → REVISED CLAIM → REASON FOR WEAKENING → DOWNSTREAM IMPACT) in PATCHES.md. If the table is missing for a SEMANTIC EDIT, that itself is a fatal re-audit issue (RE-AUDIT-NEW-S0: an undocumented or unpropagated semantic change is a defect even if the algebra is correct).

The audit is performed against the REVISED claim, not the ORIGINAL claim. A claim weakening is not a defect when documented; an undocumented or unpropagated weakening is.

P2. Per-issue closure verification

For every issue in the original 06_reports/issue_log.md, look up the matching row in the Repair Closure Matrix in REPAIR_PLAN.md. Each row must have one of these terminal statuses:

• CLOSED-VERIFIED: the patch addresses the issue; re-audit confirms the unit now passes verification under the revised claim. The original S-level is gone.
• CLOSED-WEAKENED: the original claim was found unprovable; the patch weakened it; the weakening is documented in PATCHES.md and propagated to downstream units that consumed the original claim.
• CLOSED-BLOCKAGE: the unit could not be repaired; a blockage report exists; the unit is downgraded to NOT CURRENTLY JUSTIFIED in the patched paper, with all downstream consequences propagated (corollaries downgraded, the abstract and introduction no longer cite the unprovable claim).
• STILL-OPEN: the patch did not actually close the issue. This is a re-audit failure. The issue carries its original S-level into the re-audit report.
• WAIVED: the user explicitly waived the issue with documented rationale (rare, allowed for S2/S3, almost never for S0/S1).

For each CLOSED-VERIFIED row, perform a targeted re-verification of the touched unit:

• Re-read the unit's local check file from 04_local_checks/section_*/
• Apply the verification methodology (Pass 1 + Pass 2 + Step Completeness Audit) only to this unit and its direct dependencies that were also touched
• Compare the verification verdict before and after the patch
• Record the result in the re-audit report

For each CLOSED-WEAKENED row, verify the propagation:

• Identify all downstream units that consumed the original claim (use the dependency graph)
• Check that each downstream unit was either (a) also patched to use the revised claim, (b) downgraded if it required the stronger original claim, or (c) verified to still work under the weaker claim
• Any downstream unit silently using the original strength is a NEW-S0 propagation defect.

P3. New-issue scan on touched units

For every unit edited by a patch (per PATCHES.md), run a focused new-issue scan. This is narrower than the full Pass 5 adversarial pass; it asks only: did the patch introduce a new issue that did not exist in the original audit?

Checks performed:

• New hidden assumption in the patched proof (proof now relies on a condition not in the assumption block)
• New quantifier mismatch (pointwise vs uniform, ∀∃ order, etc.) introduced by the patch
• New constant or rate dependence in the patched proof (e.g., the patched bound has a worse rate than the unit's role in the dependency chain requires)
• New circular dependency created by inserting a new lemma
• New notation drift between body and supplement caused by the patch
• New cross-file reference broken by Mode B numbering changes

Issues found in this step are labeled NEW-S0, NEW-S1, NEW-S2, NEW-S3. They are distinct from STILL-OPEN issues, which are original-audit issues the patch failed to close.

P3.5. Ladder-discipline check (semantic-edit audit)

This step audits the repair ladder discipline introduced in /proof-repair Step 3. It is a documentation-and-propagation check only. The re-audit does not try to re-solve whether a cleverer Phase A repair existed; that is not the job of the convergence test.

For any repair with chosen ladder level L4 (Add-Assumption):

Verify all of the following:

1. The per-issue repair file contains a ## Repair Ladder Defense block.
2. The Phase A Exhaustion Record is present and non-empty for the relevant lower-level branches.
3. The chosen repair is marked Claim preserved: yes and Assumptions preserved: no.
4. An ## Assumption-Extension Change Log row exists for the issue.
5. The added assumption in the log matches the assumption actually inserted into the patched theorem / lemma / assumption block.
6. The Scientific-scope impact field is filled.
7. Every downstream unit listed in Propagation to downstream theorems/lemmas has a corresponding patch in PATCHES.md or a documented re-verification.
8. The patched paper's assumption ledger reflects the new assumption consistently and without contradiction.

If any item fails, record a new re-audit issue:

• NEW-S0 for missing log row, missing propagation, or silent assumption injection
• NEW-S1 for incomplete scope-impact documentation or inconsistent assumption bookkeeping

For any repair with chosen ladder level L5 (Weaken-Claim):

Verify all of the following:

1. The per-issue repair file contains a ## Repair Ladder Defense block.
2. The Phase A Exhaustion Record is present and non-empty for the relevant lower-level branches.
3. The chosen repair is marked Claim preserved: no.
4. A ## Weaken-Claim Change Log row exists for the issue / patch.
5. The revised claim in the log matches the claim actually inserted into the patched paper.
6. Every downstream consumer listed in the change log has a corresponding propagation patch or documented downgrade.
7. The abstract, introduction, corollaries, and applications no longer silently use the original stronger claim.

If any item fails, record a new re-audit issue:

• NEW-S0 for missing change-log row, silent weakening, or missing downstream propagation
• NEW-S1 for incomplete documentation of the weakening rationale

For repairs at L1, L2, L3 (Phase A) or L6 (blockage):

Verify only that the Repair Ladder Defense block is present with the correct level recorded. No semantic-edit log is required for Phase A repairs.

Scope limit of this check:

This ladder-discipline check verifies:

• presence of the required escalation artifacts,
• propagation of semantic edits,
• consistency of the patched paper with those edits.

It does not require the re-audit to prove that no better Phase A repair existed. Disputing the choice of ladder level itself is out of scope; the re-audit's job is to verify the discipline, not to second-guess the design.

P3.7. Citation lock manifest consistency check (read-only)

Read papers/<paper-name>/cited_results.lock.md per ../stat-shared-references/cited-results-lock-protocol.md. The re-audit performs a read-only consistency check:

• Every row's Reference resolves to an existing cache entry (paper:<bibkey>#<result_id> is in ~/.claude/literature_cache/papers/<bibkey>.md).
• Every row's Entry hash at decision matches the cache entry's current hash, OR the row is flagged STALE in the validation report.
• Every load-bearing row (purpose in {load_bearing, benchmark_claim, comparative}) is at independently_checked or higher; if not, the row is flagged GAP.
• Every Axis or lineage bridge recorded column for partial or same_family rows points to an existing artifact (Lemma A.4, PATCHES.md Patch-7, etc.).
• Every patched-paper citation (recorded by the body's \cite{<bibkey>} calls intersected with the Closure Matrix's referenced units) has at least one row in the lock manifest.

Findings are written to papers/<paper-name>/audit/08_post_repair/lock_manifest_validation.md. STALE and GAP flags are warnings; the verification floor gap on load-bearing rows is a blocker (the convergence decision in Step P6 cannot advance to CONVERGED while any load-bearing row is below independently_checked).

The check is read-only; the re-audit does not edit cited_results.lock.md. Discrepancies are reported back to the user, who decides whether to re-run the originating skill (stat-paper-write, proof-repair, etc.) to upgrade or re-bind the row.

P4. Global consistency re-run (assumption ledger + dependency graph only)

Re-build the assumption ledger and the dependency graph from the patched paper. Compare against the originals:

• New assumptions introduced anywhere → must be consistent with the existing assumption set (no contradictions) and must be acknowledged in the relevant statement (no silent injection)
• Removed assumptions → must be justified (e.g., the patch tightened a lemma so the assumption is no longer used)
• New dependency edges → must not create circularity
• Notation ledger drift → must be reconciled across body and supplement

This step is the integration test. It catches the silent breakage that Step 5C adversarial per-repair tests cannot see, because per-repair tests do not have a global view of the post-patched paper.

P5. Assumption / Rate Diff Ledger

Generate audit/08_post_repair/diff_ledger.md. This is a compact, machine-readable diff across the entire dimensional structure of the paper:

# Assumption / Rate Diff Ledger

Generated by /proofcheck --post-repair on [date]. Compares the patched paper
against the pre-patch audit baseline.

## Assumption diff
| Assumption | Pre-patch scope | Post-patch scope | Change | Justified? |
|---|---|---|---|---|
| A1 (i.i.d.) | Global | Global | unchanged | n/a |
| A2 (strong convexity) | Global | Sec 3 only | NARROWED | yes (Patch 4 splits cases) |
| A_new1 (4th moment) | — | D.2 local | ADDED | yes (Patch 7, required by Lemma B.5 fix) |
| A_old3 (Hessian invertibility) | Global | — | DROPPED | yes (Patch 2 supplies it from C.3) |

## Rate / constant diff
| Object | Pre-patch | Post-patch | Change | Downstream impact |
|---|---|---|---|---|
| Thm 2.1 rate | $O(n^{-1/2})$ | $O(n^{-1/2})$ | unchanged | n/a |
| Cor 2.2 rate | $O(n^{-1/2})$ | $O(n^{-1/2} \log n)$ | DEGRADED by log | Sec 5 application paragraph now overstates; PATCH NEEDED |
| Lemma C.3 constant | universal | $\propto p^{1/2}$ | DIMENSION-DEPENDENT | review whether Thm 2.1 still holds uniformly in $p$ |

## Probability level diff
| Statement | Pre-patch | Post-patch | Change |
|---|---|---|---|
| Thm 3.1 high-prob | $1 - 2e^{-c n}$ | $1 - 2 e^{-c \log n}$ | WEAKER probability level |

## Norm / metric diff
| Object | Pre-patch norm | Post-patch norm | Change |
|---|---|---|---|

## Sample-size regime diff
| Statement | Pre-patch regime | Post-patch regime | Change |
|---|---|---|---|

## Dependency requirement diff
| Edge | Pre-patch direction | Post-patch direction | Change |
|---|---|---|---|

## Summary
Total diffs: N
Justified: M
Unjustified or unpropagated: K  ← K > 0 means re-audit is NOT CONVERGED

The diff ledger is the single most useful artifact for catching the failure mode Codex flagged: most bad repairs are not algebraic errors; they are silent strengthening, silent rate degradation, or silent incompatibility across lemmas. The ledger forces these into the open.

A row is Unjustified or unpropagated when:

• An assumption was added without an Assumption-Extension Change Log row in the per-issue repair file (L4 routing per ../stat-shared-references/proof-closure-machinery.md).
• A claim was weakened without a Weaken-Claim Change Log row in REPAIR_PLAN.md and the per-issue repair file (L5 routing per proof-closure-machinery.md).
• A rate degraded without the downstream consumers being updated.
• A probability level weakened without the corollaries being adjusted.
• A norm changed without the related statements being reconciled.

Any unjustified row triggers NEW-S0 or NEW-S1 in the convergence decision. L4 (Add-Assumption) and L5 (Weaken-Claim) route to different change logs; an L4 patch documented only in the Weaken-Claim log is still Unjustified or unpropagated.

P6. Convergence decision

The re-audit produces one of three terminal states.

• CONVERGED: every original S0/S1 issue is CLOSED-VERIFIED, CLOSED-WEAKENED, or CLOSED-BLOCKAGE; no STILL-OPEN S0/S1; no NEW-S0 or NEW-S1; the diff ledger has zero unjustified rows; the lock manifest validation (Step P3.7) reports no load-bearing row below independently_checked and no STALE entry on a load-bearing row. The repair phase is complete; the user may advance to /theory-sharpen or submission.
• NOT CONVERGED — RE-REPAIR REQUIRED: at least one of STILL-OPEN-S0, STILL-OPEN-S1, NEW-S0, NEW-S1, or an unjustified diff row remains. The user invokes /proof-repair --from-reaudit to address only the residual issues. Auto-triggering is forbidden; the user must explicitly confirm.
• NOT CONVERGED — HUMAN INTERVENTION REQUIRED: the re-audit detected a change in theorem intent, paper-level claim, or dependency structure that exceeds what a re-repair cycle can handle. Examples: the patched paper's contribution is now meaningfully different from the abstract; a Weaken-Claim repair was not propagated to the introduction's stated rate; the new assumption changes the paper's empirical scope. The user must review and decide whether to revert, restate the paper's contribution, or change venue.

The convergence decision is written to audit/08_post_repair/CONVERGENCE_VERDICT.md.

Outputs

papers/<paper-name>/audit/08_post_repair/
  RE-AUDIT_REPORT.md           # Main delta-audit report
  diff_ledger.md               # Assumption / rate / constant / probability / norm / regime diff
  CONVERGENCE_VERDICT.md       # CONVERGED / NOT CONVERGED + reason
  per_issue_closure.md         # Per-original-issue closure verification
  new_issues.md                # NEW-S0/S1/S2/S3 detected by patches

Every file in 08_post_repair/ begins with the Artifact Manifest Header (see ../stat-shared-references/codex-protocol.md). For these post-repair artifacts:

• scope: dependency_expanded (the touched units plus their direct dependencies)
• theorem_ids lists every unit whose patch is verified by this artifact
• assumption_ids lists every assumption referenced (original + new from patches)
• issue_ids lists every original issue verified for closure plus every NEW-S* issue created
• commit is the paper-repo short SHA at re-audit time (so downstream can detect staleness if a later patch lands)

Interaction with Codex Step 5C

The per-repair Codex adversarial stress-test in /proof-repair Step 5C and this post-repair re-audit are complementary, not redundant:

• Step 5C asks: "Can this individual repair be broken in isolation?" — local adversarial test.
• --post-repair asks: "Did the patched paper as a whole converge?" — integration test.

Step 5C cannot detect:

• A repair to Lemma 3 that no longer correctly feeds Theorem 1
• A weakened rate in a lemma that breaks a corollary's rate
• A new assumption in Lemma 5 that contradicts an existing assumption in Lemma 8
• A silent change in the paper's headline claim that downstream sections do not reflect

--post-repair is the only mechanism that catches these. Both must exist; neither subsumes the other.

When NOT to run

• The user has only changed comments, typos, or notation cosmetics that the diff ledger would record as zero-impact. A full re-audit is overkill.
• The original audit found zero S0/S1/S2 issues (paper was already verified) and no patches were applied. There is nothing to re-audit.
• The user is actively rewriting the paper's framework and the original audit no longer reflects the current paper structure. Re-run full /proofcheck instead.

Final Acceptance Criteria

A proof check is complete only when:

• Every main theorem dependency identified
• Every critical dependency locally checked or marked conditional
• No unresolved S0 issues
• All S1 issues repaired, downgraded, or explicitly reported
• Assumption propagation checked
• Notation drift checked
• Constants/rates/probability/quantifiers checked for main chain
• Circular dependencies ruled out or reported
• Final report states checked AND unchecked scope honestly

A repair cycle is complete only when, after /proof-repair:

• /proofcheck --post-repair has been invoked (HARD GATE if any S0 or S1 issue existed in the original audit)
• CONVERGENCE_VERDICT.md reports CONVERGED
• Every original S0/S1 issue has a terminal closure status (CLOSED-VERIFIED, CLOSED-WEAKENED, or CLOSED-BLOCKAGE)
• The diff ledger has no unjustified rows
• No NEW-S0 or NEW-S1 issues introduced by patches remain open