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

Proof Step Review

Use this internal reviewer skill for one submitted step proof.

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
• perspective_M/idea_N/proof_steps/<Step ID>/proof.md
• accepted dependency step proof/review artifacts for the target step, when dependencies exist

Output:

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

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

Responsibilities

• Treat the setting, sketch row, dependencies, and submitted proof as binding.
• Review local proof units one by one.
• Detect hidden independent subclaims not listed in the local lemma map.
• Emit exactly one status: ACCEPTED, REVISE_STEP, REVISE_SKETCH, or BLOCKED_BY_DEPENDENCY.
• Name the smallest retry target without executing reruns or consuming budgets.

Workflow

Step 1: Load The Review Target

• 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 cited 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.
• Read the submitted step proof sections: target step claim, step proof status, allowed assumptions and dependencies, local lemma map, cited result applications, local derivation, target-step assembly, blockers, and notation notes.
• If the target step lists dependencies, read the accepted dependency step proof/review artifacts and identify the exact dependency claims available for this step; otherwise record that the step has no dependency artifacts.
• Treat these artifacts as review targets; do not silently repair missing local units, citations, notation, dependencies, or assembly links.

Step 2: Audit Target Fidelity And Allowed Inputs

• Verify that the submitted proof targets the exact sketch-row claim, not a stronger, weaker, or drifted claim.
• Check that allowed assumptions come only from setting.md, the target sketch row, accepted dependencies, earlier local units, or cited results whose assumptions are checked locally. Setting technical assumptions must keep their stable assump:<slug> ids.
• Apply the shared Assumption Provenance Contract from ../_shared/checklists/artifact-contracts.md. Check that every allowed condition is classified as a primitive setting condition, a derived invariant supplied by an accepted dependency, or a local conditional hypothesis.
• Reject any generated-object, event, local-validity, stability, boundedness, recurrence, or invariant fact treated as a primitive assumption when it is not in setting.md or an accepted dependency conclusion.
• Reject hidden assumption strengthening, narrowed regimes, invalid quantifier-order changes, or unsupported explicit-dependence placeholders.
• For rate-bearing steps, apply the shared Explicit Rate Contract from ../_shared/checklists/artifact-contracts.md. Reject missing declarations of exposed variables, hidden-constant dependence, fixed quantities, probability mode, horizon mode, norm mode, admissibility conditions, or auxiliary tolerances.
• If the proof can only work after changing the sketch-row claim, assumptions, dependency list, intended tool, or output target, route to REVISE_SKETCH.
• Route to REVISE_SKETCH when the attempted proof reveals that the accepted sketch-row interface needs a new bridge step, changed output target, changed dependency, new threshold or positive-margin source, changed cited-tool wrapper conclusion, changed direct-derivation interface, changed standard-fact/tool interface, changed current-notation wrapper interface, changed primitive-source interface, separated defect classes, or changed dominance/transfer relation. Do not spend repeated REVISE_STEP attempts on a missing raw-control-to-exported-interface path.
• Route to REVISE_SKETCH when the attempted proof reveals that a theorem-critical generated event, structural wrapper, margin, threshold, recurrence source, or public bridge assigned to a direct derivation, standard tool, current-notation proof, or primitive-source derivation is not actually supported by the accepted raw assumptions, convention, branch coverage, or quantitative dominance relation. Treat this as a sketch/interface defect unless the review can identify a dependency proof flaw or purely local derivation error under the unchanged sketch row.
• If the nearest flaw is in an accepted dependency proof that can be repaired without changing its sketch row, route to BLOCKED_BY_DEPENDENCY and name that dependency as the smallest retry target.

Step 3: Audit Local Unit Structure

• Every independent nontrivial subclaim must appear in ## Local Lemma Map with a stable local unit ID and a matching subsection in ## Local Derivation.
• Every non-atomic local unit must also have a paper-ready theorem-style title and stable reference label. Treat local unit IDs such as unit_001 as audit handles only; they are not acceptable mathematical proof references.
• 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 state its assumption basis, local conditions, and exact conclusion in the statement itself, in the markdown/LaTeX-ready form "Under Assumption~\ref{assump:...} and [named dependencies or prior theorem-style results], if [specific conditions], then [conclusion]." Setting assumptions used in public-facing prose must use the stable assump:<slug> ids from setting.md and be cited by Assumption~\ref{assump:...} or Assumptions~\ref{assump:...}. Reject statements whose assumptions, regimes, parameter restrictions, or conclusions are only recoverable from surrounding prose, unit IDs, subsection titles, or the proof body.
• Each local unit proof must immediately follow its exact statement and must justify the stated contribution to the target step.
• If the proof uses induction, recursive closure, stability-radius maintenance, basin maintenance, or invariant propagation, the recurring hypothesis must appear as a named hypothesis or invariant unit.
• If the proof claims Atomic step = yes, verify that no hidden independent subclaim is used.

