name: global-proof-review description: Review a branch-local global proof diagnostic after global-proof and before step-level proof work, deciding whether the diagnostic is accepted, needs a global rewrite, requires proof-sketch repair, or exposes an idea-level obstruction. metadata: version: "1.0.0"

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:

• ACCEPTED: global_proof.md is contract-valid, detailed, faithful to the accepted sketch and setting, and safe to consume as diagnostic context. Its own status must be COMPLETE_DRAFT or PARTIAL_BLOCKED with Suggested Routing = None. The scope-and-closure certificate must be present and pass review, including row-level obligation locality classification, exported-interface feasibility and residual-to-target adequacy for downstream-facing theorem-critical outputs, noncircular closure when applicable, entry-state / first-update stress when applicable, baseline invariance when applicable, and scope-accumulation compatibility when theorem-critical controls are repeated, iterated, recursive, limiting, or otherwise accumulated. For all-time or accumulated closure rows, category labels or assignment to future local proof are insufficient: the certificate must expose the accumulated defect, sign status, concrete recurrence/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. The generated-output flow must be present and pass review whenever theorem-facing generated outputs are consumed. The theorem-critical mechanism witness must be explicit, source-adequate, source-convention compatible when a source supplies the mechanism, and scope-compatible for every hard local obligation or theorem-critical block. The review must include a complete ## Gate Evidence Table satisfying the shared Gate Evidence Row Contract for every theorem-critical obligation affecting acceptance, including every present baseline invariance obligation, exported-interface feasibility obligation, and residual-to-target adequacy obligation. Every unresolved theorem-critical hard obligation must be classified as step-local under the Step-Locality And Theorem-Contract Gate. Any theorem-critical cited result used as a mechanism source must pass the Source-To-Claim Adequacy Gate, including 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. Any unresolved obligations must be local proof obligations under unchanged sketch steps, dependencies, assumptions, output targets, generated-output flows, generated-condition interfaces, exported interfaces, residual-to-target adequacy when applicable, accumulation behavior, closure mechanisms, mechanism witnesses, source-adequate and source-convention-compatible mechanism sources, entry-state traces when applicable, inherited baseline conclusions when applicable, and boundary exclusions.
• REVISE_GLOBAL: the accepted sketch still appears viable and already contains the concrete relation, exported-interface feasibility evidence, source-convention compatibility evidence, or cited-tool discharge needed for review, but global_proof.md is missing required detail, has internal inconsistencies, misclassifies a local hard obligation, omits required audit content, has a missing or too-shallow scope-and-closure certificate, omits a generated-output flow already present in the accepted sketch, omits or understates a theorem-critical mechanism witness already present in the accepted sketch, fails to expose the key recurrence/interface, exported interface, accumulation behavior, mechanism source, source-convention compatibility, cited-tool discharge, conclusion-interface match, or concrete budget/potential or mechanism-specific control relation already present in the accepted sketch, or needs a rewrite under the same accepted sketch. Use this only when rerunning /global-proof can repair the issue without changing sketch steps, dependencies, assumptions, output targets, exported interfaces, generated-output flows, generated-condition interfaces, accumulation behavior, closure mechanisms, mechanism witnesses, mechanism sources, source-convention bridges, boundary exclusions, theorem scope/mode/metric, exposed dependence, success criterion, or conclusion.
• REVISE_SKETCH: the proof roadmap, step decomposition, step claim, dependency, assumption, output target, exported interface, generated-output flow, generated-condition bridge, generated-condition interface, accumulation behavior, closure mechanism, theorem-critical mechanism witness, mechanism source, source-convention bridge, boundary exclusion, quantitative bridge, cited-tool plan, or coverage structure must change before step proving can be sound. Also use this when the accepted sketch needs a new bridge step, changed step target, changed dependency, changed generated-output flow, changed generated-condition interface, changed accumulation interface, changed mechanism-witness entry, same-setting bridge, generated-condition interface, closure mechanism, concrete recurrence/potential or mechanism-specific control relation, changed source-convention bridge, changed raw-control-to-exported-interface relation, or conservative quantitative loss routing, or when global_proof.md correctly reports SKETCH_BLOCKED and same-idea sketch repair remains plausible.
• IDEA_FAIL: the target appears false, materially mis-scoped, or salvageable only after identifying 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. A missing mechanism witness is idea-level only when supplying it requires that theorem-contract change. The review must identify the setting or goal component that must change, not merely that the current sketch lacks a bridge.

