Imported from DechenZhang/VALG-ML-Theory-Agent (skills/proof-sketch-review/SKILL.md). Install upstream with npx skills add DechenZhang/VALG-ML-Theory-Agent --skill proof-sketch-review. Copyright stays with the author.

Proof Sketch Review

Use this internal reviewer skill after /proof-sketch and before any /proof-step runs.

Contract

Required inputs:

• perspective_M/idea_N/setting.md
• perspective_M/idea_N/proof_sketch.md

Optional inputs:

• perspective_M/idea_N/idea.md
• perspective_M/idea_N/proof_tracker.md
• perspective_M/idea_N/technical_survey.md
• prior same-perspective artifacts needed to check lineage, prior failures, or source plausibility

Output:

• perspective_M/idea_N/proof_sketch_review.md

Do not write sketch files, step proofs, step reviews, final proofs, trackers, worker logs, or accepted results.

Responsibilities

• Treat setting.md and proof_sketch.md as binding.
• Decide whether the sketch is ready for step-level proof work.
• Emit exactly one status: ACCEPTED, REVISE_SKETCH, or IDEA_FAIL.
• Assign Sketch Viability Score as an integer from 1 to 10.
• Name the smallest retry target.
• Record a retry mode that distinguishes sketch repair from idea revision.
• Diagnose theorem-level obstructions before global-proof and step proof work.
• Record every material repair obligation in a required repair bundle without executing loops or consuming retry budgets.

Workflow

Step 1: Load The Review Target

• Read the exact formalized setting and goal from setting.md.
• Read the sketch identity, proof roadmap, sketch steps, dependency notes, and blockers from proof_sketch.md.
• If setting.md records source-alignment, progress-type, or materiality metadata, apply the Source-Direction Fidelity Contract from ../_shared/checklists/artifact-contracts.md as an alignment check for the sketch.
• Treat the sketch as a review target; do not silently repair missing claims, dependencies, assumptions, or citations.
• 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 or constants were not fixed.

Step 2: Check Goal Alignment

• In exact-goal mode, verify that the proof roadmap and step targets plausibly prove the formalized goal exactly.
• In target-spec mode, verify that the proof roadmap targets a concrete valid instantiation of the target quantity, claim type, active scope, and success criterion.
• When source-direction metadata is present, verify that the sketch's concrete target is consistent with the recorded progress type and materiality. Do not reject a rigorous partial, conditional, obstruction, or diagnostic target merely because it is not full, but reject a sketch that presents it as solving the full source target or omits the remaining source-relevant gap.
• Compare quantifiers, domains, parameter qualifiers, asymptotic scope, uniformity, constants, and normalization.
• Reject sketches that silently strengthen assumptions, narrow the regime, change the target, or hide placeholder dependence when explicit dependence is required.
• When the goal or sketch exposes an explicit rate, apply the shared Explicit Rate Contract from ../_shared/checklists/artifact-contracts.md. Reject sketches that lack a rate objective declaring exposed variables, hidden-constant dependence, fixed quantities, required mode fields, and required admissibility conditions.
• Apply the shared Assumption Provenance Contract from ../_shared/checklists/artifact-contracts.md. Reject sketches for unconditional targets when generated-object, event, local-validity, stability, boundedness, recurrence, or invariant facts are placed directly into theorem-facing assumptions instead of being assigned to bridge steps or explicit blockers.
• Apply the shared Scope-Accumulation Compatibility Gate from ../_shared/checklists/artifact-contracts.md. Reject sketches when theorem-critical generated conditions, recurrences, invariants, stability, boundedness, membership, convergence, or quantitative specializations must persist, compose, vanish, or stay controlled across a repeated, iterated, recursive, limiting, or otherwise accumulated scope but the sketch does not identify defect behavior, accumulation mode, closure mechanism, mechanism source, accumulated defect or forcing term, sign status, controlling budget/potential or mechanism-specific control relation, one-step charge/absorption/potential-drop, preservation, projection, coupling, stopping, or conditioning relation, and why that relation has a finite budget or is valid under the declared scope.
• Apply the shared Generated Output Flow Gate from ../_shared/checklists/artifact-contracts.md. Reject sketches when a theorem-facing generated output is consumed by a downstream step, closure, specialization, or final theorem without a legal producer, consumer list, final-use mapping, and dependency path.
• Apply the shared Theorem-Critical Mechanism Witness Gate from ../_shared/checklists/artifact-contracts.md before ACCEPTED. Reject acceptance for any theorem-critical high-risk step or block whose witness omits the claim class and theorem role, mechanism source, source-to-claim match, key positive/control term or structural source, opposing defect terms, closure/dominance/absorption relation, boundary/null-regime handling, or required producer-consumer provenance.
• Apply the shared Entry-State / Activation Trace Gate from ../_shared/checklists/artifact-contracts.md before ACCEPTED whenever the sketch uses a recursive algorithm, dynamical process, iterative construction, or generated trajectory to prove descent, contraction, convergence, all-time control, invariant maintenance, basin/support preservation, recurrence closure, mode conversion, or exact/noiseless zero-radius behavior. Reject acceptance when the sketch does not trace an allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state at obstruction-level granularity, or when the trace shows the mechanism inactive while the theorem-facing conclusion remains false.
• Apply the shared Baseline Invariance Obligation from ../_shared/checklists/artifact-contracts.md before ACCEPTED whenever the setting, goal, 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. Reject acceptance when the sketch omits that conclusion, replaces it with a conservative or conditional surrogate, shows only that defect terms vanish, or lacks a source-adequate bridge and entry-state trace when applicable.
• Apply the shared Step-Locality And Theorem-Contract Gate from ../_shared/checklists/artifact-contracts.md before ACCEPTED. Classify every theorem-critical hard obligation as step-local, sketch/interface defect, or idea/theorem-contract defect. Reject acceptance when a sketch only names a later step for a property whose mechanism source is not already identified in primitive assumptions, accepted derived outputs, cited tools with a valid discharge path under the Source-To-Claim Adequacy Gate, explicitly conditional targets, or direct derivations, standard facts or tools, current-notation wrappers, or primitive-source derivations with checked source-convention compatibility and raw-assumption feasibility.
• Apply the shared Exported Interface Feasibility Gate and Residual-To-Target Adequacy Gate from ../_shared/checklists/artifact-contracts.md before ACCEPTED. Reject acceptance when a 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 lacks source-convention compatibility when a source supplies the output, lacks a sketch-level path from raw available controls to the exported interface, or lacks residual-to-target adequacy when a produced, baseline, transformed, or surrogate object or control is bridged into the consumed target. The sketch must identify the raw controls, exported claim, controlled and uncontrolled defect classes, dominance or transfer relation, residual terms and their sources when applicable, margin or threshold source, required target scale, source-convention compatibility when applicable, and consumers; a threshold controlling one defect class cannot discharge fixed, empirical, event-level, persistent, irreducible, or wrong-scale residual defects without a separate source.
• Apply the shared Gate Evidence Row Contract from ../_shared/checklists/artifact-contracts.md before ACCEPTED. 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. Reject acceptance when any applicable row is missing, shallow, category-only, circular, source-inadequate, lacks source-convention compatibility when a source supplies the mechanism or output, lacks residual-to-target adequacy when applicable, scope-incompatible, missing generated-output producer-consumer flow, missing entry or boundary stress when applicable, or classified as anything other than step-local.

Step 3: Check Sketch Structure And Coverage

• Every step must have a stable ID, exact intended claim, dependencies, assumptions used, proof tool or challenge, output target, and review status. Setting assumptions must be cited by their stable assump:<slug> ids from setting.md.
• The dependency graph must be acyclic; each dependency must point only to an earlier step.
• Every essential roadmap item must be represented by a step or an explicit blocker.
• High-risk obligations must be localized into lemma-sized steps or explicit blockers, not broad prose.
• Rate-bearing obligations must be localized into lemma-sized steps or explicit blockers, including all exposed structural, data/sampling, process/scope, regularity/stability, numerical/stochastic/approximation/modeling-error, auxiliary-tolerance, and confidence/probability dependencies.
• If the public theorem is expected to simplify a technical quantitative result, the sketch must include a quantitative-specialization bridge step or output target covering auxiliary choices, technical condition verification, term comparison or simplification inequalities, probability conversion, and the final simplified statement.
• If the final theorem or any downstream step needs a derived invariant, the sketch must include a bridge step or output target proving it from primitive setting conditions and accepted dependencies before unconditional use. Conditional local lemmas may assume such facts, but the sketch must not present them as primitive theorem assumptions unless the formalized goal is explicitly conditional.
• If the final theorem or any downstream step needs a theorem-critical generated condition, recurrence, invariant, stability, boundedness, membership, convergence, or quantitative specialization, the sketch must name the intended closure mechanism and mechanism source at sketch-level granularity rather than only assigning "closure" to a future step. The mechanism may be a planned proof interface, not a completed proof, but it must identify the type of closure expected under the declared theorem scope, the primitive condition, accepted derived control, cited tool with a valid 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 theorem target expected to make it nonvacuous, the concrete recurrence/potential or mechanism-specific control relation when the claim is all-time or accumulated, and the boundary regimes handled or excluded.
• Apply a Noncircular Closure Gate to all-time, uniform, limsup, invariant, stability, recurrence, support, basin, boundedness, and generated-condition claims. The sketch must identify a noncircular producer or mechanism source whose availability does not already assume the target closure claim, generated condition, or final theorem consequence, plus the exit/defect/control relation and dependency path to each consumer. A closure, admissibility, local-validity, boundedness, stability, support, basin, or invariant set may be used as a proof device only when the sketch names the independent source and exit/defect control that prove membership or maintenance under the declared scope.
• If a step or block is central to final theorem closure, recurrence, invariant maintenance, structural lower/sign/coercivity/nondegeneracy/support claims, scope upgrades, or quantitative specialization, the sketch must include a mechanism-witness entry. The entry may be obstruction-level rather than a full derivation, but it must expose the theorem role, mechanism source, key control and defect terms, closure or dominance relation, boundary/null-regime handling, and producer-consumer provenance when generated outputs are consumed.
• If such a condition or specialization is required across a repeated, iterated, recursive, limiting, or otherwise accumulated scope, the sketch must also state the accumulation behavior of defect, forcing, leakage, or residual terms. A barrier, reserve, ledger, invariant, stability, bootstrap, Lyapunov, first-exit, finite-budget, small-gain, projection, dissipative recurrence, algebraic coupling, or later-proof label is too shallow unless it names the accumulated defect, says whether its sign is controlled or adversarial/unknown, and states why those terms are locally absorbed, contractive, telescoping, summable, signed-cancelled, monotone-potential controlled, finite-budgeted under the declared scope, source-excluded, stopped/conditioned, or explicitly conditional through a concrete one-step charge/absorption/potential-drop, preservation, projection, coupling, stopping, or conditioning relation.
• If a theorem-facing generated output is consumed by any step, closure, specialization, or final assembly, the sketch must record the producer step or source, consumers, final theorem use, dependency path, and provenance class in ## Generated Output Flow. A late closure, specialization, assembly, or later-proof label does not count as a producer unless it proves the output from accepted inputs.
• Step claims should be small enough that /proof-step can prove and /proof-step-review can audit them locally.