Step 4: Audit Cited Results And Notation

• For every cited paper result, standard theorem, dependency step, or local proof unit, check that the proof restates the result before use.
• The restatement must include source or name, current-branch notation, instantiated objects, required assumptions, conclusion used, and where each assumption is discharged.
• Reject citations used only by title, theorem number, paper notation, or broad prose.
• Check that all new symbols are defined, lightweight, scoped, consistent with setting.md, and explicitly expressed from original setting notation whenever possible.
• Reject notation drift, symbol reuse with changed meaning, or direct import of cited-paper/dependency notation without translation.
• Reject generated or assumed notation whose provenance is not visible. Every new symbol, alias, event, constant, radius, threshold, rate, margin, admissibility parameter, bounded quantity, or helper object must be setting-defined, inherited from an accepted dependency, translated from a checked cited result, or derived/proved by a named local unit; if it is not expressible from original setting notation or accepted translated objects, the step must prove it before use.
• Check derivation-over-notation discipline. When notation and derivational detail conflict, require fewer helper symbols and more visible derivation. Reject helper notation, bundled constants, or aliases that make boundedness, finiteness, rates, parameter dependence, cited-result assumption discharge, or target implications appear asserted instead of derived.
• Check notation economy and public-surface classification. Every new helper object should be classified as public-facing, appendix-local, or proof-local; one-off aliases should be inlined unless they clarify the proof; and step conclusions should export only the minimal public-facing interface needed downstream.
• Reject notation cascades that make a local lemma, proposition, or target-step conclusion harder to read than the underlying mathematical claim, especially when long helper dictionaries could be kept appendix-local, proof-local, or packaged inside a named local result.
• Check constant provenance. Every new constant, radius, threshold, rate, margin, admissibility parameter, bounded quantity, finite-tube quantity, event, or helper object must be directly defined from original setting quantities, explicitly present as a theorem/admissibility condition in the current step statement, inherited from an accepted dependency claim, translated from a checked cited result, or proved/bounded by a named local unit. Treat unexplained boundedness, finiteness, or "choose constants" claims as local proof flaws.
• Check assumption provenance. Every generated-object, event, local-validity, stability, boundedness, recurrence, or invariant condition must be proved in the step, supplied by an accepted dependency, or used only as a local conditional hypothesis. Treat unproved derived invariants in the target-step interface as local proof flaws or sketch flaws, depending on whether the sketch row must change.
• Check explicit-rate preservation. A rate-bearing proof must preserve dependence in every required structural, data/sampling, algorithmic/horizon, regularity/stability, numerical/stochastic/approximation/modeling-error, auxiliary-tolerance, and confidence/probability category unless a local unit proves the specialization. Treat prose-only term absorption or dropped assumptions as local proof flaws.
• Check baseline reduction when applicable. If the step extends, perturbs, or specializes a prior theorem, dependency result, simpler regime, or limiting regime, verify that the proof preserves the path back to the corresponding baseline result or explicitly justifies any conservative loss. If the baseline is an inherited theorem-facing recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion, verify preservation of the original conclusion; a conservative loss or weaker surrogate is target-changing.

Step 5: Audit Per-Unit Rigor

For each local unit, check:

• statement fidelity to the target step and allowed assumptions
• proof validity line by line
• cited-result applicability and assumption discharge
• algebra, inequalities, probability steps, and interchanges of limits, expectations, suprema, gradients, integrals, or conditionings
• quantifiers, constants, parameter dependence, and uniformity
• stochastic-mode distinctions such as almost-sure, in-probability, in-expectation, in-Lp, and high-probability
• boundary or degenerate cases
• WLOG, symmetry, relabeling, normalization, or rescaling arguments
• phrases such as "clearly", "obviously", "standard", "similarly", and "by routine arguments"

Step 6: Run Local Adversarial Tests

Try to break high-risk local claims, especially: