proof-repair

name	proof-repair
description	Generate self-consistent repair plans for mathematical proof issues found by /proofcheck, with literature-backed support. For each problematic assumption, model, proposition, or theorem, proposes fixes that preserve the full dependency chain and searches arXiv, Semantic Scholar, and Google Scholar for new references to support repairs. Use when user says "repair proofs", "fix proof issues", "修复证明", "proof repair", "修正计划", "fix theorem", "repair assumptions", or wants to go from proof audit to actionable repair plan with literature support.
argument-hint	["path-to-paper-dir or path-to-audit-dir"]
allowed-tools	Bash(*), Read, Write, Edit, Grep, Glob, Agent, WebSearch, WebFetch
model	opus

Proof-Repair — Literature-Backed Repair Plans for Mathematical Proofs

🔬 Model Recommendation: Run this skill on Claude Opus for best results. Repair design + literature verification requires deep reasoning. If your session is not on Opus, run /model opus before invoking. Heavy reasoning (literature search, verification, full proof writing) will use Opus sub-agents.

Takes a /proofcheck audit (or a raw .tex file with known issues) and produces self-consistent repair plans with new literature references for every fixable issue.

Pipeline position:

/proofcheck → [THIS SKILL] → /proof-writer
  Find issues    Fix + literature    Write complete proofs

Upstream: /proofcheck (produces audit/ with provability triage + blockage reports) This skill: audit/ → REPAIR_PLAN.md + patched .bib + per-unit repair files Downstream: /proof-writer (writes complete corrected proofs for each repair)

Context: $ARGUMENTS

---

Step 0: Locate Inputs

Parse $ARGUMENTS to find the paper workspace.