Step 4: Audit Assumptions And Cited Tools

• Step assumptions must come from setting.md, earlier steps, or cited tools with valid discharge paths under the Source-To-Claim Adequacy Gate. Any setting technical assumption used by a step must be named by its stable assump:<slug> id.
• Step assumptions must be classified by provenance. Primitive conditions may come from setting.md; derived invariants must come from earlier step conclusions or be marked as local conditional hypotheses. Treat an unproved derived invariant listed as an assumption as blocking.
• For each cited theorem, lemma, standard fact, framework ingredient, or prior artifact, check that the sketch records enough provenance, instantiated objects, required hypotheses, and intended conclusion for later local proof work. For theorem-critical cited results, require source identity, version or stable locator when relevant, exact label or stable statement identifier when used, statement role, current-object to source-object mapping, source-convention compatibility, hypothesis-by-hypothesis discharge, conclusion-interface match, known non-output boundaries, and any needed bridge or wrapper obligation before treating the result as a step-local source.
• For theorem-critical cited wrappers that export basin, membership, support, contraction, recurrence, structural lower/sign/nondegeneracy, threshold, margin, or public bridge claims, reject ACCEPTED if the sketch assigns the wrapper output to a future step without fixing the current-notation wrapper conclusion, hypothesis discharge path, source-convention compatibility, residual-to-target adequacy when the wrapper bridges into the consumed target, margin/slack/reserve or threshold source, raw controls, controlled and uncontrolled defect classes, and downstream exported interface. Route to REVISE_SKETCH when a same-setting wrapper bridge, interface split, dependency change, convention translation, or target-preserving loss route could repair the gap; use IDEA_FAIL only when repair requires a theorem-contract change.
• For theorem-critical direct derivations, standard facts or tools, current-notation wrappers, or primitive-source derivations that export generated events, basin or membership certificates, contraction or recurrence interfaces, structural lower/sign/support controls, margins, thresholds, simplified rates, or public bridges, require the same obstruction-level source-interface preflight as for cited wrappers. Reject ACCEPTED when the sketch only names a future derivation or standard tool without recording source-convention compatibility, the exact setting convention, raw controls, exported interface, residual-to-target adequacy when applicable, quantitative dominance or transfer relation, controlled and uncontrolled defect classes, branch or boundary handling, and consumers.
• For theorem-critical initialization, entry, basin, contraction, recurrence, structural support/nondegeneracy, or baseline wrappers, require an object-target compatibility preflight before treating the obligation as step-local. The sketch or review must instantiate the exact deterministic, population, no-error, or baseline entry object produced by the current procedure when that specialization is meaningful, compare it with the object consumed by the theorem under the theorem metric, reference operator, basin, or target interface, and state equality or an explicit same-target bridge with residual-to-target adequacy. If the produced object is transformed, weighted, preconditioned, whitened, reference-operator-modified, or otherwise surrogate relative to the consumed target, reject ACCEPTED unless the sketch already states a same-target bridge supported by the setting or accepted dependencies and adequate at the consumed target scale. Reject ACCEPTED when the sketch only proves, assumes, or plans to prove nondegeneracy, gap, boundedness, curvature, concentration, or smallness of the produced object but does not show that this produced object supports the consumed target object.
• Use optional technical_survey.md, prior same-perspective artifacts, and tracker history only to check lineage, prior failures, or source plausibility.
• Treat unresolved citation applicability, unresolved source identity or label, unknown theorem-critical statement shape, hidden assumption strengthening, missing hypothesis discharge, or missing conclusion-interface match as blocking unless the sketch records it as an explicit blocker.

Step 5: Run The Early Obstruction Audit

Try to break the theorem-level viability of the sketch using general checks only. Do not rely on domain-specific labels or examples. Audit:

• Limiting-case stress: test whether the claimed conclusion and its intended mechanism source are still plausible under boundary, degenerate, asymptotic, exact/noiseless, adversarial-sign, null-direction, or baseline regimes allowed by the setting.
• Theorem-critical bridge support: identify every nontrivial bridge from primitive assumptions to theorem-facing conclusions, and check whether the sketch proves it, assigns it to a step, or records it as a blocker.
• Exported-interface feasibility: for each theorem-critical output consumed by a later step, closure, specialization, cited-tool wrapper, direct derivation, standard fact or tool, current-notation wrapper, primitive-source derivation, or final theorem, check whether the sketch gives an obstruction-level source-convention compatibility check when a source supplies the output, a raw-controls-to-exported-interface path, and residual-to-target adequacy when a bridge transfers a produced, baseline, transformed, or surrogate object or control into the consumed target. Reject acceptance when the sketch only says to absorb, charge, threshold, transfer, invoke a wrapper, apply a standard tool, prove a current-notation derivation, or use a primitive-source derivation without identifying source-convention compatibility when applicable, the raw controls, exported interface, residual decomposition when applicable, defect split, dominance or transfer relation, required target scale, and margin or threshold source.
• Cited-wrapper interface feasibility: for each theorem-critical cited-wrapper output consumed downstream, check that the sketch fixes the wrapper conclusion in current notation, the source hypotheses and discharge path, source-convention compatibility, any non-output boundaries, the raw-control-to-wrapper-output path, the margin/slack/reserve or threshold source, controlled and uncontrolled defect classes, and the producer-consumer path. Do not accept a wrapper output as step-local when the sketch only says a future step will instantiate, restate, adapt, or prove the wrapper.
• Source-convention compatibility: for each theorem-critical cited tool, standard fact or tool, current-notation wrapper, direct derivation, or primitive-source derivation, compare the source convention with the branch convention for objects, coordinates or representation, metric or inner product, population or reference operator, data/model assumptions, initialization or entry target, algorithm/procedure, normalization, quantitative dependence, and baseline/no-error specialization when relevant. If the source interface and consumed branch interface are not the same, require an explicit bridge; otherwise classify the obligation as sketch/interface defect or idea/theorem-contract defect, not step-local.
• Object-target compatibility: for each theorem-critical initialization, entry, basin, contraction, recurrence, structural support/nondegeneracy, or baseline mechanism, compare the exact produced object in the relevant deterministic, population, no-error, or baseline specialization with the theorem's consumed target object under the theorem metric, reference operator, basin, or interface. If the produced object is transformed, weighted, preconditioned, whitened, reference-operator-modified, or otherwise surrogate relative to the consumed target, require an explicit same-target bridge with residual-to-target adequacy; source-convention compatibility or properties of the surrogate alone do not suffice. If they differ without an explicit bridge adequate at the consumed target scale, classify the obligation as sketch/interface defect or idea/theorem-contract defect, not step-local; a future proof step may instantiate a fixed bridge but may not be the first place where this compatibility is discovered.
• Scope and dependence consistency: compare the sketch against the formalized quantifiers, regimes, modes, constants, exposed dependencies, hidden-constant dependence, and fixed quantities.
• Generated-condition provenance: verify that facts about generated, realized, recursive, event-conditioned, local-validity, stability, boundedness, or invariant objects are not silently treated as primitive theorem assumptions.
• Generated-output flow: verify that every theorem-facing generated output consumed by a step, closure, specialization, or final theorem has a legal producer, consumer list, final use, dependency path, and provenance class. Reject acceptance when an output has no producer, is consumed before production, is routed through a missing dependency, or is exported by a closure/specialization/assembly label without proof from accepted inputs.
• Theorem-critical mechanism witness: for every step or block central to final theorem closure, recurrence, invariant maintenance, structural lower/sign/coercivity/nondegeneracy/support claims, scope upgrades, or quantitative specialization, verify the sketch gives an obstruction-level witness covering claim class, theorem role, mechanism source, source-to-claim match, key positive/control term or structural source, opposing defect terms, closure/dominance/absorption relation, boundary/null-regime handling, and producer-consumer provenance when relevant. Reject acceptance when the sketch only names future proof work, generic geometry, local validity, smallness, admissibility, boundedness, a barrier, reserve, ledger, bootstrap, or closure category.
• Entry-state trace stress: for every theorem-critical recursive, iterative, descent, contraction, convergence, all-time, recurrence closure, invariant, basin/support, mode-conversion, or exact/noiseless specialization claim, instantiate an allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state relevant to the mechanism and trace the first update, transition, or stationary behavior. Reject acceptance when the update, descent source, closure source, generated condition, or invariant-maintenance source is inactive while the theorem-facing conclusion remains false, or when the review only says a future step, induction, basin argument, or closure will handle the state without showing the source already exists under the current theorem contract.
• Baseline invariance stress: identify every theorem-facing recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion inherited by the current target. Check that the sketch preserves the same conclusion under the relevant specialization or entry case, with a mechanism source already present under the current theorem contract. Reject acceptance when the sketch replaces the original conclusion by a weaker conservative, conditional, stopped, finite-scope, or remainder-only statement unless the current setting or triggering failure explicitly made that target-changing repair.
• Obligation locality classification: apply the Step-Locality And Theorem-Contract Gate to every theorem-critical hard obligation before acceptance. Record whether each obligation is step-local, sketch/interface defect, or idea/theorem-contract defect. A future proof step is not a mechanism source; it is acceptable only when the source is already identified and the step merely instantiates or derives the claim from that source under unchanged theorem contract and interfaces.
• Noncircular closure gate: for all-time, uniform, limsup, invariant, stability, recurrence, support, basin, boundedness, and generated-condition claims, check that the proposed closure does not assume the target property as an admissibility condition, theorem-facing premise, generated-condition hypothesis, local-validity premise, or downstream output before proving it. Reject acceptance when the closure source is the later closure step itself, an unproved generated condition, or a renamed version of the target property.
• Closure-mechanism viability: for any theorem-critical generated condition, recurrence, invariant, stability, boundedness, membership, convergence, or quantitative specialization, check that the sketch names an intended mechanism such as self-contraction, dissipative/restoring recurrence, telescoping, summable control, signed cancellation, monotone potential, reserve/ledger under declared scope, stopping/conditioning argument, projection/nonexpansive maintenance, algebraic coupling, structural lower/upper comparison, or explicitly conditional target. Also check that it names a mechanism source: a primitive condition, accepted derived control, cited tool with a valid 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 theorem target. Do not require a full derivation at sketch-review stage, but reject sketches that only defer closure to later work or name a closure category without a source-adequate mechanism, valid source, source-convention compatibility when required, and concrete control relation. For theorem-critical cited results, adequacy still requires source identity, version or stable locator when relevant, exact label or stable statement identifier when used, statement role, source-object mapping, source-convention compatibility, hypothesis discharge, conclusion-interface match, known non-output boundaries, and any bridge or wrapper accounting.
• Scope-accumulation compatibility: when such a condition or specialization is required across a repeated, iterated, recursive, limiting, or otherwise accumulated scope, check that the sketch classifies defect behavior as locally absorbed, contractive, telescoping, summable, signed-cancelled, monotone-potential controlled, finite-budgeted under the declared scope, source-excluded, stopped/conditioned, explicitly conditional, or unsupported. A classification is valid only if the sketch names the accumulated defect, sign status, controlling budget/potential or mechanism-specific control relation, one-step charge/absorption/potential-drop, preservation, projection, coupling, stopping, or conditioning relation, and finite-budget or declared-scope validity justification. Reject acceptance when the sketch names only a future barrier, reserve, ledger, invariant, stability, bootstrap, Lyapunov, first-exit, small-gain, projection, dissipative recurrence, algebraic coupling, or local proof without explaining accumulation compatibility and source.
• Citation and tool applicability: check whether each cited or standard tool has valid source identity, version or stable locator when relevant, exact label or stable statement identifier when used, statement role, source-object mapping, hypothesis discharge, conclusion-interface match, known non-output boundaries, and any bridge or wrapper obligation for the current setting. For theorem-critical cited results, reject acceptance when the sketch only says the result is plausible, framework-compatible, label-uncertain, statement-shape-uncertain, or to be checked in a future proof step without recording source identity, source hypotheses, their current discharge, and the conclusion interface needed downstream.
• Source-convention baseline stress: when a theorem-critical source is used to preserve a baseline, no-error, no-noise, population, limiting, or exact-specialization conclusion, instantiate that specialization at obstruction-level granularity and check that the source target, branch target, and consumed metric or interface still coincide or have an explicit bridge. If the specialization reveals a convention mismatch, route before proof-step work.
• Same-setting repair plausibility: decide whether every material obstruction can plausibly be repaired within the same idea and formalized setting/goal, or whether repair would require changing primitive assumptions, changing the algorithm/model/procedure, changing theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Target-preserving bridge-repair gate: when the obstruction is a missing bridge between available controls and a theorem-facing conclusion, first test whether the current formalized setting and goal can be preserved by revising the sketch roadmap. Treat repairs as target-preserving when they add or reorganize bridge steps, dependency interfaces, conditional local lemmas, quantitative-specialization steps, or conservative quantitative loss terms already allowed by the current target. If such a repair is plausible, route to REVISE_SKETCH, not IDEA_FAIL. Use IDEA_FAIL only after explaining why all target-preserving sketch repairs would require changing primitive assumptions, changing the algorithm/model/procedure, changing theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion. A repair that weakens, omits, or replaces an inherited baseline invariance obligation is target-changing unless the setting, goal, or triggering failure explicitly authorized the weaker target.
• Interface-splitting check: when one planned step combines defect classes controlled by different sources, verify that the sketch separates the needed bridges or explains a single source that controls all classes. If one parameter, event, margin, or cited result controls only part of the exported claim, route to REVISE_SKETCH unless the remaining terms have their own source under the unchanged setting.
• Residual-to-target adequacy check: when a theorem-critical bridge transfers a produced, baseline, transformed, or surrogate object or control into a consumed target, verify the residual decomposition, theorem metric or norm, source for each residual term, required target margin or scale, and dominance at that scale. If this comparison is absent, only source-side, wrong-scale, or deferred to a proof step, classify the issue as sketch/interface defect or idea/theorem-contract defect, not step-local.

For every sketch, explicitly scan any present high-risk obligation class:

• Structural property claims needed by the theorem or cited tools, such as positivity, nondegeneracy, lower or upper bounds, regularity, conditioning, stability, or comparison properties. When the theorem needs a lower, signed, contractive, coercive, or nondegenerate source, stress-test whether the setting supplies it or explicitly excludes boundary regimes where it vanishes.
• Mechanism-source nonvacuity: when a step is supposed to prove contraction, coercivity, positivity, nondegeneracy, a lower bound, signed descent, support preservation, basin closure, recurrence closure, or exact/zero-limit behavior, test the null-source regime where that mechanism vanishes while the target conclusion would remain false or the theorem-critical obstruction would remain present. If the setting allows that regime and no earlier bridge, primitive condition, cited tool, 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 excludes it, reject the sketch as REVISE_SKETCH or IDEA_FAIL; do not accept it as a merely hard future step.
• Entry-state activation: when a theorem-critical mechanism is supposed to start from an initialized recursion, iterative process, generated trajectory, or boundary case, test whether the first update or stationary behavior activates the source before the theorem-facing claim is consumed. If an allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state makes the mechanism vanish while the target conclusion is false, reject as REVISE_SKETCH when a same-setting bridge, conditional interface, basin split, excluded-boundary clause, or conservative target-preserving loss could repair it, and as IDEA_FAIL when repair requires changing primitive entry or initialization assumptions, changing the algorithm/model/procedure, changing theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Source-to-claim adequacy: check whether each named mechanism source has the right type of content for the claim class. Upper bounds, smallness, finite budgets, local boxes, admissibility inequalities, or generic regularity do not by themselves support positive lower, coercive, signed, support-preservation, or nondegenerate claims. If the sketch treats such a source as adequate without a primitive, earlier-derived, cited, direct derivation, standard fact or tool, current-notation wrapper, primitive-source derivation, or conditional lower/sign/support/conditioning source with the required feasibility checks, reject as REVISE_SKETCH when a same-setting bridge or conditional interface could repair it, and as IDEA_FAIL only when repair requires changing primitive assumptions, changing the algorithm/model/procedure, changing theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Direct/standard/current-notation/primitive-source feasibility: when the sketch assigns a theorem-critical generated event, structural wrapper, margin, threshold, recurrence source, or public bridge to a direct derivation, standard fact or tool, current-notation wrapper, or primitive-source derivation, test whether the exact primitive assumptions imply the exported interface under the stated convention and every allowed branch or regime covered by that interface. Also test source-convention compatibility when the source is inherited or translated from another convention. If the implication or convention bridge is unsupported, classify it as sketch/interface defect or idea/theorem-contract defect, not step-local.
• Approximation, expansion, perturbation, discretization, stochastic-error, or modeling-error controls, including remainder terms and parameter dependence.
• Recursive, inductive, invariant, boundedness, local-validity, membership, or region-maintenance arguments for generated objects.
• Mode upgrades, including local-to-broader-scope, pointwise-to-uniform, conditional-to-unconditional, event-conditioned-to-theorem-facing, finite-scope-to-broader-scope, or convergence/probability-mode conversions.
• Accumulation-sensitive closures, including generated conditions or quantitative controls whose defect, forcing, leakage, residual, or approximation terms are persistent, one-sided, nondecaying, additive, adversarial-sign, or otherwise not obviously compatible with the declared theorem scope.
• Noncircular closure-sensitive claims, including all-time, uniform, limsup, invariant, stability, recurrence, support, basin, boundedness, and generated-condition conclusions whose proof would be circular if the same property is assumed as a condition, admissibility premise, or source.
• Explicit dependence in any domain-appropriate rate category, including structural, data/sampling, process/scope, regularity/stability, numerical/stochastic/approximation/modeling-error, auxiliary-tolerance, and confidence/probability dependence.
• Exported interface feasibility and residual-to-target adequacy for theorem-critical generated outputs, margins, thresholds, simplified bounds, basin or membership certificates, recurrence interfaces, cited-tool wrapper conclusions, direct derivation outputs, standard fact or tool outputs, current-notation wrapper outputs, primitive-source derivation outputs, and public bridges.
• Public specialization or simplification of a technical quantitative result, including auxiliary choices, technical condition verification, term comparison or simplification inequalities, probability conversion, and final hidden-constant dependence.
• Unproved derived or generated-object facts hidden inside admissibility, event, local-validity, stability, boundedness, recurrence, membership, or invariant assumptions.

Promote verified breaks and unresolved theorem-critical obligations into ## Blocking Issues and ## Required Repair Bundle.

Step 6: Diagnose The Sketch Outcome

• Use the deepest blocking issue to choose the status.
• Assign Sketch Viability Score using the full set of material issues, not only the deepest issue.
• Keep score and status aligned:
  • ACCEPTED: score 8, 9, or 10.
  • REVISE_SKETCH: score 5, 6, or 7.
  • IDEA_FAIL: score 1, 2, 3, or 4.
• Use REVISE_SKETCH when the proof roadmap, steps, dependencies, assumptions, blockers, citations, high-risk coverage, generated-output flow, or scope-accumulation interface must change but the idea and formalized setting/goal remain viable.
• Use REVISE_SKETCH when a theorem-critical mechanism witness, noncircular closure source, concrete recurrence/potential or mechanism-specific control relation, or hard-obligation locality classification is missing, shallow, or scope-incompatible but the same setting may still support one through revised bridge steps, dependency interfaces, conditional local lemmas, generated-output flow, generated-condition interfaces, or quantitative-specialization/loss-routing.
• Before selecting IDEA_FAIL, record why REVISE_SKETCH cannot preserve the current formalized setting and goal. A missing proof bridge is not automatically idea-level when the current target can absorb a conservative quantitative loss, conditional local interface, or revised bridge/dependency structure.
• Use IDEA_FAIL only when the target appears false, materially mis-scoped, or salvageable only by changing primitive assumptions, changing the algorithm/model/procedure, changing theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion; for a missing witness, this requires explaining why no same-setting sketch repair can supply it.
• Use ACCEPTED only when the sketch is structurally valid, goal-aligned, preserves every applicable Baseline Invariance Obligation, has concrete, source-adequate, and scope-compatible mechanism witnesses for every step or block covered by the Theorem-Critical Mechanism Witness Gate, classifies every unresolved theorem-critical hard obligation as truly step-local, passes the corresponding null-source, noncircular-closure, Entry-State / Activation Trace, and scope-accumulation stress checks with concrete all-time/accumulated recurrence/potential or mechanism-specific control relations rather than category labels, has legal producer-consumer flow for theorem-facing generated outputs, includes a complete ## Gate Evidence Table satisfying the shared Gate Evidence Row Contract for every theorem-critical obligation affecting acceptance, and is ready to spawn /proof-step subagents.

Step 7: Write The Review

