# Proofcheck

> Systematically verify mathematical proofs in statistics/ML theory paper appendices. Use when user says "proof check", "check proofs", "verify proofs", "audit paper", "检查证明", "证明验证", or wants to verify correctness of a paper's mathematical proofs.

- Skill: `gyf9712/proofcheck` (Agent Skill)
- Install (CLI): `npx skillmds@latest add gyf9712/proofcheck`
- Raw SKILL.md: https://api.skillmd.com/api/skills/gyf9712/proofcheck/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Security
- Author: gyf9712 (https://skillmd.com/u/gyf9712)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/gyf9712/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.

```bash
# 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)

```bash
# 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`:
```markdown
## 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:

```bash
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 `\ref`s.
- **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**:
```markdown
### 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:

```markdown
## 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:

```markdown
### 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:

```markdown
### 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`:

```markdown
---
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`:

```markdown
## 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

…(truncated)