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

Proof Step

Use this internal skill to prove exactly one Step ID from an accepted proof sketch.

Contract

Required inputs:

• perspective_M/idea_N/setting.md
• perspective_M/idea_N/proof_sketch.md
• accepted perspective_M/idea_N/proof_sketch_review.md
• target Step ID
• accepted dependency step proof/review artifacts listed by the target step, when dependencies exist

Optional inputs:

• accepted diagnostic perspective_M/idea_N/global_proof.md only when paired with accepted perspective_M/idea_N/global_proof_review.md
• accepted perspective_M/idea_N/global_proof_review.md when global_proof.md is provided
• latest same-step proof_steps/<Step ID>/proof.md
• triggering same-step proof_steps/<Step ID>/review.md, downstream proof_steps/<Downstream Step ID>/review.md naming this step as the failed dependency, or final proof_review.md when repairing PROOF_STEP_FLAW

Output:

• perspective_M/idea_N/proof_steps/<Step ID>/proof.md

Do not modify the sketch, dependency artifacts, downstream step artifacts, final proof artifacts, trackers, worker logs, or accepted results.

Reference boundary:

• Do not read prior same-perspective idea_K branches directly.
• Use only the current setting.md, accepted proof_sketch.md, accepted proof_sketch_review.md, accepted dependency artifacts when dependencies exist, latest same-step proof, triggering same-step review, downstream dependency-block review, final review for PROOF_STEP_FLAW, and optionally accepted diagnostic global_proof.md paired with accepted global_proof_review.md as planning guidance.
• Use global_proof.md only for step-relevant proof ideas, gap notes, and hard-step diagnostics. Do not use it as proof evidence, a cited result, an assumption source, or authority to change the target step claim.
• Do not read or use global_proof.md if global_proof_review.md is missing, stale, invalid, or not ACCEPTED.
• If an older-branch technique is needed, it must already be encoded in the current sketch, accepted dependencies, or cited results checked inside the current step proof.
• If global_proof.md suggests a changed step claim, dependency, or assumption, stop and route to /proof-sketch instead of repairing inside /proof-step.

Responsibilities

• Prove only the assigned step claim under the assumptions and dependencies in proof_sketch.md.
• Keep the proof self-contained relative to setting.md, the target step, and accepted dependencies.
• Expose local proof structure so /proof-step-review can audit each local unit.
• Preserve valid local units on repair unless the review identifies them as flawed.

Workflow

Step 1: Load The Assigned Step

• Read the exact formalized setting and goal from setting.md.
• Read the target row from the controller-accepted proof_sketch.md: intended claim, dependencies, assumptions used, technical challenge, intended proof tool or cited result, output target, and row-local review status. Setting assumptions should be named by their stable assump:<slug> ids from setting.md.
• Treat proof_sketch_review.md as the sketch-level acceptance source; do not use the row-local Review status field as the acceptance gate.
• If the target step lists dependencies, read the accepted dependency step proof/review artifacts and identify the exact dependency claims available for use; otherwise record that the step has no dependency artifacts.
• If an accepted diagnostic global_proof.md and accepted global_proof_review.md are provided, read only the parts relevant to the target Step ID; record any useful proof idea as planning context, not as an allowed assumption or established result.
• Treat the sketch row as binding. Do not prove a stronger, weaker, or drifted claim unless the blocker explicitly says the sketch row must change.

Step 2: Set Local Scope

• List only the setting assumptions, sketch-row assumptions, and accepted dependency claims needed for the step. Cite setting assumptions by their stable assump:<slug> ids from setting.md.
• Apply the shared Assumption Provenance Contract from ../_shared/checklists/artifact-contracts.md. Classify each allowed condition as a primitive setting condition, a derived invariant supplied by an accepted dependency, or a local conditional hypothesis. Do not treat generated-object, event, local-validity, stability, boundedness, recurrence, or invariant facts as primitive unless they are explicitly setting assumptions.
• Do not list global_proof.md statements as allowed assumptions or dependencies.
• Introduce lightweight local notation for this step and record it in ## Notation And Assumption Notes.
• Define every new symbol before use, and express it explicitly in original setting.md notation whenever possible.
• Do not import notation from cited papers, dependency proofs, or prior attempts without translating it into the current branch notation.
• Keep notation consistent with setting.md; if a local abbreviation is useful, state its scope and do not reuse an existing symbol with a new meaning.
• Do not generate or assume new notation by convenience. Every new symbol, alias, event, constant, radius, threshold, rate, margin, admissibility parameter, bounded quantity, or helper object must be classified in ## Notation And Assumption Notes as a setting-defined expression, an accepted dependency object, a checked cited-result object translated into current notation, or a locally derived/proved object. If a useful object is not expressible from original setting notation or accepted translated objects, prove its existence or bound as a named local unit before using it.
• Use derivation-over-notation discipline. When notation and derivational detail conflict, prefer fewer helper symbols and more visible derivation. A helper symbol may shorten repeated complex expressions or name a stable conceptual object, but it must not hide the proof of boundedness, finiteness, rates, parameter dependence, cited-result assumption discharge, or target implications.
• Apply notation economy before exporting a step conclusion. Introduce a helper symbol, constant, threshold, envelope, or shorthand only when it is reused or clearly improves proof clarity; inline one-off expressions when they do not obscure the derivation.
• Classify every new helper object in ## Notation And Assumption Notes as public-facing, appendix-local, or proof-local. Export only the minimal public-facing interface needed by downstream steps or the final theorem; keep proof bookkeeping as appendix-local or proof-local.
• If a step needs many helper objects, package them inside a named local result and expose a compact conclusion rather than making the step target or downstream interface a long helper dictionary.
• Track constant provenance in ## Notation And Assumption Notes. Every new constant, radius, threshold, rate, margin, admissibility parameter, bounded quantity, or finite-tube quantity must be classified as directly defined from original setting quantities, explicitly present as a theorem/admissibility condition in the current step statement, inherited from an accepted dependency claim, or proved/bounded by a named local unit. Do not introduce free bounded quantities or "choose finite constants" claims without one of those sources.
• Track assumption provenance in ## Notation And Assumption Notes. Any generated-object, event, local-validity, stability, boundedness, recurrence, or invariant condition used by the step must be marked as proved in this step, supplied by an accepted dependency, or only a local conditional hypothesis. If it is needed for the target step conclusion and is not proved or supplied, set Step Proof Status = PARTIAL_BLOCKED.
• For rate-bearing steps, apply the shared Explicit Rate Contract from ../_shared/checklists/artifact-contracts.md. Record the exposed variables, hidden-constant dependence, fixed quantities, probability mode, horizon mode, norm mode, admissibility conditions, and auxiliary tolerances in ## Notation And Assumption Notes before they are used in derivations.
• When the step extends, perturbs, or specializes a prior theorem, dependency result, simpler regime, or limiting regime, record the baseline-reduction obligation in ## Explicit Rate Audit or ## Notation And Assumption Notes. Prove that the step conclusion reduces to the corresponding baseline result under the relevant specialization, or explicitly state and justify any conservative loss. If the baseline is an inherited theorem-facing recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion, preserve that original conclusion; a conservative loss or weaker surrogate is target-changing.

Step 3: Plan Local Proof Units

• Split every independent nontrivial subclaim into a local unit with a stable ID such as unit_001.
• Use local unit types lemma, proposition, claim, hypothesis, or invariant.
• Give every non-atomic local unit a paper-ready theorem-style title and a stable ASCII reference label, such as lem:step-003-unit-001 or prop:step-006-tube. The local unit ID is an audit handle only; mathematical prose must cite the paper-ready result, not the ID.
• Each local unit statement must be self-contained relative to setting.md, accepted dependencies, earlier local units, and restated cited results.
• Each local unit statement must explicitly record its assumption basis, any local conditions, and exact conclusion in the statement itself. Use the markdown/LaTeX-ready analogue of "Under Assumption~\ref{assump:...} and [named dependencies or prior theorem-style results], if [specific conditions], then [conclusion]" rather than relying on nearby prose or the proof body to supply assumptions. If a setting assumption is used, cite the same stable id from setting.md, which assembly will translate into the numbered assumption label.
• If the step uses induction, recursive closure, stability-radius maintenance, basin maintenance, or invariant propagation, expose the recurring hypothesis as a named hypothesis or invariant unit.
• If the step is genuinely atomic, write Atomic step = yes in ## Local Lemma Map and justify why no hidden independent subclaim is being used.

Step 4: Restate And Check Cited Results

• Before using any cited paper result, standard theorem, dependency step, or local proof unit, restate it in ## Cited Result Applications.
• For each cited result, record the source or name, restated statement in current notation, instantiated objects, required assumptions, conclusion used, and where each assumption is discharged.
• Do not cite a result only by title, theorem number, or paper notation.
• If an intended cited result cannot be restated with checked assumptions, treat that citation use as unresolved.

Step 5: Write Local Derivation And Assembly