• Use ../_shared/templates/proof-sketch-review.md.
• Copy or summarize the reviewed sketch identity and proof roadmap faithfully.
• ## Sketch Viability Score must contain one integer from 1 to 10.
• ## Audit Summary must cover goal alignment, dependency audit, high-risk coverage, and assumption/citation plausibility.
• ## Early Obstruction Audit must record the outcome of the limiting-case stress, theorem-critical bridge support, scope/dependence consistency, generated-condition provenance, citation/tool applicability, same-setting repair plausibility, and high-risk obligation class checks.
• ## Early Obstruction Audit must record the Theorem-Critical Mechanism Witness Gate result, including whether any missing, shallow, or scope-incompatible witness is same-setting sketch-repairable or requires idea-level change.
• ## Early Obstruction Audit must record the Entry-State / Activation Trace Gate result, including the allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state tested, the first-update or stationary-behavior trace, and the route when a mechanism is inactive while the theorem-facing conclusion remains false.
• ## Early Obstruction Audit must record the Baseline Invariance Obligation result whenever applicable, including the inherited baseline conclusion, the specialization or entry case tested, the mechanism source, whether the original conclusion is preserved, and the route when the sketch only supports a weaker surrogate.
• ## Early Obstruction Audit must record the Step-Locality And Theorem-Contract Gate result, including an obligation locality classification for every theorem-critical hard obligation and the route for every non-step-local obligation.
• ## Early Obstruction Audit must record the Exported Interface Feasibility Gate and Residual-To-Target Adequacy Gate result for every theorem-critical downstream-facing output target, including the raw controls, exported interface, defect split, residual decomposition when applicable, dominance or transfer relation, margin or threshold source, required target scale, and route when the interface is missing or unsupported.
• ## Early Obstruction Audit must record the object-target compatibility result when a theorem-critical wrapper or mechanism depends on an initialized, entry, reference, population, no-error, or baseline object, including the produced object, consumed target object, theorem metric or basin, whether the produced object is transformed, weighted, preconditioned, whitened, reference-operator-modified, or otherwise surrogate relative to the consumed target, bridge if any, residual-to-target adequacy of that bridge when applicable, and route when the comparison fails or is deferred.
• ## Early Obstruction Audit must record the Noncircular Closure Gate result for all-time, uniform, limsup, invariant, stability, recurrence, support, basin, boundedness, and generated-condition claims.
• ## Early Obstruction Audit must record the outcome of the Scope-Accumulation Compatibility Gate whenever repeated, iterated, recursive, limiting, or otherwise accumulated theorem-critical controls appear.
• ## Early Obstruction Audit must record the outcome of the Generated Output Flow Gate whenever theorem-facing generated outputs are consumed.
• ## Gate Evidence Table must satisfy the shared Gate Evidence Row Contract. Include one 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. ACCEPTED is invalid if any applicable row is absent, has empty or unreasoned N/A fields, uses only a category or future-step label, lacks a legal source, concrete control relation, residual-to-target adequacy when applicable, or raw-control-to-exported-interface relation, has circular closure, omits producer-consumer flow, fails an applicable entry or boundary stress check, or gives a locality verdict other than step-local.
• ## Blocking Issues is None only when accepted; otherwise write numbered blockers with location, defect, downstream effect, and smallest repair direction.
• ## Required Repair Bundle is None only when accepted; otherwise list all material repair obligations needed by the next /proof-sketch or /subagent-idea-generator run, including linked issue locations, required change, affected assumptions or step IDs, and the smallest repair target for each item. Include a target-preserving repair check: either state the sketch-level bridge/roadmap repair obligation, or state the concrete reason no sketch-level repair can preserve the current setting and goal.
• ## Review Rationale must explain why the selected status is the deepest required change.
• Keep status, smallest retry target, and retry mode aligned with the status rules below.

Review Checks

