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

Proof Review Aggregate

Use this internal final-review aggregator after all four specialized reviewers complete and their artifacts pass contract gates in the upgraded split workflow.

Contract

Required inputs:

• perspective_M/idea_N/setting.md
• perspective_M/idea_N/latex_template/1_intro.tex
• perspective_M/idea_N/latex_template/2_preliminary.tex
• perspective_M/idea_N/latex_template/3_main.tex
• perspective_M/idea_N/latex_template/4_proof_sketch.tex
• perspective_M/idea_N/latex_template/5_appendix.tex
• perspective_M/idea_N/latex_template/main.tex
• perspective_M/idea_N/latex_template/arxiv.sty
• perspective_M/idea_N/latex_template/ims.bst
• perspective_M/idea_N/latex_template/reference.bib
• perspective_M/idea_N/assembly_report.md
• accepted perspective_M/idea_N/proof_sketch.md
• accepted perspective_M/idea_N/proof_sketch_review.md
• valid diagnostic perspective_M/idea_N/global_proof.md paired with accepted perspective_M/idea_N/global_proof_review.md
• accepted perspective_M/idea_N/global_proof_review.md
• accepted proof_steps/<Step ID>/proof.md and proof_steps/<Step ID>/review.md artifacts for every required sketch step
• perspective_M/idea_N/proof_review_structural.md
• perspective_M/idea_N/proof_review_rigor.md
• perspective_M/idea_N/proof_review_citation.md
• perspective_M/idea_N/proof_review_adversarial.md

Output:

• perspective_M/idea_N/proof_review.md

Do not modify proofs, sketches, step artifacts, specialized reviews, trackers, worker logs, or accepted results. In upgraded split mode, this is the only skill that writes proof_review.md.

Responsibilities

• Validate the four specialized review artifacts against their machine-readable contracts.
• Compare the final attempted claim against authoritative setting.md.
• Combine specialized findings into exactly one controller-facing decision.
• Select the deepest blocking issue and the smallest retry target supported by the controller.
• Emit Score, Failure Type, Critical Issues, Suggested Next Action, and Retry Mode.

Specialized review artifacts, global_proof.md, and global_proof_review.md are diagnostic inputs. They do not prove the theorem and do not directly update trackers or route retries.

Workflow

Step 1: Load Aggregate Inputs

• Load setting.md, all content and support files under latex_template/, assembly_report.md, accepted proof_sketch.md, accepted proof_sketch_review.md, valid diagnostic global_proof.md, accepted global_proof_review.md, accepted step proof/review artifacts, and all four specialized reviews.
• Treat setting.md as the authoritative source for the formalized goal.
• If setting.md records source-alignment, progress-type, or materiality metadata, apply the Source-Direction Fidelity Contract from ../_shared/checklists/artifact-contracts.md as a final-claim labeling and alignment check.
• Treat specialized review artifacts, global_proof.md, and global_proof_review.md as diagnostic inputs only. They do not prove the theorem and do not directly update trackers or route retries.

Step 2: Validate Specialized Review Contracts

• Confirm the controller artifact gate has passed all four specialized reviews: structural, rigor, citation, and adversarial.
• If any specialized review artifact is missing or contract-invalid, stop and ask the controller to rerun or hand off only that specialized reviewer. Do not write or overwrite proof_review.md from invalid diagnostic inputs.
• For each specialized review, validate:
• Reviewer Verdict is exactly the raw token PASS or BLOCKING, with no Markdown code formatting, quotes, bullets, or surrounding prose.
• PASS has raw-token Blocking Issues = None, Suggested Repair Depth = None, and Smallest Candidate Repair Target = None, with no Markdown code formatting, quotes, bullets, or surrounding prose.
• BLOCKING has at least one numbered blocking issue, non-None Suggested Repair Depth, and an aligned repair target.
• Suggested Repair Depth is one of the raw tokens None, assembly, step, sketch, or idea.
• Smallest Candidate Repair Target is aligned with the repair depth and controller-supported targets.

Step 3: Run Aggregate Contract Checks