Expected structure (created by /proofcheck):
papers/<paper-name>/
  paper.tex
  CHECK_PLAN.md
  EXECUTION_ORDER.md
  audit/
    01_index/theorem_inventory.md
    02_ledgers/{notation,assumption,constants}_ledger.md
    03_dependencies/dependency_graph.md
    04_local_checks/section_*/*_check.md
    05_adversarial/{hidden_assumptions,counterexamples}.md
    06_reports/{issue_log.md, FINAL_REPORT.md}

Read these files in order:

1. audit/06_reports/FINAL_REPORT.md — executive summary, all open issues
2. audit/06_reports/issue_log.md — detailed issue list with severity
3. audit/03_dependencies/dependency_graph.md — what depends on what
4. audit/02_ledgers/assumption_ledger.md — all assumptions and their scope
5. CHECK_PLAN.md — proof architecture understanding

If no audit/ exists, tell the user to run /proofcheck first, or offer to run a lightweight inline check on the specific unit they point to.

New in v2: Also read provability triage and blockage reports from local check files:

• Units marked PROVABLE AFTER WEAKENING → pre-classify as Weaken-Claim repair
• Units marked NOT CURRENTLY JUSTIFIED → pre-classify as Replace-Technique or blockage
• Candidate literature hints from blockage reports → seed the literature search (Step 4)

Step 0B: Detect Reference Mode (MANDATORY before any LaTeX patch)

JASA / AoS / Biometrika / JRSS-B / Econometrica submissions typically separate Main Text and Supplementary Material into TWO compiled PDF files. LaTeX \ref{} does NOT work across files (without the fragile xr package), so every cross-file citation must use hard-coded numbers, not \ref{}.

Detect the paper's reference mode BEFORE writing any LaTeX patches:

Mode A: Single-file paper (one .tex compiles to one PDF)

• Most arXiv preprints, NeurIPS/ICML/ICLR (one combined PDF)
• Use \label{...} and \ref{...} / \eqref{...} / \cref{...} freely
• Any new lemma/equation gets a \label{}

Mode B: Two-file submission (separate main.tex + supplement.tex → two PDFs)

• Common for JASA, AoS, Biometrika, JRSS-B, Econometrica, JBES
• Identify by:
  • Multiple top-level .tex files (e.g., paper.tex + supplement.tex / appendix.tex / supp.tex)
  • Author's cover_letter.txt or submission notes mentioning "supplement"
  • Section labeled "Online Supplement" / "Supplementary Material" at end of paper
• Reference rules:
  • Within the same file → use \ref{...} as normal
  • Across files (main↔supplement) → NEVER use \ref{} (it won't compile)
  • Cross-file references must use hard-coded numbers:
    • "Lemma S.3" (S prefix for supplement items)
    • "Theorem 2.1 of the main text" (when supplement refers to main)
    • "equation (S.7)" (equations in supplement use S.N numbering)
  • When patching, you must KNOW the supplement's lemma numbering scheme to insert the right hard-coded number

Detection procedure:

# Count top-level .tex files (excluding those \input'd by others)
find papers/<paper-name> -maxdepth 2 -name "*.tex" -type f

# Check for explicit supplement files
ls papers/<paper-name>/{supp*,supplement*,appendix*}.tex 2>/dev/null

# Check for S-prefix labels (signal of two-file mode)
grep -l "\\label{.*:S\\.\|\\label{S" papers/<paper-name>/*.tex

If two .tex files exist with parallel content (one shorter "main", one longer "supp"), this is Mode B. Confirm with the user before proceeding.

Where in REPAIR_PLAN.md to record:

## Reference Mode
Mode: [A: single-file / B: two-file main+supplement]
Files:
  - paper.tex (main text)
  - supplement.tex (supplementary material)  [if Mode B]
Numbering scheme (Mode B):
  - Main text: 1, 2, 3, ...
  - Supplement: S.1, S.2, S.3, ... (or "S1, S2, S3")
Cross-file citation style: hard-coded numbers + "of the supplement" / "of the main text"

All LaTeX patches in Step 7 (PATCHES.md) MUST respect this mode.

---

Step 1: Issue Triage & Repair Classification

Read ALL issues from issue_log.md and each 04_local_checks/ file. Build a Repair Triage Table:

| Issue ID | Severity | Unit | Issue Type | Repair Class | Downstream Impact | Priority |
|----------|----------|------|------------|-------------- |-------------------|----------|
| I-01 | S0 | Lemma C.3 | Hidden assumption | Add-Assumption | Thm 2.1, Cor 2.2 | P0 |
| I-02 | S1 | Thm 3.1 | Rate mismatch | Weaken-Claim | Final theorem | P0 |
| I-03 | S1 | Prop B.2 | Missing step | Insert-Lemma | Lemma B.4 | P1 |
| I-04 | S2 | Def 2.3 | Notation drift | Notation-Fix | 5 units | P2 |

Repair Classes (choose one per issue)

Class	When to use	Needs literature?
Add-Assumption	Proof uses unstated condition	Yes — find papers with similar assumption or weaker alternative
Weaken-Claim	Theorem claims more than proved	Maybe — find if stronger result exists elsewhere. MANDATORY: produce a Weaken-Claim Change Log entry per the schema in stat-shared-references/proof-closure-machinery.md (5 columns: Patch ID, Original claim verbatim, Revised claim verbatim, Reason for weakening, Downstream impact). Without the log entry, /proofcheck --post-repair will flag this as NEW-S0 (undocumented semantic change).
Strengthen-Proof	Gap in reasoning, but claim is likely true	Yes — find technique/lemma to fill the gap
Insert-Lemma	Missing intermediate step	Yes — may exist as known result in literature
Fill-Skipped-Steps	Author skipped intermediate steps; proofcheck flagged NONTRIVIAL or UNRECONSTRUCTIBLE jumps	Sometimes — TRIVIAL/VERIFIABLE need no refs, NONTRIVIAL may need a named technique, UNRECONSTRUCTIBLE may need new lemma + refs
Expand-Sketch-to-Proof	proofcheck flagged the unit as SKETCH-ONLY or PARTIAL-SKETCH (entire proof body is outline, not rigorous derivation)	Often — sketch usually relies on cited techniques that need to be properly invoked with prerequisites verified. The "expansion" is the entire proof; literature support helps confirm cited techniques apply
Replace-Technique	Current technique fundamentally flawed	Yes — find alternative proof strategy
Fix-Constants	Rates, bounds, or constants wrong	Maybe — check if correct constants known
Fix-Quantifiers	Pointwise↔uniform, ∀∃ order, etc.	Maybe — find uniform versions of cited results
Notation-Fix	Symbol drift, type mismatch	No
Citation-Fix	External theorem misapplied	Yes — find correct version or alternative theorem

Expand-Sketch-to-Proof repair workflow (when unit was SKETCH-ONLY / PARTIAL-SKETCH)

HARD PRIORITY RULE: Any unit flagged SKETCH-ONLY or PARTIAL-SKETCH by /proofcheck is automatically P0 priority for this repair class, regardless of severity ranking on other dimensions. Sketches MUST be expanded — they cannot be deferred to "later revision" or "future work".

The reason: a sketch is not just a low-quality proof; it is the absence of verification. Other issues (constants, quantifiers, etc.) are corrections of something that exists. A sketch needs the proof to be CREATED. Until it exists, the theorem's status is unsupported.

When proofcheck flags a unit as SKETCH-ONLY or PARTIAL-SKETCH, the repair is to write the entire proof — not just fix a step. This is distinct from Fill-Skipped-Steps (which fills isolated gaps inside an otherwise rigorous proof).

Approach:

1. Read the sketch carefully — what high-level strategy does it claim? Extract the proof outline as a numbered list of intended steps.

2. For each intended step:

   • Is the cited technique actually applicable here? (verify prerequisites)
   • Is there a standard reference for the technique? Cite it explicitly
   • Write out the actual derivation, not just the verbal claim

3. Trigger /proof-writer with the original claim + extracted outline, asking for a COMPLETE proof (not a sketch — see proof-writer's anti-sketch rules). The skill should refuse to produce another sketch.

4. Verify the expanded proof:

   • Does it conclude the original claim exactly?
   • Are all assumptions used? Are any extra assumptions snuck in?
   • Send to /proofcheck for re-audit after expansion

5. Literature support:

   • For each non-trivial technique invoked, cite the canonical reference
   • If the sketch said "similar to [Paper Z]", verify Paper Z actually has the full proof and adapt it explicitly (not just point at it)

Output: a complete proof replacing the sketch, with explicit derivations and proper citations. Marked in PATCHES.md as Patch: replace sketch with full proof.

Hard completion rule: REPAIR_PLAN.md cannot be marked complete while ANY sketch unit remains unexpanded. Each detected sketch must end in one of two terminal states:

• EXPANDED: full proof written by /proof-writer, re-classified as COMPLETE by /proofcheck
• BLOCKAGE: blockage report written explaining why the sketch cannot be expanded (theorem itself is downgraded to NOT CURRENTLY JUSTIFIED)

There is no third option. "Partially expanded" or "expansion deferred to revision" are NOT terminal states.

The REPAIR_PLAN.md must contain a sketch-tracking section:

## Sketch Expansion Tracker (auto-generated)

| Unit | Sketch class (from proofcheck) | Expansion state | Final status |
|------|------------------------------|----------------|-------------|
| Thm 3.1 | SKETCH-ONLY | EXPANDED | COMPLETE proof written; verified by re-check |
| Lemma B.2 | PARTIAL-SKETCH | EXPANDED | 4 gaps filled with full derivations |
| Cor 5.3 | SKETCH-ONLY | BLOCKAGE | Cited technique inapplicable; theorem downgraded |

Outstanding sketches: 0  ← MUST be 0 for plan to be marked complete

If any row has Expansion state ≠ EXPANDED / BLOCKAGE, the skill returns to expansion before producing the final plan.

Common failure modes for this repair class:

• The sketch was actually NOT provable as stated (was hiding the real issue) → downgrade to NOT CURRENTLY JUSTIFIED + blockage report (this is BLOCKAGE state, valid terminal)
• The cited technique doesn't actually apply → reclassify as Replace-Technique → still must expand the resulting alternative proof
• Expansion reveals a missing assumption → reclassify as Add-Assumption → still must expand the resulting proof under the new assumption

Fill-Skipped-Steps repair workflow (special handling)

This class handles skips identified by /proofcheck's Step Completeness Audit. Workflow varies by the skip's classification:

VERIFIABLE skips (S3):

• Re-verify proofcheck's reconstruction is correct
• Write out the 2-5 intermediate steps explicitly
• LaTeX patch: insert the steps between the existing equations
• No literature needed — uses standard manipulations only

NONTRIVIAL skips (S1):

• Identify the non-obvious bridging idea
• If it's a named technique (e.g., Sherman-Morrison, dominated convergence, Borel-Cantelli), cite the standard reference
• If it's a problem-specific lemma, write it as a new lemma (via /proof-writer)
• LaTeX patch: insert either the cited bridging step or the new lemma + its use

UNRECONSTRUCTIBLE skips (S0):

• Treat as a genuine gap — do NOT manufacture a bridge
• Investigate whether: (a) the original proof is wrong (the jump doesn't actually hold) (b) the original proof uses an unstated assumption (→ Add-Assumption repair) (c) a different proof technique is needed entirely (→ Replace-Technique)
• If still unable to bridge after literature search, write a Blockage Report and recommend the author either provide the bridge or weaken the claim

Priority Rules

• P0: S0 issues + any S1 issue on the critical path to main theorem
• P1: S1 issues not on critical path + S2 issues affecting ≥3 downstream units
• P2: Remaining S2 + all S3

---

Step 2: Dependency Impact Analysis

For each P0 and P1 issue, trace the full downstream impact using the dependency graph:

## Impact Analysis: I-01 (Lemma C.3 — hidden invertibility assumption)

### Direct dependents
- Lemma C.5 (uses C.3 conclusion directly)
- Theorem 2.1 (assembles C.3 + C.5)

### Transitive dependents
- Corollary 2.2 (follows from Thm 2.1)
- Section 4 applications (all use Cor 2.2)

### Repair constraint
Any fix to C.3 must:
1. Not strengthen assumptions of Thm 2.1 beyond what the paper's intro promises
2. Preserve the rate O(n^{-1/2}) in Thm 2.1
3. Keep the constant universal (not parameter-dependent)

### Cascading repairs needed?
- If we add "H is invertible" to C.3, must verify C.5 and Thm 2.1 still hold
- Check: does the application section provide invertibility naturally?

Build a Repair Dependency DAG: some repairs must happen before others (e.g., fixing a base lemma assumption before fixing the theorem that uses it).

---

Step 3: Enforce the Repair Priority Ladder (HARD GATE)

Before generating candidate repairs, classify each candidate by ladder level and by repair class. The full ladder definition (Phase A / B / C, L1-L6), the mapping from levels to repair classes, the sibling-not-ordered rules for L2/L3 and L4/L5, and the hard enforcement requirements all live in stat-shared-references/proof-closure-machinery.md under "Repair Priority Ladder".

Operational summary for this step:

1. For each issue from Step 1, identify the relevant Phase A branches (L1 internal correction / L2 supporting lemma / L3 alternative technique). Attempt them with concrete candidate sketches.
2. A candidate enters Phase B (L4 Add-Assumption or L5 Weaken-Claim) only after the per-issue repair file records a Phase A exhaustion entry for the relevant branches. The Phase A Exhaustion Record block schema is in proof-closure-machinery.md.
3. L4 requires an Assumption-Extension Change Log entry; L5 requires a Weaken-Claim Change Log entry. Both schemas are in proof-closure-machinery.md. A Phase B repair without the matching log is invalid and is demoted to L6 (Blockage / NOT CURRENTLY JUSTIFIED).
4. The chosen repair's Repair Ladder Defense block (schema in proof-closure-machinery.md) must be written into the per-issue repair file before the repair is admitted to Step 5 (Complete-Proof Writing).

/proofcheck --post-repair enforces all of the above by checking the schema instances on the patched paper.

---

Step 3B: Generate Candidate Repairs (per issue)

For each issue, generate 1-3 candidate repair strategies, each typed with a ladder level in addition to invasiveness:

## Repair Candidates: I-01 (Lemma C.3 — hidden invertibility assumption)

### Candidate A: Add explicit assumption (Ladder level: L4 / invasiveness: LOW within Phase B)
- Repair class: Add-Assumption
- Claim preserved: yes; Assumptions preserved: no
- Add "Assume H(θ) is invertible for all θ ∈ Θ" to Lemma C.3 statement
- Propagate to Theorem 2.1 assumptions
- Check: is this already implied by existing Assumption 2 (strong convexity)? If yes, this is actually an L2 candidate, not L4.
- Risk: may narrow the theorem's applicability

### Candidate B: Insert supporting lemma (Ladder level: L2 / invasiveness: MEDIUM)
- Repair class: Insert-Lemma
- Claim preserved: yes; Assumptions preserved: yes
- Add Lemma C.3' proving H(θ) invertibility under existing assumptions
- Needs: strong convexity (Assumption 2) ⟹ H(θ) ≻ 0
- Advantage: Phase A repair; no main-theorem assumption change
- Literature needed: standard result connecting strong convexity to Hessian invertibility

### Candidate C: Alternative technique — Avoid inversion entirely (Ladder level: L3 / invasiveness: HIGH)
- Repair class: Replace-Technique
- Claim preserved: yes; Assumptions preserved: yes
- Replace matrix inversion step with pseudo-inverse + regularization
- Requires reworking Eqs. (47)-(52)
- May change constants but preserves rate
- Literature needed: perturbation theory for pseudo-inverse in M-estimation

Note that Candidate A above is L4 (Phase B). If Candidate B (L2) or C (L3) reaches PROVABLE AS STATED, the ladder rule requires choosing B or C over A; A may be selected only with a documented Phase A exhaustion record.

Repair Quality Criteria

Each candidate must satisfy ALL of:

1. Mathematically correct — the repaired proof must be valid
2. Self-consistent — does not contradict other assumptions or break downstream results
3. Minimal — prefer the least invasive fix
4. Preserves claims — ideally keeps the theorem statement unchanged (or weakens minimally)
5. Literature-supportable — can cite existing results for any new technique/lemma used

Feasibility Triage per Candidate (from /proof-writer methodology)

Before investing in literature search, classify each candidate:

Status	Meaning	Next action
PROVABLE AS STATED	The repaired claim follows from (original + new) assumptions	Proceed to literature search + full proof writing
PROVABLE AFTER WEAKENING	Repair works but requires weaker theorem statement	Document the weakened claim explicitly, then proceed
NOT CURRENTLY JUSTIFIED	Cannot see how to make this repair work	Write blockage report, try next candidate

Anti-fabrication rule: If NO candidate reaches PROVABLE status, do NOT force a repair. Instead write a Blockage Report:

• Exact reason no repair works
• What additional theoretical development would be needed
• Whether the main theorem survives if this unit is dropped
• Honest assessment: is the paper's claim false, or just unproven?

Mandatory output blocks per candidate

Each candidate selected for the next step (Step 4 literature search and Step 5 complete-proof writing) requires the following mandatory blocks in its per-issue repair file at audit/07_repairs/section_*/*_repair.md. The schemas live in stat-shared-references/proof-closure-machinery.md and are not duplicated here.