• Goal alignment: the sketch must plausibly prove the exact goal or a valid target-spec instantiation without target drift.
• Source/progress alignment: when present in setting.md, the sketch must preserve source alignment, progress type, and materiality, and must state any remaining source gap for partial, conditional, obstruction, or diagnostic branches.
• Viability scoring: the review must assign one integer Sketch Viability Score from 1 to 10 and align it with the selected status.
• Step structure: every step needs a stable ID, exact intended claim, dependencies, assumptions used, proof tool or challenge, output target, and review status; setting assumptions should appear as stable assump:<slug> ids.
• Dependency validity: the graph must be acyclic; steps may depend only on earlier steps.
• Coverage: every essential roadmap item and high-risk obligation must be a step or an explicit blocker.
• Early obstruction audit: the review must apply limiting-case stress, theorem-critical bridge support, scope/dependence consistency, generated-condition provenance, citation/tool applicability, and same-setting repair plausibility before acceptance.
• High-risk obligation scan: when present, the review must stress-test structural property claims, approximation or perturbation controls, recursive or invariant maintenance arguments, mode upgrades, explicit dependence, public quantitative specializations, and hidden generated-condition assumptions.
• Theorem-critical mechanism witness scan: any step or block central to theorem closure, recurrence, invariant maintenance, structural lower/sign/coercivity/nondegeneracy/support claims, scope upgrades, or quantitative specialization must have an obstruction-level witness. Reject acceptance when the witness is missing, shallow, or replaced by a future-step label.
• Entry-state trace scan: theorem-critical recursive, iterative, descent, contraction, convergence, all-time, recurrence closure, invariant, basin/support, mode-conversion, and exact/noiseless specialization claims must trace an allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state through the first update, transition, or stationary behavior when the Entry-State / Activation Trace Gate applies. Reject acceptance when a mechanism is inactive while the target conclusion remains false.
• Obligation locality scan: every theorem-critical hard obligation must be classified as step-local, sketch/interface defect, or idea/theorem-contract defect before acceptance. Reject acceptance when a claimed hard step needs a mechanism source, theorem-facing assumption, generated-condition producer, closure interface, accumulation behavior, mode change, scope change, metric change, exposed dependence change, or weakening the conclusion that is not already supported under the current theorem contract.
• Mechanism-source scan: theorem-critical contraction, coercivity, positivity, nondegeneracy, lower-bound, signed-descent, support, basin, recurrence-closure, and exact/zero-limit claims must have a nonvacuous primitive, earlier-step, cited-tool, direct derivation, standard fact or tool, current-notation wrapper, primitive-source derivation with checked source-convention compatibility and raw-assumption feasibility, or explicitly conditional source. A future step target is not a source by itself.
• Source-to-claim adequacy scan: the source must match the claim type. Reject acceptance when a lower/sign/support/coercivity/nondegeneracy claim is supported only by upper bounds, smallness, finite budgets, local boxes, admissibility inequalities, generic geometry, or future proof work.
• Noncircular closure scan: all-time, uniform, limsup, invariant, stability, recurrence, support, basin, boundedness, and generated-condition claims must have a noncircular producer or mechanism source, exit/defect/control relation, and dependency path to each consumer. Reject acceptance when the sketch assumes the same generated condition, closure, support, basin membership, boundedness, stability, recurrence, or invariant that it must prove.
• Explicit-rate coverage: exposed variables, hidden constants, fixed quantities, required mode fields, admissibility conditions, and bridge obligations must appear in the sketch when an explicit rate is requested or exposed.
• Assumption-provenance coverage: any generated-object, event, local-validity, stability, boundedness, recurrence, or invariant fact required for the target must be proved by a planned bridge step, supplied by an earlier dependency, restricted to a local conditional lemma, or recorded as a blocker.
• Generated-output flow coverage: theorem-facing generated outputs consumed by downstream steps, closure, specialization, or final theorem assembly must have a legal producer, consumers, final use, dependency path, and provenance class, or be recorded as blockers.
• Closure-mechanism coverage: theorem-critical generated conditions, recurrences, invariants, stability, boundedness, membership, convergence, and quantitative specializations must have an intended closure mechanism and mechanism source named at sketch-level granularity, or be recorded as blockers. This is a viability check, not a completed proof obligation.
• Scope-accumulation coverage: repeated, iterated, recursive, limiting, or otherwise accumulated theorem-critical controls must identify defect behavior, accumulation mode, closure mechanism, mechanism source, accumulated defect or forcing term, sign status, concrete budget/potential or mechanism-specific control relation, one-step relation, and finite-budget or declared-scope validity justification, or be recorded as blockers. This is a viability check, not a completed proof obligation.
• Gate evidence coverage: the review must include row-level evidence for every theorem-critical obligation affecting acceptance. Narrative audit prose does not substitute for a required row.
• Exported-interface feasibility coverage: downstream-facing theorem-critical outputs must have a sketch-level raw-control-to-exported-interface path and residual-to-target adequacy when a bridge transfers a produced, baseline, transformed, or surrogate object or control into the consumed target. Missing dominance inequalities, missing positive margins, missing threshold sources, missing cited-tool wrapper, direct-derivation, standard-fact/tool, current-notation-wrapper, primitive-source output interfaces, missing target-scale residual dominance, or unseparated defect classes route to REVISE_SKETCH when a same-setting bridge or split could repair them.
• Baseline invariance coverage: when the target has an inherited baseline/recovery conclusion, acceptance requires a row-level audit showing the original conclusion is preserved under the relevant specialization or entry case. A weaker conservative, conditional, stopped, finite-scope, or remainder-only substitute is not target-preserving.
• Target-preserving bridge-repair gate: missing theorem-critical bridges must be tested for same-setting sketch repair before routing to idea revision. IDEA_FAIL reviews must include a concrete same-setting sketch-repair impossibility rationale.
• Assumption provenance: step assumptions must come from setting.md, earlier steps, or cited tools with valid discharge paths under the Source-To-Claim Adequacy Gate, and setting technical assumptions must be cited by stable ids.
• Citation adequacy: cited tools must be traceable and specific enough for later local proof and review. Theorem-critical cited tools must also pass the Source-To-Claim Adequacy Gate by recording source identity, version or stable locator when relevant, exact label or stable statement identifier when used, statement role, source-object mapping, source-convention compatibility, hypothesis discharge, conclusion-interface match, known non-output boundaries, and any required bridge or wrapper obligation before they can support ACCEPTED.
• Blocker localization: unresolved obstacles must identify whether the smallest repair is sketch repair or idea revision.
• Required repair bundle: non-accepted reviews must list every material repair obligation, not only the first or deepest blocker.

Status Rules

• ACCEPTED: the sketch is goal-aligned, structurally valid, sufficiently covered, preserves every applicable Baseline Invariance Obligation, classifies every unresolved theorem-critical hard obligation as step-local, has plausible, source-adequate, accumulation-compatible, noncircular, entry-state-traced when applicable, and nonvacuous mechanism witnesses for theorem-critical closures and structural descent/support claims, has feasible raw-control-to-exported-interface paths and residual-to-target adequacy when applicable for downstream-facing theorem-critical outputs, includes a complete Gate Evidence Table satisfying the shared Gate Evidence Row Contract, and is ready for step proof. Use Sketch Viability Score = 8-10, Smallest Retry Target = None, and Retry Mode = none.
• REVISE_SKETCH: the proof roadmap, bridge structure, dependency interface, step decomposition, high-risk coverage, theorem-critical mechanism witness, noncircular closure source, or hard-obligation locality interface needs repair while the idea and formalized setting/goal remain viable. Use Sketch Viability Score = 5-7, Smallest Retry Target = /proof-sketch, and Retry Mode = revise_sketch.
• IDEA_FAIL: the target appears false, materially mis-scoped, or salvageable only by changing primitive assumptions, changing the algorithm/model/procedure, changing theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion. Use Sketch Viability Score = 1-4, Smallest Retry Target = /subagent-idea-generator, and Retry Mode = new_idea. The review must explain why same-setting sketch repair is insufficient.

Write proof_sketch_review.md using ../_shared/templates/proof-sketch-review.md.