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

Global Proof Review

Use this internal skill after /global-proof writes global_proof.md and before any /proof-step runs.

Contract

Required inputs:

• perspective_M/idea_N/setting.md
• accepted perspective_M/idea_N/proof_sketch.md
• accepted perspective_M/idea_N/proof_sketch_review.md
• perspective_M/idea_N/global_proof.md

Optional inputs:

• perspective_M/idea_N/proof_tracker.md
• prior same-branch review or final-review failures when the controller provides them as diagnostic history

Output:

• perspective_M/idea_N/global_proof_review.md

Do not modify global_proof.md, sketches, step artifacts, final proofs, trackers, worker logs, or accepted results. Do not write or overwrite latex_template/.

Responsibilities

• Review global_proof.md as an early theorem-level diagnostic gate.
• Check that the diagnostic is detailed enough for downstream step work and later final reviews.
• Check fidelity to setting.md, the accepted proof_sketch.md, and the accepted proof_sketch_review.md.
• Localize material issues to the smallest valid retry target: /global-proof, /proof-sketch, or /subagent-idea-generator.
• Re-audit theorem viability independently; accepted proof_sketch_review.md is an input gate, not authority that the idea or sketch is actually viable after global_proof.md exposes more structure.
• Run a harsh early idea-failure screen so theorem-level obstructions are not deferred to step workers as open-ended hard steps.
• Require a scope-and-closure review before acceptance so shallow "hard local step" labels cannot hide missing theorem-level closure mechanisms or mechanism sources.
• Require a generated-output flow review before acceptance so theorem-facing generated outputs are not exported by closure, specialization, assembly, or later-proof labels without a legal producer-consumer path.
• Independently apply the Theorem-Critical Mechanism Witness Gate before acceptance, even when proof_sketch_review.md accepted.
• Apply the Noncircular Closure Gate before acceptance whenever the diagnostic uses all-time, uniform, limsup, invariant, stability, recurrence, support, basin, boundedness, or generated-condition claims.
• Apply the Entry-State / Activation Trace Gate before acceptance whenever the diagnostic uses recursive, iterative, descent, contraction, convergence, all-time, recurrence closure, invariant, basin/support, mode-conversion, or exact/noiseless specialization claims.
• Apply the Step-Locality And Theorem-Contract Gate before acceptance, even when the diagnostic labels an obligation as a hard local step.
• Apply the Baseline Invariance Obligation before acceptance whenever the setting, goal, accepted sketch, triggering review, or prior same-perspective branch contains a theorem-facing recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion.
• Apply the Residual-To-Target Adequacy Gate before acceptance whenever a theorem-critical bridge transfers a produced, baseline, transformed, or surrogate object or control into a consumed target, margin, threshold, basin, recurrence interface, generated-condition interface, structural claim, quantitative specialization, or public bridge.
• Apply the Gate Evidence Row Contract before acceptance. Fill ## Gate Evidence Table row by row for every theorem-critical generated condition, recurrence, invariant, stability, boundedness, membership, convergence, structural lower/sign/coercivity/nondegeneracy/support claim, quantitative specialization, baseline invariance obligation, scope upgrade, theorem-closure block, generated-output flow, exported-interface feasibility obligation, residual-to-target adequacy obligation, or hard obligation that affects acceptance.
• Preserve the diagnostic boundary: global_proof.md is not proof evidence, not a cited result, not an assumption source, and not authority to change accepted sketch-step claims.

Workflow

1. Read the exact setting and goal from setting.md.
2. Verify proof_sketch_review.md accepts the current proof_sketch.md. If not, stop as an input contract failure, do not write or overwrite global_proof_review.md, and ask the controller to rerun or hand off the correct upstream artifact or stage. If it is accepted, treat that only as permission to review the global diagnostic; do not inherit its viability judgment blindly.
3. Read global_proof.md and validate its required sections, controlled status, suggested routing, diagnostic boundary note, theorem-level block map, sketch-step coverage, dependency and assumption audit, citation and tool audit, quantitative dependence audit, scope and closure certificate, generated-output flow, early obstruction and repair-plausibility audit, and gap notes.
4. Check whether the global proof diagnostic is faithful to the accepted sketch and setting. It may expose gaps, but it must not silently repair claims, change dependencies, alter assumptions, drop quantitative obligations, or change the proof roadmap.
5. Audit theorem-level composition: every accepted sketch step must have a coherent global role or explicit blocker, every theorem-level block needed by the attempted claim must be mapped, and every unresolved obligation must be localized.
6. Audit assumption provenance, generated-output flow, cited-tool applicability, quantitative dependence, theorem-critical mechanism witnesses, scope-compatible closure, mechanism-source support, hard-step localization, and same-setting repair plausibility using the rules below.
7. Run the early idea-failure screen. Do not perform substantial step proofs; use only obstruction-level checks, limiting or boundary stress, recurrence/interface plausibility, provenance checks, and same-setting repair plausibility.
8. Decide the smallest valid status and retry target using the status rules.
9. Write global_proof_review.md using ../_shared/templates/global-proof-review.md.

Status Rules

Global-Proof Review Status must be exactly one of:

• ACCEPTED
• REVISE_GLOBAL
• REVISE_SKETCH
• IDEA_FAIL

Status meanings: