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

Global Proof

Use this internal skill after /proof-sketch-review accepts a sketch 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

Optional inputs:

• perspective_M/idea_N/proof_tracker.md
• triggering perspective_M/idea_N/global_proof_review.md when rerunning after REVISE_GLOBAL
• prior same-branch sketch, global-proof-review, step, assembly, or final review failures when the controller provides them as diagnostic history

Output:

• perspective_M/idea_N/global_proof.md

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

Responsibilities

• Draft a detailed theorem-level proof implied by the accepted sketch.
• Make the draft review-ready for a later global-proof reviewer by exposing claim identity, theorem-level blocks, dependency flow, assumption provenance, cited-tool obligations, quantitative-dependence obligations, and unresolved links.
• Check that the sketch steps cohere globally and plausibly compose to the formalized goal.
• Attempt theorem-critical derivations deeply enough to expose whether generated conditions, recurrences, invariants, stability, boundedness, membership, convergence, quantitative specializations, structural lower/sign/coercivity/nondegeneracy/support claims, scope upgrades, or theorem-closure blocks have a concrete closure mechanism and mechanism source under the declared theorem scope.
• Trace theorem-facing generated outputs from their producer step, theorem-level block, primitive source, accepted-derived source, cited tool with a valid diagnostic discharge path under the Source-To-Claim Adequacy Gate, direct derivation, standard fact or tool, current-notation wrapper, primitive-source derivation with checked source-convention compatibility and raw-assumption feasibility, or explicitly conditional target to every consumer block, closure block, specialization, and final theorem use.
• Expose missing links, hard steps, and likely step-local bottlenecks before step workers run.
• Expose candidate idea-level obstructions for /global-proof-review only when the global diagnostic identifies the required theorem-contract change: changed primitive assumptions, changed algorithm/model/procedure, changed theorem scope/mode/metric, changed exposed dependence, changed success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Route sketch-level or roadmap-level blockers back to /proof-sketch.

global_proof.md is diagnostic guidance. It is not proof evidence, not a cited result, not an assumption source, and not a substitute for accepted step proofs.

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.md, and ask the controller to rerun or hand off the correct upstream artifact or stage.
3. Read every sketch step, dependency, assumption, intended proof tool, output target, rate objective, and blocker.
4. If rerunning after global_proof_review.md returned REVISE_GLOBAL, read its blocking issues and required repair bundle. Repair only diagnostic-artifact defects under the same accepted sketch; do not change sketch steps, dependencies, assumptions, output targets, generated-output flows, generated-condition interfaces, accumulation behavior, closure mechanisms, mechanism witnesses, mechanism sources, boundary exclusions, theorem scope/mode/metric, exposed dependence, success criterion, or conclusion inside /global-proof.
5. 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.

1. Apply the shared Assumption Provenance Contract and Generated Output Flow Gate from ../_shared/checklists/artifact-contracts.md. Check whether the accepted sketch proves every theorem-facing generated-object, event, local-validity, recurrence, boundedness, membership, structural condition, or invariant fact needed by an unconditional target from primitive conditions and accepted dependencies. Check whether every theorem-facing generated output consumed by the attempted theorem has a legal producer, consumers, final theorem use, and dependency path.
2. Apply the shared Explicit Rate Contract from ../_shared/checklists/artifact-contracts.md whenever the setting, goal, sketch, or review exposes quantitative dependence. Apply the shared Baseline Invariance Obligation whenever those artifacts expose a recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion.
3. Apply the shared Theorem-Critical Mechanism Witness Gate and Residual-To-Target Adequacy Gate from ../_shared/checklists/artifact-contracts.md. For every theorem-critical generated condition, recurrence, invariant, stability, boundedness, membership, convergence, quantitative specialization, structural lower/sign/coercivity/nondegeneracy/support claim, scope upgrade, or theorem-closure block, name a derivation path from primitive conditions, accepted dependencies, cited tools, direct derivations, standard facts or tools, current-notation wrappers, primitive-source derivations, or explicitly conditional targets to the target condition or control, including the claim class and theorem role, closure mechanism, mechanism source, source-to-claim match, source-convention compatibility when a source supplies the mechanism, residual-to-target adequacy when a bridge transfers a produced, baseline, transformed, or surrogate object or control into the consumed target, key positive/control term or structural source, opposing defect terms, closure/dominance/absorption relation, accumulation behavior under the declared scope when repeated, iterated, recursive, limiting, or otherwise accumulated, boundary regimes handled or excluded, and producer-consumer provenance when generated outputs are consumed; otherwise record the missing witness or bridge as a blocker.
4. Apply the shared Exported Interface Feasibility Gate and Residual-To-Target Adequacy Gate from ../_shared/checklists/artifact-contracts.md. For every theorem-critical downstream-facing output target, generated condition, margin, threshold, simplified bound, basin or membership certificate, recurrence interface, cited-tool wrapper conclusion, direct derivation output, standard fact or tool output, current-notation wrapper output, primitive-source derivation output, or public bridge, expose the raw controls, exported interface, defect terms, controlled and uncontrolled defect classes, residual-to-target adequacy when a bridge transfers a produced, baseline, transformed, or surrogate object or control into the consumed target, dominance or transfer relation, margin or threshold source, source-convention compatibility when a source supplies the output, object-target compatibility when an entry, reference, population, no-error, or baseline object is consumed, branch or boundary handling when applicable, and consumers. If a direct derivation, standard fact or tool, current-notation wrapper, or primitive-source derivation supplies the output, also expose the exact setting convention, source-convention compatibility, object-target compatibility when applicable, and raw-assumption-to-output path. If this path or residual-to-target adequacy is missing under the accepted sketch, classify it as sketch/interface defect or candidate idea/theorem-contract defect.
5. Classify every theorem-critical hard obligation as step-local, sketch/interface defect, or idea/theorem-contract defect under the shared Step-Locality And Theorem-Contract Gate.
6. Write a detailed theorem-level proof draft that follows the sketch dependency order and explicitly marks unresolved links.
7. Build a theorem-level block map and a coverage map from each Step ID to the portion of the whole-proof draft it supports.
8. Build the required ## Scope And Closure Certificate for every theorem-critical generated condition, recurrence, invariant, stability, boundedness, membership, convergence, quantitative specialization, structural lower/sign/coercivity/nondegeneracy/support claim, scope upgrade, or theorem-closure block covered by the Theorem-Critical Mechanism Witness Gate, including the concrete recurrence/potential or mechanism-specific control relation at diagnostic granularity for every all-time or accumulated certificate row, mechanism source / boundary exclusion, obligation locality classification, noncircular closure status, and entry-state / first-update stress entries when applicable.
9. Build ## Generated Output Flow for theorem-facing generated outputs consumed by blocks, closure, specialization, or final theorem use.
10. Audit dependency closure, generated-output flow, assumption provenance, cited-tool applicability, quantitative dependence, exported-interface feasibility, scope-accumulation compatibility, early obstruction patterns, and same-setting repair plausibility.
11. Diagnose the smallest required repair level using the status rules below.
12. Write global_proof.md using ../_shared/templates/global-proof.md.

Global Draft Rules