• Always: ## Repair Ladder Defense block (chosen level + repair class + claim/assumption preservation + Phase A Exhaustion Record + Phase B Justification if L4/L5 + Semantic-Edit Log Pointer + Blockage Pointer if L6).
• If chosen class is Weaken-Claim (ladder L5) or candidate feasibility was PROVABLE AFTER WEAKENING: ## Weaken-Claim Change Log block per the schema in stat-shared-references/proof-closure-machinery.md (5 columns: Patch ID, Original claim verbatim, Revised claim verbatim, Reason for weakening, Downstream impact). Without this block, the repair is demoted to NOT CURRENTLY JUSTIFIED.
• If chosen class is Add-Assumption (ladder L4): ## Assumption-Extension Change Log block per the schema in proof-closure-machinery.md (7 columns: Issue ID, Original assumption set, Added assumption verbatim, Natural weaker variant considered, Why the weaker variant fails, Scientific-scope impact, Propagation to downstream theorems/lemmas). The "Natural weaker variant considered" column is the local-minimality defense. Without this block, the repair is demoted to NOT CURRENTLY JUSTIFIED.

The Downstream impact / Propagation columns in both Change Logs are propagation contracts: every listed unit must have a corresponding patch in PATCHES.md. The re-audit treats unpropagated downstream consumers as NEW-S0 (silent overstatement in the patched paper).

Proof Strategy Selection for Repairs

When a repair involves writing new proof content (Insert-Lemma, Strengthen-Proof, Replace-Technique), choose a proof strategy explicitly:

• Direct: when the result follows from straightforward calculation or known facts
• Contradiction: when the negation leads to a clear impossibility
• Induction: when the result has recursive structure (iterations, sequence convergence)
• Reduction: when a known theorem handles the core difficulty
• Construction: when we need to exhibit a specific object (counterexample, witness)
• Coupling: for probabilistic arguments comparing two processes
• Optimization / variational: for existence, bounds via optimization

Record the chosen strategy in the repair specification — this guides /proof-writer later.

---

Step 4: Literature Search for Repair Support

For EACH candidate repair that needs literature support, run a targeted multi-source search.