When multiple statuses appear applicable, choose the deepest sound retry target that is already justified by the artifacts under review. A contract-invalid or shallow global_proof.md gives REVISE_GLOBAL only when the missing diagnostic detail prevents a reliable sketch-level or idea-level classification; it must not mask an independently visible REVISE_SKETCH or IDEA_FAIL obstruction.

Target alignment:

• ACCEPTED -> Smallest Retry Target = None
• REVISE_GLOBAL -> Smallest Retry Target = /global-proof
• REVISE_SKETCH -> Smallest Retry Target = /proof-sketch
• IDEA_FAIL -> Smallest Retry Target = /subagent-idea-generator

Do not add Retry Mode or a numeric score to global_proof_review.md.

Audit Rules

• Contract audit: reject as REVISE_GLOBAL when required sections are missing, the diagnostic is too shallow to review, controlled status or suggested routing is invalid, or the diagnostic boundary note is absent. For a missing or too-shallow scope-and-closure certificate, use REVISE_GLOBAL only when the accepted sketch already contains the concrete relation and the diagnostic omitted or misstated it; otherwise route by the Scope and Closure Review rules to REVISE_SKETCH or IDEA_FAIL.
• Contract-defect tie-breaker: if a contract defect coexists with an independently visible theorem-contract obstruction, record both issues and choose REVISE_SKETCH or IDEA_FAIL when the stronger route is already justified from setting.md, the accepted sketch, and the reviewed global diagnostic.
• Claim and sketch fidelity audit: check that the attempted theorem claim preserves the formalized goal mode, scope, assumptions, quantifier order, and exposed dependence. Reject as REVISE_SKETCH or IDEA_FAIL if fidelity can only be restored by changing the sketch or idea.
• Prior-review independence audit: use accepted proof_sketch_review.md as workflow provenance and prior diagnostic context, but rerun theorem-level viability checks independently. If the global diagnostic exposes an obstruction omitted by the sketch review, choose the status required by the current obstruction.
• Theorem-level structure audit: check that named theorem-level blocks compose toward the attempted theorem, respect the accepted dependency order, and account for every accepted sketch step.
• Dependency and assumption audit: classify theorem-facing conditions as primitive conditions, accepted derived conclusions, local conditional hypotheses, or missing derived-condition bridges. Unconditional targets may not consume missing generated-condition bridges as assumptions.
• Generated-output flow audit: check ## Generated Output Flow for every theorem-facing generated output consumed by the attempted theorem, theorem-level block, closure block, or public specialization. Reject as REVISE_GLOBAL if the accepted sketch already contains a valid producer-consumer flow but the diagnostic omits or misstates it. Reject as REVISE_SKETCH if a generated output has no legal producer, has consumers before producers, lacks a dependency path, is exported by a closure/specialization/assembly label without proof from accepted inputs, or needs a new bridge, output target, dependency, generated-condition interface, or flow allocation. Reject as IDEA_FAIL only when the generated output cannot be supported without changing primitive assumptions, algorithm/model/procedure, theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Exported-interface feasibility audit: apply the shared Exported Interface Feasibility Gate and Residual-To-Target Adequacy Gate to 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. Reject acceptance when the diagnostic treats a missing raw-control-to-exported-interface path or missing residual-to-target adequacy as a hard local step. Independently re-check direct derivations, standard facts or tools, current-notation wrappers, and primitive-source derivations even when proof_sketch_review.md accepted them: the diagnostic must expose source-convention compatibility, the exact setting convention, raw controls, exported interface, residual decomposition when applicable, defect split, dominance or transfer relation, required target scale, margin or threshold source, branch or boundary handling, and consumers. Use REVISE_GLOBAL only when the accepted sketch already contains that valid evidence but the diagnostic omits or misstates it. Use REVISE_SKETCH when the sketch needs a new bridge, changed output target, changed dependency, new margin or threshold source, changed wrapper, direct-derivation, standard-fact/tool, current-notation, or primitive-source conclusion, separated defect classes, changed source-convention bridge, changed residual-to-target bridge, or changed dominance/transfer relation. Use IDEA_FAIL only when support requires changing the theorem contract under the existing criteria.
• Citation and tool audit: check that every cited theorem, standard fact, technical tool, direct derivation, current-notation wrapper, primitive-source derivation, or dependency use names the current objects, assumptions to discharge, conclusion needed, and affected block or Step ID. For theorem-critical cited results, independently apply the Source-To-Claim Adequacy Gate even if proof_sketch_review.md accepted: 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 accepting the result as a step-local source. For theorem-critical standard tools, direct derivations, current-notation wrappers, and primitive-source derivations, independently require the raw-assumption-to-claim implication, convention check, source-convention compatibility when inherited or translated from another convention, quantitative scale or dominance relation, and branch or boundary stress needed by the exported interface. Treat plausible framework fit, intended mapping, unresolved source identity or label, unknown statement shape, category-level standard fact/tool, direct-derivation, current-notation, or primitive-source fit, unverified convention translation, or deferred local checking as insufficient.
• Quantitative dependence audit: when quantitative dependence is exposed or a baseline invariance obligation is present, check that variables, hidden-constant dependence, fixed quantities, probability or stochastic mode, horizon or limiting mode, norm or metric mode, auxiliary tolerances, public specialization obligations, baseline-reduction obligations, and inherited baseline/recovery conclusions are preserved or explicitly blocked.
• Scope and closure review: check ## 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. For each certificate entry, verify the target condition or control, declared theorem scope, local interface or recurrence when relevant, key positive/control term or structural source, defect or forcing terms, closure mechanism, mechanism source / boundary exclusion, source-to-claim adequacy when the target needs a structural lower/sign/support/nondegeneracy claim, obligation locality classification, noncircular closure status when applicable, entry-state / first-update stress result when applicable, primitive controls, generated controls, boundary stress result, and failure mode if the mechanism is absent. For every all-time or accumulated row, also verify the concrete recurrence/potential or mechanism-specific control relation, the accumulated defect or forcing term, its sign status, one-step charge/absorption/potential-drop, preservation, projection, coupling, stopping, or conditioning relation, and finite-budget or declared-scope validity justification. Reject acceptance when a row only says later step work will close the condition or only names a closure category such as finite-budgeted, monotone-potential controlled, Lyapunov, first-exit, reserve, ledger, stopped/conditioned, locally absorbed, small-gain, projection, dissipative recurrence, or algebraic coupling. Reject as REVISE_GLOBAL if the accepted sketch already contains the concrete relation but the certificate is absent, too shallow, omits or misstates it, names a closure category without exposing the relation and mechanism source, omits source adequacy for a structural lower/sign/support/nondegeneracy claim, omits a theorem-critical mechanism witness already present in the accepted sketch, omits or misstates a row's obligation locality classification, omits or misstates a required noncircular closure status, omits or misstates a required entry-state trace, or fails to expose the key recurrence/interface. Reject as REVISE_SKETCH if passing the certificate requires a new same-setting bridge step, changed step target, changed dependency, changed assumption, changed generated-condition interface, changed closure mechanism, changed mechanism witness, changed mechanism source, changed source-to-claim adequacy, changed entry-state interface or boundary exclusion, changed quantitative-specialization interface, or a new concrete recurrence/potential or mechanism-specific control relation under the current theorem contract. Reject as IDEA_FAIL if the claimed theorem contract cannot be supported without changing primitive assumptions, algorithm/model/procedure, theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Baseline invariance review: identify every theorem-facing recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion inherited by the current target. Reject acceptance when global_proof.md omits it, replaces it with a conservative or conditional surrogate, proves only that defect terms vanish, or labels its missing source as a hard local step without an existing source-adequate sketch interface and any applicable entry-state trace. Use REVISE_GLOBAL only when the accepted sketch already contains valid baseline evidence and the diagnostic failed to expose it; otherwise route to REVISE_SKETCH or IDEA_FAIL by the existing theorem-contract criteria.
• Source-convention compatibility review: for every 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 differ, acceptance requires an explicit bridge in the accepted sketch and diagnostic; otherwise route to REVISE_SKETCH or IDEA_FAIL using the existing theorem-contract criteria.
• Object-target compatibility review: for theorem-critical initialization, entry, basin, contraction, recurrence, structural support/nondegeneracy, or baseline wrappers, independently instantiate the exact deterministic, population, no-error, or baseline entry object produced by the current procedure when meaningful, and compare it 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 already supported by the accepted sketch and diagnostic. Reject acceptance if the diagnostic treats source-convention compatibility or nondegeneracy, gap, boundedness, curvature, concentration, or smallness of the produced or surrogate object as sufficient without equality or an explicit bridge to the consumed target object and required target scale. Use REVISE_GLOBAL only when the accepted sketch already contains the valid object-target bridge and global_proof.md failed to expose it; otherwise route to REVISE_SKETCH or IDEA_FAIL using the existing theorem-contract criteria.
• Noncircular closure review: for all-time, uniform, limsup, invariant, stability, recurrence, support, basin, boundedness, and generated-condition entries, verify that the certificate names a noncircular producer or mechanism source, exit/defect/control relation, and dependency path to each consumer. Reject acceptance if the source assumes the same target closure, generated condition, or final theorem consequence; use REVISE_SKETCH when a same-setting bridge or interface could repair the circularity, and IDEA_FAIL only after identifying 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.
• Step-locality and theorem-contract review: in Scope And Closure Review, Hard-Step Localization Audit, and Early Idea-Failure Screen, classify every theorem-critical hard obligation as step-local, sketch/interface defect, or idea/theorem-contract defect. A future proof step is not a mechanism source. ACCEPTED is valid only when the needed mechanism source already exists 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 whose source-convention compatibility and raw-assumption-to-claim feasibility have already been checked at obstruction-level granularity, and the future proof step only instantiates the source under the unchanged accepted sketch and theorem contract. Use REVISE_SKETCH when the current idea can plausibly support the source but the roadmap, bridge, dependency, closure interface, generated-output flow, accumulation interface, decomposition, direct-derivation interface, standard-fact/tool interface, current-notation wrapper, primitive-source interface, or cited-tool plan is missing or wrong. Use IDEA_FAIL when repairing the missing source would require changing primitive assumptions, algorithm/model/procedure, theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Gate evidence review: ## Gate Evidence Table must 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. Use REVISE_GLOBAL only when the accepted sketch already contains the valid evidence and global_proof.md failed to expose it; otherwise route to REVISE_SKETCH or IDEA_FAIL using the smallest sound retry target.
• Scope-accumulation review: when a certificate entry concerns a repeated, iterated, recursive, limiting, or otherwise accumulated theorem-critical control, verify that it 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. The classification is valid only when it names the accumulated defect, whether its sign is controlled or adversarial/unknown, the budget/potential or mechanism-specific control relation controlling cumulative effect, the 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 stated all-time, uniform, limsup, or other declared scope. Persistent, one-sided, nondecaying, additive, or adversarial-sign terms are unsupported unless that concrete current-target-compatible relation is identified. Reject as REVISE_GLOBAL only if the accepted sketch already contains this concrete accumulation interface but the diagnostic omitted or misstated it. Reject as REVISE_SKETCH if the sketch needs a new or changed accumulation interface, bridge, dependency, closure mechanism, boundary exclusion, generated-condition interface, or same-setting control relation. Reject as IDEA_FAIL if compatibility requires changing primitive assumptions, algorithm/model/procedure, theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Entry-state trace review: when a certificate entry concerns a recursive, iterative, descent, contraction, convergence, all-time, recurrence closure, invariant, basin/support, mode-conversion, or exact/noiseless specialization claim, verify that the diagnostic names an allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state and traces the first update, transition, or stationary behavior. Reject acceptance if the mechanism source is inactive while the theorem-facing conclusion remains false, or if the diagnostic only says a future step, induction, basin argument, or closure handles the state without showing an already available source under the current theorem contract.
• Scope-compatible closure mechanisms must be one or more of: 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. A scope-compatible mechanism must also have a valid mechanism source: a primitive condition, accepted derived control, 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 theorem target. If no listed mechanism and mechanism source, or equivalent explicitly conditional theorem target, is available under the declared scope, the artifact cannot be accepted. Naming the mechanism category is not enough unless the diagnostic exposes the concrete relation required by the Scope-Accumulation Compatibility Gate.
• Theorem-critical mechanism witness review: independently check every hard local obligation or theorem-level block central to final theorem closure, recurrence, invariant maintenance, structural lower/sign/coercivity/nondegeneracy/support claims, scope upgrades, quantitative specialization, theorem-facing generated invariant, boundedness, balance, support, basin, local-validity, factor self-bound, or all-time closure claim. Acceptance requires an obstruction-level witness with claim class, theorem role, mechanism source, source-to-claim match, source-convention compatibility when a source supplies the mechanism or output, key positive/control term or structural source, opposing defect terms, closure/dominance/absorption relation, boundary/null-regime handling, and producer-consumer provenance when relevant. Control of a primary descent metric is not a witness for a generated direction unless the diagnostic states the coupling inequality from the primary metric to the generated quantity. Reject as REVISE_GLOBAL only when the accepted sketch already contains the witness and source-convention compatibility evidence and global_proof.md merely failed to expose it. Reject as REVISE_SKETCH when the same setting may support the witness through a revised bridge, source-convention bridge, interface, generated-condition interface, output flow, or quantitative-specialization/loss-routing step. Reject as IDEA_FAIL only when supplying the witness would require changing primitive assumptions, algorithm/model/procedure, theorem scope/mode/metric, exposed dependence, or success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Global obstruction audit: check the reviewed global_proof.md Early Obstruction And Repair Plausibility section. Treat missing or shallow obstruction analysis as REVISE_GLOBAL; treat a correctly exposed roadmap obstruction as REVISE_SKETCH when it is a missing bridge, interface, decomposition, closure path, generated-output flow, accumulation interface, or other target-preserving repair under the same theorem contract, and as IDEA_FAIL only after identifying 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.
• Hard-step localization audit: distinguish hard local proof obligations under unchanged sketch steps from defects that require a changed roadmap, new bridge, changed assumption, changed dependency, changed generated-condition interface, changed closure mechanism, changed mechanism source, changed boundary exclusion, changed theorem scope/mode/metric, changed exposed dependence, changed success criterion, or weakening the conclusion. Record the Step-Locality And Theorem-Contract Gate classification for each theorem-critical hard obligation.
• Hard-step flow audit: do not accept a diagnostic that labels a missing generated-output producer, missing consumer dependency, or unsupported generated-output export as a hard local step. A hard step remains local only when the generated output it consumes already has a legal producer-consumer path under unchanged sketch steps and dependencies.
• Hard-step exported-interface audit: do not accept a diagnostic that labels a missing downstream-facing interface as a hard local step when the accepted sketch does not already expose the raw controls, exported claim, defect split, dominance or transfer relation, residual-to-target adequacy when a bridge transfers a produced, baseline, transformed, or surrogate object or control into the consumed target, margin or threshold source, and consumers. A hard step remains local only when the step worker is deriving a relation whose interface and sources are already fixed under the accepted sketch.
• Hard-step source-interface audit: do not accept a diagnostic that labels a theorem-critical generated event, structural wrapper, margin, threshold, recurrence source, or public bridge as hard local work merely because a direct derivation, standard fact or tool, current-notation wrapper, or primitive-source derivation is assigned to a future step. A hard step remains local only when the accepted sketch and diagnostic already expose source-convention compatibility, the source convention, raw-assumption-to-output path, quantitative dominance or transfer relation, residual-to-target adequacy when a bridge transfers a produced, baseline, transformed, or surrogate object or control into the consumed target, branch or boundary handling, and downstream interface.
• Hard-step cited-wrapper audit: do not accept a diagnostic that labels a theorem-critical cited-wrapper output as hard local work when the accepted sketch has not already fixed the current-notation wrapper conclusion, source hypotheses, source-convention compatibility, hypothesis discharge path, known non-output boundaries, any wrapper bridge, raw controls, controlled and uncontrolled defect classes, margin/slack/reserve or threshold source, exported interface, and downstream consumers. Use REVISE_GLOBAL only when the accepted sketch already contains this evidence and the diagnostic omitted it; use REVISE_SKETCH when the sketch must add or change the wrapper bridge, interface, dependency, defect split, convention bridge, or margin/reserve source; use IDEA_FAIL only when repair requires a theorem-contract change.
• Hard-step accumulation audit: do not accept a diagnostic that labels an accumulated generated-condition or recurrence closure as a hard local step when the defect behavior is persistent, one-sided, nondecaying, additive, adversarial-sign, or otherwise noncompatible with the declared theorem scope and no current-target-compatible absorption, dissipation, cancellation, stopping or conditioning, scope-limited budget, source exclusion, or explicitly conditional target is identified.
• Hard-step entry-state audit: do not accept a diagnostic that labels an allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state obstruction as a hard local step when the first update, transition, or stationary behavior leaves the mechanism inactive and the theorem-facing conclusion remains false. Use REVISE_SKETCH when a same-setting bridge, conditional interface, basin split, excluded-boundary clause, or conservative target-preserving loss can repair the issue, and IDEA_FAIL when repair requires changing primitive entry or initialization assumptions, the algorithm/model/procedure, theorem scope/mode/metric, exposed dependence, success criterion, adding a theorem-facing mechanism source not supported by the setting, or weakening the conclusion.
• Mechanism-source hard rejection: do not accept a diagnostic that labels contraction, coercivity, positivity, nondegeneracy, lower-bound, signed-descent, support-preservation, basin-closure, recurrence-closure, or exact/zero-limit work as a hard local step when its source is only generic geometry, local tube, small gain, later step, upper bounds, finite budgets, local boxes, admissibility inequalities, or similar wording. Acceptance requires a concrete nonzero/sign/support/conditioning source adequate for the claim class and a null, degenerate, exact/noiseless, or boundary stress check showing that the mechanism cannot vanish while the target conclusion would remain false or the theorem-critical obstruction would remain present. If the missing source can be added by changing the sketch, use REVISE_SKETCH; if it would require changing primitive assumptions, algorithm/model/procedure, 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 IDEA_FAIL.
• Early idea-failure screen: do not let the diagnostic label a theorem-contract obstruction as a merely hard local step. A hard step remains step-local only when the needed conclusion is already an accepted sketch claim, the global diagnostic gives a source-adequate same-setting proof interface with a scope-compatible closure mechanism and mechanism source, any required residual-to-target adequacy is already exposed for bridges from produced, baseline, transformed, or surrogate objects or controls into consumed targets, the source already exists 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-to-output feasibility, and no new theorem-facing assumption, mechanism, mode change, scope change, metric change, exposed dependence change, success criterion change, or weakening the conclusion is needed.
• Same-setting repair plausibility: choose REVISE_GLOBAL for diagnostic-document defects under the same sketch, REVISE_SKETCH for roadmap defects that remain plausibly repairable in the same idea, and IDEA_FAIL only for current-idea obstructions.