• Check that assembly_report.md has a valid completion status and that the LaTeX bundle is consistent with it and does not present unresolved blockers as proved. If assembly_report.md is missing or contract-invalid, set Failure Type = PROOF_ASSEMBLY_FLAW, Suggested Next Action = /proof-assembly, and Retry Mode = repair_assembly.
• If assembly_report.md has Status = PARTIAL_BLOCKED, treat its blockers as aggregate assembly blockers and route to /proof-assembly unless the report or public bundle shows the smallest valid repair target is /proof-step <Step ID> or /proof-sketch.
• Check that the LaTeX bundle is self-contained enough to be a paper-ready proof and does not introduce stronger claims, new assumptions, or unreviewed proof material.
• Run the public-TeX compile/support gate: latex_template/main.tex must compile from inside latex_template/ using the five content files and style; latex_template/arxiv.sty, latex_template/ims.bst, and latex_template/reference.bib must exist. When external citations are used, the compile entry must use reference.bib and ims.bst; when no external citations are used, the public output must not show a visible empty References section.
• Run the public-TeX structure gate: latex_template/1_intro.tex must contain \section{Theoretical Setup} with numbered assumption environments, each with a unique stable \label{assump:...} that preserves an assumption id from setting.md; latex_template/2_preliminary.tex must contain \section{Preliminaries} before the theorem and only useful notation explicitly derived from original setting quantities with what/why/main-theorem-use explanations; latex_template/3_main.tex must contain \section{Main Theorem}; latex_template/4_proof_sketch.tex must contain \section{Proof Sketch}; and latex_template/5_appendix.tex must contain \appendix, \section{Proof Details}, appendix subsections for required sketch steps named by step name or goal, allow multiple theorem-style units per subsection, and end with a final \subsection{Proof of the Main Theorem}.
• Run the main-theorem self-containedness gate: the theorem in latex_template/3_main.tex may use only notation defined in latex_template/1_intro.tex, numbered assumptions cited as Assumption~\ref{assump:...} or Assumptions~\ref{assump:...}, latex_template/2_preliminary.tex, or constants/functions fully defined inline inside the theorem statement before use with explicit dependence. Reject aggregate acceptance if the theorem refers to appendix-local results, proof-step IDs, step-local constants, or local-proof labels such as lem:, prop:, claim:, cor:, hyp:, inv:, or app:.
• Run the assumption-provenance gate from ../_shared/checklists/artifact-contracts.md. Reject aggregate acceptance if an unconditional public theorem or preliminary theorem-facing package assumes generated-object, event, local-validity, stability, boundedness, recurrence, membership, or invariant facts that are not primitive conditions and are not proved by named accepted-step, theorem-level, or appendix results before use.
• Run the main-theorem compactness/readability gate: if latex_template/3_main.tex retains a long or hard-to-read technical theorem dominated by admissibility dictionaries, then it must also contain a readable simplified theorem or corollary under domain-appropriate theorem-local simplifying assumptions that are explicitly stated and bridged. Reject aggregate acceptance for a dense technical theorem with no readable simplified theorem/corollary, even if all specialized reviewers pass.
• Reject aggregate acceptance when a readable corollary still depends on an unreadable theorem-level admissibility dictionary. The public theorem needs a concise reader-facing interface, and technical dictionaries must be moved into named appendix theorem-style results with a bridge when they are too large for the theorem statement.
• Run the public-appendix-shape gate: latex_template/5_appendix.tex may use only lemma, theorem, proposition, corollary, and proof environments for public theorem-style proof content, apart from appendix headings and concise mathematical exposition needed to introduce a result. Reject aggregate acceptance if the public appendix uses claim, hypothesis, or invariant environments or public Claim~, Hypothesis~, or Invariant~ proof dependencies. Accepted step-local claims, hypotheses, and invariants must be converted into lemma, theorem, proposition, or corollary statements with proofs, or integrated into proof text inside allowed proof environments.
• Run the theorem-style statement-shape gate: every public theorem, lemma, proposition, or corollary in latex_template/3_main.tex and latex_template/5_appendix.tex must be self-contained and state its assumption basis using Assumption~\ref{assump:...} / Assumptions~\ref{assump:...} references or named prior theorem-style results, list any local "if" conditions, and state the "then" conclusion before the proof. Reject aggregate acceptance when assumptions, regimes, parameter restrictions, or conclusions are only implicit in surrounding prose, subsection titles, proof-step IDs, local unit IDs, or proof text.
• Run the notation-economy, notation-provenance, derivation-over-notation, and constant-provenance gate: public preliminaries and the main theorem must avoid proof-local aliases, component radii, one-off bookkeeping quantities, and long helper-constant dictionaries unless they are essential public objects. When notation and derivational detail conflict, require fewer helper symbols and more visible derivation. Every public symbol, constant, radius, threshold, rate, margin, admissibility parameter, bounded quantity, finite-tube quantity, event, or helper object must be directly defined from original setting quantities, translated from an accepted dependency or checked cited result, explicitly present as a theorem/admissibility condition, or proved/bounded by a named local result. Reject aggregate acceptance for unexplained finite constants, free boundedness claims, notation not expressible from original setting quantities without a derivation, notation that hides proof obligations, or helper notation that replaces the derivation needed to audit boundedness, finiteness, rates, parameter dependence, cited-result assumption discharge, or implications.
• Reject aggregate acceptance when notation or an admissibility package hides an unproved derived invariant behind names such as verified, admissible, good, stable, regular, local-valid, recurrent, bounded, core, tube, basin, or membership. For explicitly conditional final targets, require the attempted claim and review to state the conditional scope.
• Run the proof-step notation-surface gate: verify that step helper objects are classified as public-facing, appendix-local, or proof-local when introduced, and reject aggregate acceptance when proof-local or appendix-local dictionaries leak into the main theorem without being essential public quantities. If the accepted step interface itself exported too much notation, route to /proof-step; if assembly promoted nonpublic helper objects unnecessarily, route to /proof-assembly.
• Run the proof-step assumption-provenance gate: verify that any theorem-facing derived invariant used by final assembly is proved by an accepted step or appendix result. If assembly wording is the only problem, route to /proof-assembly; if a step exported an unproved derived invariant, route to /proof-step <Step ID>; if the sketch lacks a bridge step, route to /proof-sketch.
• Run the explicit-rate gate from `../_shared/checklists/artifact-