Guiding principle: A proof repair is only as credible as its references. Prioritize results from top-tier venues; treat unreviewed preprints as supplementary evidence only.

4A: Cache-consult first (mandatory)

Before invoking any web tool, consult the durable literature cache at ~/.claude/literature_cache/. The protocol lives in stat-shared-references/literature-cache-protocol.md (router with Minimum Load Map). For this step, the typical loads are:

• literature-cache-protocol.md (router) — always.
• applicability-axes.md — if the candidate is load_bearing / benchmark_claim / comparative and an axis check is needed.
• cache-verification-states.md — when fetching new entries; when the entry is below source_checked; when source version may be stale.

Procedure:

1. Read the cache INDEX (~/.claude/literature_cache/INDEX.md) to identify cache hits matching the repair's literature need (technique, anchor paper, schema, comparator).
2. For each cache hit, do a result-scoped load (Read with offset/limit) of the matching per-result entry. Do not dump full paper containers.
3. For each cache miss, proceed to the web search workflow below, then write the proposal back to ~/.claude/literature_cache/inbox/<bibkey>.draft.md per the inbox protocol in cache-verification-states.md.

Credibility tier classification (next subsection) applies to BOTH cache hits and fresh web results.

4B: Venue Credibility Tiers

All search results MUST be classified by venue tier before recommendation.

Tier 1 — Gold Standard (prefer these; a single T1 citation can anchor a repair)

Domain	Venues
Statistics "Big 4"	Annals of Statistics (AoS), Journal of the American Statistical Association (JASA), Journal of the Royal Statistical Society Series B (JRSS-B), Biometrika
Probability	Annals of Probability, Probability Theory and Related Fields, Stochastic Processes and their Applications
Mathematics	Annals of Mathematics, Inventiones Mathematicae, Acta Mathematica, CPAM
ML/AI Top Conferences	NeurIPS, ICML, ICLR, COLT, ALT, AISTATS
ML Journals	Journal of Machine Learning Research (JMLR), Machine Learning (Springer)
Econometrics	Econometrica, Journal of Econometrics (JOE), Review of Economic Studies, Journal of Business & Economic Statistics (JBES)
Optimization	Mathematical Programming, SIAM Journal on Optimization, Mathematics of Operations Research
Applied Math / Numerical	SIAM Review, SIAM Journal on Numerical Analysis, Mathematics of Computation
Authoritative Textbooks	Springer GTM/Lecture Notes, Cambridge Tracts, Princeton Series in Applied Mathematics

Tier 2 — Strong (acceptable, especially alongside a T1 reference)

Domain	Venues
Statistics	Electronic Journal of Statistics (EJS), Bernoulli, Statistica Sinica, Scandinavian Journal of Statistics
ML/AI	AAAI, IJCAI, UAI, KDD, JAIR
Math	Transactions AMS, Journal of Functional Analysis, Advances in Mathematics
Econometrics	Econometric Theory, Journal of Applied Econometrics, Econometric Reviews
Applied	IEEE Trans. on Information Theory, IEEE Trans. on Signal Processing

Tier 3 — Supplementary (use only when T1/T2 unavailable; flag as lower confidence)

Source	Use case
arXiv preprints (not yet published)	Cutting-edge technique, no peer-reviewed version yet
Workshop papers (NeurIPS/ICML workshops)	Preliminary results
Technical reports / working papers	University reports, NBER working papers
Conference papers outside top tier	Regional or secondary conferences

Tier 4 — Avoid (do NOT cite unless absolutely no alternative exists)