Early Idea-Failure Screen

Apply this screen before accepting global_proof.md, even when it reports COMPLETE_DRAFT or PARTIAL_BLOCKED.

Do not try to prove a blocked step. Instead, use short theorem-level obstruction checks:

• Contract contradiction check: ask whether the attempted theorem needs a property, mode, condition, boundedness, stability, recurrence closure, convergence upgrade, cancellation, comparison, accumulation bound, generated-condition support, or quantitative simplification that the setting forbids, excludes from primitive assumptions, or only allows as a derived conclusion without a producer path.
• Missing-mechanism check: if global_proof.md assigns a hard block to future step work, identify the mechanism and mechanism source that would make the block true, and check whether the source is adequate for the claim class. If either is absent from primitive assumptions, accepted prior blocks, cited tools, direct derivations, standard facts or tools, current-notation wrappers, primitive-source derivations with checked source-convention compatibility and raw-assumption feasibility, explicitly conditional targets, and the accepted sketch interface, or if the source is only an upper/size/budget/local-validity/small-gain control for a lower/sign/support/coercivity/nondegeneracy claim, treat the issue as REVISE_SKETCH or IDEA_FAIL, not ACCEPTED.
• Obligation-locality check: classify every alleged hard local block as step-local, sketch/interface defect, or idea/theorem-contract defect. Route to REVISE_SKETCH when a source-adequate mechanism appears available under the current theorem contract but the accepted sketch fails to expose the bridge, source-convention compatibility, interface, dependency, closure mechanism, generated-output flow, accumulation behavior, decomposition, or cited-tool discharge, or when the obstruction is only a missing bridge, interface, or decomposition under the same theorem contract. This same-setting plausibility is routing evidence only, not acceptance evidence; step-local acceptance still requires a source-adequate mechanism, source-convention compatibility when a source supplies the mechanism or output, and valid cited-tool discharge when applicable. Route to IDEA_FAIL only after identifying 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.
• Direct/standard/current-notation/primitive-source feasibility check: when an alleged hard local block is assigned to a direct derivation, standard fact or tool, current-notation wrapper, or primitive-source derivation, verify at obstruction-level granularity that source-convention compatibility is exposed and that the exact primitive assumptions and accepted dependencies imply the exported interface under the declared convention, dependence, and every allowed branch or regime it covers. If this convention bridge or implication is absent or false, route to REVISE_SKETCH or IDEA_FAIL, not ACCEPTED.
• Source-convention stress check: when an alleged hard local block depends on a cited tool, standard fact or tool, current-notation wrapper, direct derivation, or primitive-source derivation inherited or translated from another convention, instantiate any relevant no-error, no-noise, population, limiting, exact-baseline, or entry specialization and check whether the source target and consumed branch target coincide under the branch metric, objects, and procedure. If they differ without an explicit bridge, route before step proof.
• Object-target stress check: when an alleged hard local block depends on an initialized, entry, reference, population, no-error, or baseline object, instantiate the exact produced object and the consumed target object under the branch procedure and theorem metric. If the produced object is transformed, weighted, preconditioned, whitened, reference-operator-modified, or otherwise surrogate relative to the consumed target, check for an explicit same-target bridge with residual-to-target adequacy before accepting the block as local. If the produced object is only shown to have its own nondegeneracy, gap, boundedness, curvature, concentration, or smallness, and no bridge shows it lies in or controls the consumed target interface at the required target scale, route before step proof.
• Residual-to-target stress check: when an alleged hard local block depends on transferring a produced, baseline, transformed, or surrogate object or control to a consumed target, expose the residual decomposition, source for each residual term, theorem metric or norm, and required target margin or scale. If any residual is uncontrolled, persistent, fixed, event-level, wrong-scale, or controlled only for the source-side object, route before step proof.
• Entry-state trace check: for every alleged hard local recursive, iterative, descent, contraction, convergence, all-time, recurrence closure, invariant, basin/support, mode-conversion, or exact/noiseless specialization block, instantiate an allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state and trace the first update, transition, or stationary behavior at obstruction-level granularity. Do not accept when the mechanism is inactive while the target conclusion remains false; decide whether the repair is a same-setting sketch repair or an idea-level theorem-contract change.
• Nonvacuity check: for any hard block whose conclusion needs contraction, coercivity, positivity, nondegeneracy, a lower bound, signed descent, support preservation, basin closure, recurrence closure, or exact/zero-limit behavior, test the allowed null or degenerate regime where the proposed mechanism is zero while the target conclusion would remain false or the theorem-critical obstruction would remain present. If no accepted source excludes that regime, do not accept the diagnostic.
• Shallow-certificate check: reject acceptance when any certificate entry covered by the Theorem-Critical Mechanism Witness Gate does not name the target condition or control, claim class and theorem role, local interface or recurrence when relevant, key positive/control term or structural source, defect or forcing terms, closure mechanism, mechanism source / boundary exclusion, source-to-claim adequacy when relevant, entry-state / first-update stress result when applicable, primitive controls, generated controls, closure/dominance/absorption relation, boundary stress result, and failure mode if the mechanism is absent. A claim that later local proving will close the condition or supply the witness is not a mechanism.
• Accumulation-defect check: when a local interface exposes a noncontractive, one-sided, additive, accumulated, biased, non-summable, persistent, nondecaying, adversarial-sign, or otherwise noncompatible term, check whether the declared theorem scope or conclusion would require local absorption, contraction, summability, cancellation, monotone-potential control, source exclusion, stopping or conditioning, a scope-limited budget, or another bridge. First decide whether exposing, routing, or absorbing the term through a current-target-compatible bridge is a same-setting sketch repair. Use IDEA_FAIL only after identifying 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. If the obstruction is only a missing bridge, interface, or decomposition under the same theorem contract, route REVISE_SKETCH.
• Interface-defect check: when a local interface exposes multiple defect classes, check whether each class has a source or threshold that can control it under the unchanged sketch. A threshold, margin, or cited wrapper that controls only one defect class cannot support an exported interface whose other defect classes are fixed, empirical, event-level, persistent, or irreducible unless another source controls those terms. If the obstruction is a missing bridge, split, or dominance relation under the same theorem contract, route REVISE_SKETCH.
• Limiting and boundary stress: test allowed degenerate, boundary, exact, noiseless, high-precision, low-sample, large-scope, adversarial-sign, null-direction, entry-state, stationary-state, or baseline regimes only to the extent needed to reveal whether the claimed mechanism source is still nonvacuous. Do not develop a full counterexample when a short structural mismatch is enough.
• Generated-condition check: reject acceptance when generated-object, event, local-validity, boundedness, stability, recurrence, membership, structural, support, basin, or invariant facts are effectively required as theorem-facing assumptions for an unconditional target or are deferred to a future proof step without an already identified mechanism source and producer path.
• Generated-output flow check: reject acceptance when a theorem-facing generated output is consumed without a legal producer-consumer path, or when a closure, specialization, assembly, or later-proof label exports such an output without proving it from accepted inputs. First decide whether adding or reallocating a bridge, output target, dependency, or conditional local interface is a same-setting sketch repair.
• Dependence and mode check: if the strongest supported bound necessarily depends on an index, horizon, event, tolerance, initialization, approximation level, confidence parameter, data quantity, algorithmic quantity, or generated radius that the theorem excludes or hides, decide whether exposing that dependence is a same-setting sketch repair or a changed idea. Use IDEA_FAIL when the public theorem scope/mode/metric, exposed dependence, or success criterion must change, or when repair requires weakening the conclusion.
• Baseline invariance check: if the strongest supported statement preserves only a weaker baseline, conservative remainder, conditional/stopped/finite-scope conclusion, or vanishing-defect clause while the current target inherited a stronger baseline/recovery conclusion, decide whether a same-setting sketch bridge can preserve the original conclusion. Use IDEA_FAIL when preserving the original baseline conclusion requires a theorem-contract change or when the diagnostic's proposed repair weakens the inherited conclusion.
• Same-setting repair cut: use REVISE_SKETCH when an added or rewritten bridge step, dependency interface, conditional local lemma with discharge, quantitative-specialization step, or conservative loss-routing step could plausibly support the missing property under the same setting and goal. Use IDEA_FAIL when 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.

