dechenzhang/valg-ml-theory-agent/proof-review-structural

Proof Review Structural

Use this internal diagnostic reviewer after /proof-assembly in the upgraded split workflow.

Contract

Required inputs:

• perspective_M/idea_N/setting.md
• perspective_M/idea_N/latex_template/1_intro.tex
• perspective_M/idea_N/latex_template/2_preliminary.tex
• perspective_M/idea_N/latex_template/3_main.tex
• perspective_M/idea_N/latex_template/4_proof_sketch.tex
• perspective_M/idea_N/latex_template/5_appendix.tex
• perspective_M/idea_N/latex_template/main.tex
• perspective_M/idea_N/latex_template/arxiv.sty
• perspective_M/idea_N/latex_template/ims.bst
• perspective_M/idea_N/latex_template/reference.bib
• perspective_M/idea_N/assembly_report.md
• accepted perspective_M/idea_N/proof_sketch.md
• accepted perspective_M/idea_N/proof_sketch_review.md
• valid diagnostic perspective_M/idea_N/global_proof.md paired with accepted perspective_M/idea_N/global_proof_review.md
• accepted perspective_M/idea_N/global_proof_review.md
• accepted proof_steps/<Step ID>/proof.md and proof_steps/<Step ID>/review.md artifacts for every required sketch step

Output:

• perspective_M/idea_N/proof_review_structural.md

Required machine-readable fields:

• Reviewer Verdict
• Blocking Issues
• Nonblocking Concerns
• Suggested Repair Depth
• Smallest Candidate Repair Target

Do not modify proofs, sketches, step artifacts, trackers, worker logs, proof_review.md, or accepted results.

Responsibilities

• Audit final claim alignment against authoritative setting.md.
• Check theorem/subgoal architecture, dependency closure, sketch-step coverage, and accepted-step traceability.
• Verify assembly did not introduce independent unreviewed lemmas or alter accepted step statements.
• Check the LaTeX bundle for structural consistency and paper-ready self-containment.
• Emit diagnostic fields only; do not assign score, failure type, retry mode, or controller routing.
• Treat assembly_report.md as diagnostic assembly-status context only, not as proof evidence or authority to accept a final claim.
• Treat global_proof.md and global_proof_review.md as diagnostic context only, not as proof evidence or authority to accept a final claim.

Workflow

Step 1: Load Structural Inputs

• Load all content and support files under latex_template/, assembly_report.md, accepted proof_sketch.md, accepted proof_sketch_review.md, valid diagnostic global_proof.md, accepted global_proof_review.md, and accepted step proof/review artifacts for every required sketch step.
• Treat these artifacts as review targets; do not silently repair missing blocks, stale dependencies, changed statements, or synchronization defects.
• Use assembly_report.md only to identify the reported attempted claim, assembly status, and blockers. Do not use it as proof evidence or authority to accept a final claim.
• Use global_proof.md only to identify expected whole-proof structure, known hard steps, and diagnostic gaps after confirming global_proof_review.md is accepted. Do not use either global artifact as proof evidence, a cited result, an assumption source, or authority to accept a final claim.

Step 2: Check Claim Integrity

• Compare the attempted claim in the LaTeX bundle against authoritative setting.md.
• Determine goal mode:
• exact-goal mode: setting.md states the exact theorem claim.
• target-spec mode: setting.md gives a theorem-ready target specification whose exact final bound, constants, or dependence were not fixed.
• In exact-goal mode, verify that the attempted claim matches the formalized goal.
• In target-spec mode, verify that the attempted claim is a concrete valid instantiation of the target quantity, claim type, active scope, success criterion, and required dependence.
• Reject structural acceptance if the attempted claim silently strengthens assumptions, narrows the regime, changes quantifier order, changes the theorem target, or leaves required dependence as placeholder text such as "up to constants" or "up to polynomial factors".

Step 3: Check Proof Architecture

• Verify that the LaTeX bundle contains the required theorem-level structure: target theorem, named intermediate blocks, and assembly of the target theorem.
• Each named theorem-level block must have an exact statement and a clear source: accepted step artifact, direct assembly-only reasoning, or explicit blocker.
• Identify orphan theorem-level blocks: blocks not mapped to a sketch step, not used by final assembly, and not justified as direct assembly-only reasoning.
• Identify missing major transitions: places where the accepted steps do not structurally bridge to the target theorem or attempted claim.
• If the proof uses induction, recursive closure, stability-radius maintenance, basin maintenance, or invariant propagation, verify that the recurring hypothesis is represented by a named hypothesis or invariant block in the final structure.

Step 4: Check Sketch-Step Coverage

• Map every required sketch Step ID to its accepted step proof/review artifacts and to the theorem-level block or assembly use in the LaTeX bundle.
• Every required sketch step must be used, or explicitly declared unnecessary with a reason that does not change the accepted sketch.
• Every final theorem-level block sourced from a step must preserve the accepted step claim, assumptions, dependency meaning, and conclusion.
• A final block must not merge multiple accepted steps in a way that hides which accepted step claim supports which part of the theorem.

Step 5: Check Dependency Closure

• Confirm that every dependency listed by an accepted step is also accepted and available.
• Confirm that final theorem-level blocks do not use unavailable, stale, rejected, or downstream-dependent step claims.
• Check for cyclic or impossible dependency flow in the final proof architecture, including implicit cycles introduced during assembly.
• If a final block uses a step claim, verify that the accepted dependencies of that step are either cited through the step artifact or explicitly accounted for in the assembly.

Step 6: Check Assembly Discipline

• Assembly-only reasoning may only reconcile notation, combine accepted step claims, check direct dependency closure, or prove direct implications from accepted claims.
• Mark as blocking any independent unreviewed lemma, new inequality, convergence-mode upgrade, assumption discharge, changed accepted step statement, changed step assumption, or stronger theorem-level claim introduced by assembly.
• If the final proof needs a new proof obligation not covered by accepted steps, diagnose the smallest structural repair target rather than accepting the assembly.

Step 7: Reconcile Global Diagnostics

• Compare accepted-step coverage and final assembly against the hard steps, gaps, and coverage notes in valid global_proof.md.
• A hard step flagged by global_proof.md must be discharged by an accepted step artifact, explicitly handled by direct assembly-only reasoning, or remain visible as a blocker.
• If global_proof.md exposed a sketch-level gap that the final proof appears to bypass without sketch revision or accepted step proof, mark this as structural blocking.

Step 8: Check LaTeX Bundle Synchronization