Source	Reason
Unpublished manuscripts with no arXiv ID	No traceability
Blog posts, lecture slides, StackExchange	Not citable in academic work
Retracted papers	Compromised
Predatory journals (check Beall's list heuristics)	Unreliable peer review

Credibility Scoring Rules

1. T1 published + high citations (≥50) → Credibility: GOLD — use as primary anchor
2. T1 published + moderate citations (10-49) → Credibility: STRONG — reliable
3. T1 published + low citations (<10) or very recent → Credibility: ACCEPTABLE — verify theorem carefully
4. T2 published → Credibility: GOOD — acceptable, prefer T1 if available
5. T3 arXiv preprint, ≥20 citations → Credibility: CONDITIONAL — acceptable if theorem is self-contained and verifiable
6. T3 arXiv preprint, <20 citations → Credibility: WEAK — use only if no alternative; must verify theorem step-by-step
7. T4 any → Credibility: REJECT — do not cite

When two references support the same repair, always prefer the higher-tier one. When a preprint exists alongside its published version, always cite the published version.

4C: Formulate Search Queries

Convert each repair need into 2-3 precise search queries, targeting different source types:

Issue: Hidden invertibility assumption in M-estimation Hessian
Repair: Prove invertibility from strong convexity

Query 1 (textbook/classic): "strong convexity Hessian positive definite" 
  → target: T1 textbooks (Boyd, Nesterov, Rockafellar)
Query 2 (journal result): "minimum eigenvalue Hessian strongly convex M-estimation"
  → target: AoS, JASA, Biometrika, JMLR, Econometrica
Query 3 (recent technique): "M-estimator regularity condition relaxation"
  → target: recent NeurIPS/ICML/COLT + stat.TH arXiv

4D: Multi-Source Search (parallel)

Launch parallel searches using Agent tool, each with venue-awareness:

Agent 1: arXiv + Published Venue Cross-Check

Search arXiv for: [query]
Focus on stat.TH, math.ST, stat.ML, cs.LG categories
Prefer papers from last 5 years

For each hit:
1. Check if it has a PUBLISHED version (journal or conference)
   - Look for DOI, "published in [venue]" in abstract/comments
   - If published: record the venue and cite the published version
   - If preprint only: flag as T3, record citation count
2. Extract the specific theorem/lemma that supports our repair
3. Assign venue tier (T1/T2/T3)

Return: title, authors, year, arxiv ID, published venue (if any), tier, 
        citation count, the exact theorem statement

Agent 2: Semantic Scholar (venue-filtered)

Use WebFetch on Semantic Scholar API:
https://api.semanticscholar.org/graph/v1/paper/search?query=[encoded-query]&limit=20&fields=title,authors,year,abstract,externalIds,citationCount,venue,publicationTypes

Apply filters:
- First pass: venue matches T1 list → take all
- Second pass: venue matches T2 list → take if citationCount > 10
- Third pass: remaining → take only if citationCount > 50

Return: title, authors, year, venue, tier, citation count, DOI, relevant theorem

Agent 3: Targeted High-Quality Source Search

WebSearch for: [query] site:projecteuclid.org OR site:jstor.org OR site:springer.com OR site:jmlr.org

These sites host T1/T2 journals directly:
- projecteuclid.org → AoS, Annals of Prob, Bernoulli, EJS
- jstor.org → Econometrica, JASA, JRSS-B, Biometrika, AoS
- jmlr.org → JMLR
- springer.com → Math Programming, Prob Theory & Related Fields

Also search: [query] + "textbook" OR "monograph" for authoritative book references

Return: title, authors, year, venue/publisher, tier, the standard reference for this result

4E: Evaluate & Rank Search Results

For each paper found, build a Credibility-Weighted Evaluation Table:

Paper	Venue	Tier	Citations	Credibility	Theorem	Matches need?	Assumptions OK?	Recommend?
van der Vaart (1998)	Cambridge UP (textbook)	T1	10k+	GOLD	Thm 5.41	Exact	Yes	PRIMARY
Chen & Li (2022)	AoS	T1	35	STRONG	Lemma 3.1	Close variant	Check condition 2	SECONDARY
Zhang (2024)	arXiv only	T3	8	WEAK	Thm 2	Exact but new	Unverified	SUPPLEMENTARY
Anonymous (2023)	ICML workshop	T3	2	WEAK	Prop 1	Partial	Unknown	SKIP

Selection priority: PRIMARY > SECONDARY > SUPPLEMENTARY. Always include at least one T1 reference per repair if possible. If only T3 available, flag explicitly in repair plan as "lower confidence — needs independent verification."

4F: Verify Cited Results (with venue-appropriate rigor)

For each recommended paper, do a verification proportional to its tier:

T1 Gold/Strong references (textbooks + top journals):

1. Fetch the exact theorem statement
2. Verify: do OUR assumptions satisfy THEIR prerequisites?
3. Verify: does THEIR conclusion give us exactly what we need?
4. Check: notation compatibility, constants, finite-sample vs asymptotic
5. Trust level: HIGH — can cite with confidence after prerequisite check

T2 Good references:

1. All T1 checks, PLUS:
2. Verify the theorem is not from a corrigendum or errata
3. Cross-reference with at least one T1 source for the same or similar result

T3 Supplementary references (preprints, workshops):

1. All T1 checks, PLUS:
2. Read the proof of the cited theorem (not just the statement)
3. Verify the proof is complete and does not itself have gaps
4. Check if the result has been independently reproduced or cited by T1/T2 papers
5. Trust level: LOW — must note "preprint, not yet peer-reviewed" in repair plan

This prevents citation misuse — the same error class we check for in /proofcheck.

4F.cache: Write back to cache + update lock manifest (mandatory for new sources)

For every reference that was a cache miss in Step 4A and has now been fetched and verified, write a proposal to the cache inbox at ~/.claude/literature_cache/inbox/<bibkey>.draft.md per cache-verification-states.md. The proposal must include:

• Manifest header with verification_status: unverified_extract
• Source URL, source version, retrieval date, source hash, verbatim quote blocks with locators and text hashes
• Applicability contract on the 8 axes per applicability-axes.md
• Theoretical lineage block (primary_line, role_in_literature) per citation-purpose-protocol.md

The repair itself can proceed using the just-fetched content (the writing skill is allowed to use its own unverified_extract immediately because it just read the source). Downstream skills consuming this evidence will require /lit-cache verify promotion (workflow in lit-cache-verify-protocol.md) before using it at source_checked or higher. The user is notified that an inbox entry awaits verification.

Lock manifest update (per cited-results-lock-protocol.md): append a row to papers/<project>/cited_results.lock.md for the new citation site. The repair's citation purpose is typically load_bearing (for Citation-Fix and Strengthen-Proof repairs that invoke the result as a step), technique_inheritance (for Replace-Technique repairs borrowing a proof device), or standard_tool (when the repair invokes a named tool like Talagrand or Bernstein). Follow the "read before write" + "append, do not edit" discipline: do not overwrite existing rows; if the same paper is already in the manifest under a different purpose or site, add a new row.

4G: Fallback When No High-Quality Reference Found

If no T1/T2 reference supports a repair:

1. Can the result be proved from scratch? → Write it as a new lemma (Step 5B) with proof, and note "self-contained proof, no external reference needed"
2. Is a classic textbook result? → Cite the most authoritative textbook even if not found via search (e.g., Durrett for probability, Billingsley for convergence, Rockafellar for convex analysis, van der Vaart for asymptotics, Tsybakov for nonparametric estimation)
3. Only T3 preprint available? → Cite it but add:

   ⚠ Reference [X] is an arXiv preprint (not peer-reviewed).
   The cited theorem was independently verified during this repair.
   Consider replacing with a published reference when available.
   

4. No reference at all? → Write the complete proof yourself (Step 5B) and mark the repair as "self-proved — review recommended"

---

Step 5: Assemble Repair Plan

For each issue, select the best candidate and write a detailed repair specification.

Create per-unit repair files: audit/07_repairs/section_X/{ID}_repair.md

## Repair: I-01 — Lemma C.3 invertibility assumption

### Selected Strategy: Candidate B (Insert supporting lemma)

### Reason for Selection
- Candidate A adds assumption to main theorem (undesirable)
- Candidate B proves invertibility from existing assumptions (minimal impact)
- Candidate C is too invasive (rewrites 6 equations)

### Mathematical Fix

**New Lemma C.3' (to insert before Lemma C.3)**:

Under Assumption 2 (strong convexity with parameter μ > 0),
the Hessian H(θ) satisfies λ_min(H(θ)) ≥ μ for all θ ∈ Θ.

Proof sketch:
By strong convexity, ∇²f(θ) ≽ μI for all θ.
Since H(θ) = E[∇²f(θ)], and expectation preserves PSD ordering,
H(θ) ≽ μI, so λ_min(H(θ)) ≥ μ > 0.  □

### Literature Support

| # | Reference | Venue/Tier | Credibility | What it provides | BibTeX key |
|---|-----------|-----------|-------------|------------------|------------|
| 1 | Boyd & Vandenberghe (2004), Convex Optimization, §9.1.2 | Cambridge UP (T1 textbook) | GOLD | Strong convexity ⟹ H ≻ 0 | boyd2004convex |
| 2 | Nesterov (2018), Lectures on Convex Optimization, Thm 2.1.10 | Springer (T1 textbook) | GOLD | λ_min bound from strong convexity | nesterov2018lectures |

### LaTeX Patch

**Reference mode**: A (single-file) — using `\ref{}` cross-references
Location: paper.tex, after line [XXX] (end of Lemma C.2 proof)

```latex
\begin{lemma}[Hessian invertibility]\label{lem:hessian-invert}
Under Assumption~\ref{assump:strong-convex}, for all $\theta \in \Theta$,
$\lambda_{\min}(H(\theta)) \geq \mu > 0$.
\end{lemma}
\begin{proof}
By strong convexity (Assumption~\ref{assump:strong-convex}),
$\nabla^2 f(x;\theta) \succeq \mu I$ for all $x$ and $\theta \in \Theta$.
Taking expectations preserves the Loewner order, so
$H(\theta) = \mathbb{E}[\nabla^2 f(X;\theta)] \succeq \mu I$.
\end{proof}

If reference mode were B (two-file) the same patch would instead use hard-coded numbers for any cross-file reference:

% In supplement.tex — inserting Lemma S.3 (next supplement number)
\begin{lemma}[Hessian invertibility]\label{lem:hessian-invert}
% Cross-file: Assumption 2 of the main text — DO NOT use \ref{}
Under Assumption~2 of the main text, for all $\theta \in \Theta$,
$\lambda_{\min}(H(\theta)) \geq \mu > 0$.
\end{lemma}
% Within supplement, normal \ref{} is fine:
% ... use Lemma~\ref{lem:hessian-invert} later in the supplement

When the main text needs to cite this new supplement lemma, it must write "Lemma S.3 of the supplement" with a hard-coded S.3, NOT \ref{lem:hessian-invert}.

Rule of thumb (apply automatically when writing patches):

• Patch lives in the SAME file as everything it references → use \ref{} / \eqref{}
• Patch references something in the OTHER file (main↔supplement) → hard-coded number
• When inserting new lemmas in supplement (Mode B), assign them S-prefixed labels AND record the assigned number, so subsequent main-text patches can hard-code it

Repair Provability Status

PROVABLE AS STATED — invertibility follows from strong convexity (Assumption 2)

Proof Strategy for New Content

Direct (strong convexity → PSD Hessian → positive minimum eigenvalue)

Downstream Verification Checklist

• Lemma C.3: replace "H(θ) is invertible" with "by Lemma C.3'"
• Lemma C.5: no change needed (inherits through C.3)
• Theorem 2.1: no new assumptions (invertibility now proved)
• Corollary 2.2: no change needed

Open Risks

• [Any remaining fragile points after this repair]

---

## Step 5B: Write Complete Repaired Proofs (via /proof-writer methodology)

For each repair that involves new proof content (Insert-Lemma, Strengthen-Proof,
Replace-Technique), write a COMPLETE proof — not just a sketch.

Apply /proof-writer's rigor standards:

1. **Claim normalization**: Restate the repaired claim with all quantifiers, domains, types explicit
2. **Dependency map**: List every fact the new proof depends on
3. **Numbered steps**: Every step justified, no "clearly/obviously/standard arguments"
4. **Edge cases**: Handle or explicitly exclude degenerate cases
5. **Final verification**: Theorem statement matches exactly what was proved

Write each complete proof into the repair file under a new section:

```markdown
### Complete Repaired Proof

**Repaired Claim** (normalized):
[Exact statement with all quantifiers and assumptions]

**Proof Strategy**: [chosen strategy from Step 3]

**Dependency Map**:
1. This proof uses: [list]
2. Assumption A2 provides: [what]
3. New reference [Smith 2023, Thm 3.2] provides: [what]

**Proof**:
Step 1. [justified step]
Step 2. [justified step]
...
Therefore [conclusion]. ∎

**Verification Checklist**:
- [ ] Statement matches what was proved (not stronger)
- [ ] Every assumption used is listed
- [ ] Every nontrivial implication justified (no "clearly")
- [ ] Every inequality direction correct
- [ ] Every cited result applicable under stated assumptions
- [ ] Edge cases handled or excluded
- [ ] No hidden dependence on unproved lemma

If the complete proof cannot be written honestly, downgrade the repair status:

• If proof works but under extra conditions → status: PROVABLE AFTER WEAKENING
• If proof hits a wall → status: NOT CURRENTLY JUSTIFIED + blockage report

This is the key quality gate: a repair is only "complete" when the full proof is written and verified, not when the strategy is sketched.

Step 5C: Codex Adversarial Stress-Test of Repairs (if Codex MCP available)

For every P0 and P1 repair with a complete proof, run the per-repair fresh-thread stress-test defined in CODEX_PROTOCOL.md under "Per-Repair Fresh Thread" and "Per-Repair Stress-Test Call Template".

Rules (full rationale and template in CODEX_PROTOCOL.md):

• One fresh mcp__codex__codex thread per logically-independent repair; up to 2-3 repairs may share a thread only if they sit on the same dependency edge or assumption block.
• model_reasoning_effort: xhigh is forced (the scope hits the Reasoning Effort Ladder triggers: theorem / lemma / proof step / rate / quantifier).
• Anti-anchor opening prompt; forced falsification attempt; structured PASS / FIXABLE / FAIL verdict.
• FIXABLE / FAIL iterate via mcp__codex__codex-reply on the same thread (Case B continuation).
• Verdicts are recorded in audit/07_repairs/codex_stress_test.md per the artifact schema in CODEX_PROTOCOL.md "Per-Repair Stress-Test Verdict Recording" (one row per repair, threadId tracked).

The full per-repair call template, the verdict recording schema, the rationale (Codex's honest anchoring self-assessment), and the iterative push-back protocol all live in CODEX_PROTOCOL.md. This skill does not duplicate them inline.

---

Step 6: Cross-Repair Consistency Check

After all individual repairs are designed, verify they work together:

6A: Assumption Consistency Matrix

Build a matrix: rows = all assumptions (original + newly added), columns = all proof units. Check: no unit requires contradictory assumptions.

| Assumption | Scope | Added by repair? | Used by | Conflicts with |
|------------|-------|-----------------|---------|----------------|
| A1: i.i.d. | Global | No (original) | B.1-B.5 | None |
| A2: strong convexity | Global | No (original) | C.3', C.3-C.5 | None |
| A_new1: bounded 4th moment | Local to D.2 | Yes (I-03 repair) | D.2, D.4 | Check: does A1 + A2 imply this? |

6B: Rate/Constant Propagation Check

If any repair changes a rate or constant:

1. Trace through the entire dependency chain to the main theorem
2. Verify the main theorem's rate is preserved (or document the change)
3. Check that no "O(·) hides forbidden dependency" is introduced

6C: New Reference Compatibility & Quality Gate

Check that newly cited papers are:

• Compatible with each other (don't assume contradictory conditions)
• Compatible with the paper's existing framework
• From reputable venues — apply venue tier rules:

Quality gate: If ANY repair relies SOLELY on T3/T4 references:

1. Flag it in REPAIR_PLAN.md with ⚠ warning
2. Provide the self-contained proof (Step 5B) as backup
3. Recommend the author search for a published reference before submission

Cross-check: For each new reference, verify:

• The venue is real and indexed (check DBLP, MathSciNet, or Web of Science)
• The paper is not retracted or has a published erratum affecting the cited theorem
• If citing a preprint, check if a published version now exists (common for arXiv papers)
• If the paper's own references already cite a T1 source for the same fact, prefer that one

---

Step 7: Write Master Repair Plan + Bibliography

7A: REPAIR_PLAN.md

Write papers/<paper-name>/REPAIR_PLAN.md:

# Repair Plan: [Paper Title]

Generated from /proofcheck audit on [date].

## Executive Summary
- Total issues found: N
- Repairable issues: M
- Repairs requiring new literature: K
- New references needed: R
- Main theorem status after repair: [Preserved / Weakened to ...]
- Convergence status: [NOT YET RE-AUDITED / CONVERGED / NOT CONVERGED]

## Repair Priority Order

Execute repairs in this order (respects dependency DAG):

### Phase 1: Foundation Repairs (do first)
| Issue | Unit | Repair Class | Strategy | New refs needed |
|-------|------|-------------|----------|-----------------|

### Phase 2: Critical Path Repairs
| ... |

### Phase 3: Support Repairs
| ... |

## Repair Ladder Summary

Insert the `## Repair Ladder Summary` table per the schema in `stat-shared-references/proof-closure-machinery.md`. One row per issue with columns: Issue ID, Unit, Chosen repair class, Chosen ladder level, Claim preserved?, Assumptions preserved?, Escalation justified?, Pointer to per-issue defense.

## Per-Issue Repair Specifications

Link to each `audit/07_repairs/section_X/*_repair.md` file. Each repair file contains a `Repair Ladder Defense` block per the schema in `proof-closure-machinery.md`.

## Repair Closure Matrix

Insert the `## Repair Closure Matrix` table per the schema in `proof-closure-machinery.md`. Every issue from `06_reports/issue_log.md` must have a row (closure-matrix completeness rule).

## Weaken-Claim Change Log

Insert the `## Weaken-Claim Change Log` block per the schema in `proof-closure-machinery.md`. **MANDATORY** if any repair is class `Weaken-Claim`. A row is required even when there is exactly one Weaken-Claim repair.

## Assumption-Extension Change Log

The per-issue repair file (not the master REPAIR_PLAN.md) holds the canonical Assumption-Extension Change Log block per the schema in `proof-closure-machinery.md`. **MANDATORY** if any repair is class `Add-Assumption` (ladder L4). The master plan's Repair Ladder Summary row points to the per-issue file's Change Log entry.

## New References Summary

| # | Key | Full citation | Venue | Tier | Credibility | Supports repair of | Verified? | Cache reference |
|---|-----|--------------|-------|------|-------------|-------------------|-----------|----------------|

Each row's `Cache reference` resolves to a `paper:<bibkey>#<result_id>` entry per `literature-cache-protocol.md`. The lock manifest at `papers/<project>/cited_results.lock.md` records the citation purpose and verification level used at decision time.

## Reference Quality Summary

- T1 (Gold Standard) references: X / Y total
- T2 (Strong) references: _
- T3 (Supplementary / preprint): _ ← flag each with ⚠ if used
- Self-proved lemmas (no external ref): _

## Consistency Verification

- [ ] Assumption matrix: no contradictions
- [ ] Rate propagation: main theorem rate preserved (or, if not, documented in Weaken-Claim Change Log)
- [ ] New references: mutually compatible
- [ ] New references: all T1/T2 venue verified (no predatory journals)
- [ ] T3 preprint references: cited theorems independently verified
- [ ] Downstream units: all re-verified after repair (via post-repair audit)
- [ ] Repair Closure Matrix is complete (every original issue has a row)
- [ ] Weaken-Claim Change Log is complete (every Weaken-Claim repair has a row + propagation patches)
- [ ] Assumption-Extension Change Log is complete (every Add-Assumption repair has a row in its per-issue file)
- [ ] Every per-issue repair file has a Repair Ladder Defense block (L4/L5 include Phase A Exhaustion Record + Phase B Justification + Semantic-Edit Log Pointer)

## Residual Issues (cannot repair without major rework)

| Issue | Why unrepairable | Impact |

## Hard-Gate Completion Rule

The full Hard-Gate Completion Rule (9 conditions) lives in `stat-shared-references/proof-closure-machinery.md`. Headline conditions:

- Every issue has a terminal closure row; every Weaken-Claim and Add-Assumption repair has its mandatory Change Log entry; outstanding sketches = 0; every P0/P1 repair passed the per-repair Codex stress-test (per `CODEX_PROTOCOL.md`); the Consistency Verification checklist is fully checked.
- **If the original audit contained any S0 or S1 issue**: `/proofcheck --post-repair` has been invoked AND `audit/08_post_repair/CONVERGENCE_VERDICT.md` reports `CONVERGED`. HARD GATE.
- **If the original audit contained only S2 and S3 issues**: `--post-repair` is strongly recommended; the executive summary states `Convergence status: NOT YET RE-AUDITED (S2/S3-only)`.

### 7B: Generate BibTeX Entries

Write new references to `papers/<paper-name>/repair_references.bib`:

```bibtex
% References added to support proof repairs
% Generated by /proof-repair on [date]

@book{boyd2004convex,
  title={Convex Optimization},
  author={Boyd, Stephen and Vandenberghe, Lieven},
  year={2004},
  publisher={Cambridge University Press}
}

7C: Generate LaTeX Patch Summary

Write papers/<paper-name>/PATCHES.md with all LaTeX modifications in order. Each patch declares its reference mode and conformance:

# LaTeX Patches — Apply in Order

## Reference Mode
- Mode: [A: single-file / B: two-file main+supplement]
- Files involved:
  - paper.tex (main text)
  - supplement.tex (if Mode B)
- Supplement numbering scheme (if Mode B): S.1, S.2, S.3, ... or S1, S2, S3, ...

## Patch 1: Insert Lemma S.3 (Hessian invertibility)
- File: supplement.tex   ← which file
- After line: [XXX]
- New label assigned: `\label{lem:hessian-invert}` (only valid within supplement.tex)
- New display number: **S.3** (record this for any future main-text patch citing it)
- Cross-file references inside this patch:
  - "Assumption 2 of the main text" — hard-coded (cross-file)
- Within-file references inside this patch:
  - `\ref{assump:strong-convex-supp}` — OK if assumption is also in supplement
- Insert:
  ```latex
  [the latex block, mode-correct]

Patch 2: Update Theorem 2.1 in main text to invoke new Lemma S.3

• File: paper.tex ← main text
• Line: [YYY]
• Change: "since H(θ) is invertible (Lemma~\ref{...})" → "since H(θ) is invertible (Lemma~S.3 of the supplement)"
• NOTE: hard-coded "S.3" because this is a cross-file reference

Patch 3: Fix Theorem 3.1 rate

• File: paper.tex
• Line: [ZZZ]
• Change: O(n^{-1}) → O(n^{-1} \log n)

Patch 4: Add new bibliography entries

• File: references.bib (shared between main.tex and supplement.tex)
• Append: [entries from repair_references.bib]
• Note: .bib is shared, so BibTeX \cite{key} works in BOTH files normally

### Pre-patch validation rules

Before finalizing PATCHES.md, the agent must verify:

1. **Every `\ref{}` in a patch resolves within the SAME file**
   - Scan each patch's LaTeX block for `\ref{LABEL}` / `\eqref{LABEL}` / `\cref{LABEL}`
   - For each, check whether the `\label{LABEL}` exists in the patch's target file
   - If not → ERROR: convert to hard-coded reference

2. **Every cross-file reference uses hard-coded numbers**
   - Scan for phrases like "Lemma X.Y", "Theorem N", "equation (M)" in cross-file contexts
   - Verify the number is hard-coded, not a `\ref{}`

3. **Supplement-file lemma numbering is consistent**
   - If Mode B: new lemmas in supplement get S-prefixed display numbers
   - Track assigned numbers across patches so the master plan is internally consistent

4. **Citation `\cite{}` works in both files**
   - BibTeX `\cite{}` is fine cross-file because .bib is shared
   - Only mathematical-object `\ref{}` is mode-sensitive

---

## Quick Mode

If user only wants to repair a SINGLE unit (not full audit):

/proof-repair papers/my-paper/ --unit "Lemma C.3"

1. Read just that unit's check file from `04_local_checks/`
2. Read dependency graph for context
3. Generate repair candidates
4. Search literature
5. Output single repair file

## From-Reaudit Mode (`--from-reaudit`)

Invoked as `/proof-repair --from-reaudit papers/<paper-name>/`. This is a focused mode that handles residual issues found by `/proofcheck --post-repair` after a previous repair cycle. It is **manually triggered only**; the pipeline does not auto-loop.

### Pre-conditions

- `audit/08_post_repair/CONVERGENCE_VERDICT.md` exists and reports `NOT CONVERGED — RE-REPAIR REQUIRED` (not `HUMAN INTERVENTION REQUIRED` — that one requires the user to first decide whether to revert, restate, or change venue before any re-repair makes sense).
- The user has read `audit/08_post_repair/RE-AUDIT_REPORT.md` and confirmed the residual issues are within scope for another mechanical repair pass.

### Inputs

1. `audit/08_post_repair/RE-AUDIT_REPORT.md` — the delta-audit report
2. `audit/08_post_repair/new_issues.md` — NEW-S0/S1 issues introduced by previous patches
3. `audit/08_post_repair/per_issue_closure.md` — STILL-OPEN issues from the original audit
4. `audit/08_post_repair/diff_ledger.md` — unjustified diff rows
5. The previous REPAIR_PLAN.md, PATCHES.md, and patched paper

### What this mode does

This mode runs a narrowed version of the main `/proof-repair` workflow on the residual issue set only.

#### Step F1: Collect residuals

Build a focused issue list combining:

- Every `STILL-OPEN` issue from `per_issue_closure.md` (original issues the previous patch did not close)
- Every `NEW-S0` and `NEW-S1` issue from `new_issues.md` (issues the previous patch introduced)
- Every unjustified diff row from `diff_ledger.md` (silent semantic changes not propagated)

S2 and S3 residuals are listed but do not force the cycle to continue; the user decides whether to address them now or accept the open list.

#### Step F2: Classify residuals by cause

Each residual is one of:

- `INCOMPLETE-FIX`: the patch attempted the right strategy but missed steps or edge cases. Re-apply the same repair class with the missed details addressed.
- `WRONG-CLASSIFICATION`: the original repair class was wrong (e.g., Strengthen-Proof was tried where Add-Assumption was needed). Reclassify and re-design.
- `UNDOCUMENTED-WEAKENING`: a Weaken-Claim repair was applied without a PATCHES.md change-log row, or without propagation to downstream units. Generate the missing change-log table and propagate.
- `PROPAGATION-GAP`: a repair was correctly designed and locally verified, but downstream units that consumed the original claim were not updated. Add downstream-propagation patches without touching the already-correct local repair.
- `NEW-DEFECT`: the previous patch introduced a fresh defect in a unit that was previously verified. Treat as a new repair from scratch.

#### Step F3: Repair the residuals only

For each residual, run Steps 3-5 of the main workflow (Generate Candidates, Literature Search, Write Complete Proof) on the residual itself. **Do not re-litigate already-CLOSED-VERIFIED issues.** The previous REPAIR_PLAN.md remains the canonical record for those.

If a residual repair touches a unit already repaired in the previous cycle, the new patch is layered on top — the closure matrix gains a second row for the same unit, marked as `Repair cycle 2`. The previous cycle's row is preserved with its terminal status.

#### Step F4: Update REPAIR_PLAN.md and PATCHES.md

The existing REPAIR_PLAN.md is **appended to**, not rewritten:

- New section: `## Repair Cycle 2 — From Re-Audit Verdict on [date]`
- New Closure Matrix rows for the residual issues
- Updated cycle-2 patches in PATCHES.md, clearly labeled `Cycle 2 — Patch N`
- Updated Codex Stress-Test results for cycle-2 repairs

The summary section is updated to reflect both cycles.

#### Step F5: Re-invoke `/proofcheck --post-repair`

`--from-reaudit` does not declare convergence itself. After it finishes, the user invokes `/proofcheck --post-repair` again. This is the only path to a `CONVERGED` verdict.

### Hard rule against auto-looping

The pipeline never automatically loops `proof-repair --from-reaudit → proofcheck --post-repair → proof-repair --from-reaudit → ...`. Each invocation requires the user to confirm:

- Are the residual issues mechanically fixable, or do they signal a deeper problem (wrong theorem, wrong assumption set, wrong technique entirely)?
- Has the cycle count exceeded 2? If so, the user should consider whether the paper's framework needs to be revisited via `/theory-design` or `/theory-sharpen` rather than continuing to patch.

If a residual cannot be closed after two `--from-reaudit` cycles, escalate: the affected theorem is downgraded to NOT CURRENTLY JUSTIFIED in the patched paper, the abstract and introduction are updated to remove the claim, and the user decides whether the paper still has a publishable contribution without it.

### Common failure modes

- **Cascading rate degradation**: a Weaken-Claim repair in Lemma 5 cascades to corollaries 6, 7, 8, each requiring its own propagation patch. By cycle 2, the paper's headline rate may no longer be defensible. Flag this in `RE-AUDIT_REPORT.md` and let the user decide whether to weaken the headline rate or revert to the original (stronger but unproven) statement.
- **Assumption infection**: an Add-Assumption repair adds a moment condition to Lemma 3; cycle-2 reveals this condition contradicts a sparsity assumption used in Theorem 1. The repair set is inconsistent. Escalate to human intervention rather than producing another cycle.
- **Sketch-expansion loops**: a SKETCH-ONLY unit expanded in cycle 1 reveals new sketches in its expansion (because the cited technique itself was a sketch in the cited paper). Treat as `BLOCKAGE` and stop expanding; do not chain sketch-expansion across cycles.

---

## Output Summary

When complete, report to user:

Repair plan generated for [Paper].

Issues addressed: X / Y total ├── P0 (critical): A repaired, B residual ├── P1 (important): C repaired └── P2 (minor): D repaired

New literature found: N papers ├── T1 Gold (AoS/JASA/Biometrika/JRSS-B/Econometrica/NeurIPS/ICML/JMLR/textbooks): K ├── T2 Strong (EJS/Bernoulli/AAAI/KDD/IEEE-IT): M ├── T3 Supplementary (arXiv preprints): J ← ⚠ if any └── Self-proved (no external ref): L

Files created: ├── REPAIR_PLAN.md — master repair roadmap ├── PATCHES.md — ordered LaTeX modifications ├── repair_references.bib — new BibTeX entries └── audit/07_repairs/ — per-unit repair specifications

Next steps:

1. Review REPAIR_PLAN.md — accept/reject each repair, verify the Repair Closure Matrix and Weaken-Claim Change Log are complete
2. For complex repairs, run: /proof-writer [specific repaired claim] to get publication-ready proof text
3. Apply patches: /proof-repair --apply to auto-patch paper.tex
4. Convergence test (REQUIRED if any S0/S1 issue existed): /proofcheck --post-repair papers/my-paper/ → produces audit/08_post_repair/CONVERGENCE_VERDICT.md → REPAIR_PLAN.md cannot be marked complete until verdict is CONVERGED
5. If re-audit reports NOT CONVERGED — RE-REPAIR REQUIRED: /proof-repair --from-reaudit papers/my-paper/ then re-run step 4. Max 2 cycles; after that, downgrade affected theorems to NOT CURRENTLY JUSTIFIED.