When the screen triggers, ## Required Repair Bundle must state why /global-proof is insufficient and why /proof-sketch is either the right next target or insufficient. For entry-state trace failures, state the inactive mechanism for the allowed entry, initial, stationary, null, degenerate, exact/noiseless, or boundary state and whether repair requires a new sketch interface or a required theorem-contract change. For IDEA_FAIL, explicitly identify the setting or goal component that must change and 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.

Required Repair Bundle

For non-accepted reviews, list all material repair obligations, not just the first blocker. Each repair item must name:

• the affected artifact or section;
• the smallest repair target;
• the exact claim, block, step, dependency, assumption, citation, generated-output flow, generated-condition interface, closure mechanism, mechanism source, boundary exclusion, quantitative obligation, or diagnostic-boundary issue;
• whether the repair must preserve the current accepted sketch or requires a new sketch attempt.

Write Required Repair Bundle = None only when Global-Proof Review Status = ACCEPTED.

Writing Rules

• Include all template sections: Global-Proof Review Identity, Global-Proof Review Status, Smallest Retry Target, Blocking Issues, Required Repair Bundle, Contract And Status Audit, Claim And Sketch Fidelity Audit, Theorem-Level Structure Audit, Dependency And Assumption Audit, Citation And Tool Audit, Quantitative Dependence Audit, Scope And Closure Review, Gate Evidence Table, Hard-Step Localization Audit, Early Idea-Failure Screen, and Review Rationale.
• Use raw controlled tokens on their own line for Global-Proof Review Status and Smallest Retry Target; do not wrap them in Markdown code formatting.
• Do not prove the theorem or repair global_proof.md inside the review.
• Do not treat global_proof.md as mathematical authority. Review whether it is a usable diagnostic artifact only.
• If global_proof.md reports SKETCH_BLOCKED, independently decide whether the obstruction is sketch-level or idea-level and route to /proof-sketch or /subagent-idea-generator accordingly.
• If global_proof.md reports COMPLETE_DRAFT or PARTIAL_BLOCKED but the review finds a sketch-level or idea-level obstruction, choose the harsher review status and explain the mismatch.