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

Proof Assembly

Use this internal skill after all required proof steps have accepted reviews.

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
• accepted proof_steps/<Step ID>/proof.md and proof_steps/<Step ID>/review.md for every required sketch step

Optional input:

• final proof_review.md when repairing PROOF_ASSEMBLY_FLAW

Outputs:

• 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

Do not modify sketch artifacts, step artifacts, trackers, worker logs, or accepted results.

Responsibilities

• Assemble only accepted step proofs into theorem-level form.
• Preserve accepted step statements, assumptions, and dependencies.
• Prove the final theorem by composing accepted step claims and direct assembly-only implications.
• Write latex_template/ as the canonical public proof source. In the LaTeX bundle, "paper-ready" means polished theorem-style exposition: compact exposition for the main theorem and proof sketch, but complete journal-style proof detail for latex_template/5_appendix.tex, not a condensed appendix summary.
• Write assembly_report.md as the controller-private assembly status artifact. Do not put workflow status fields such as ## Status, COMPLETE, or PARTIAL_BLOCKED into public TeX.
• Stop honestly when assembly needs an unreviewed lemma, changed step statement, changed assumption, or new proof obligation.

Workflow

Step 1: Load Accepted Inputs

• Read the exact formalized setting and goal from setting.md, including the stable assump:<slug> ids assigned to technical assumptions.
• Read the accepted proof_sketch.md and proof_sketch_review.md.
• Read every accepted proof_steps/<Step ID>/proof.md and proof_steps/<Step ID>/review.md required by the sketch.
• If repairing from final proof_review.md, repair only assembly-level defects, notation reconciliation, presentation, or LaTeX-bundle synchronization. Do not repair step or sketch defects inside assembly.
• If repairing PROOF_ASSEMBLY_FLAW that reports compressed, missing, or unsynchronized appendix proof detail, regenerate each affected appendix subsection from the corresponding accepted proof-step source body. Do not use the compressed appendix as the proof source and do not try to polish a representative summary into acceptance. Severe shortening is repairable only after direct comparison with the accepted source sections shows that the removed text is non-proof cleanup, exact duplicate setup, or valid repetition under the repetition rule.

Step 2: Verify Coverage And Dependency Closure

• Confirm every required sketch step has an accepted proof artifact and an accepted review artifact.
• Confirm every step dependency used by an accepted step is also accepted and available.
• Treat the accepted proof_steps/<Step ID>/proof.md files as the source of truth for appendix derivations. For every used accepted step, perform an internal proof-obligation pass over that step's ## Local Derivation, all invoked ## Cited Result Applications, and ## Target-Step Assembly.
• Preserve every mathematical proof-obligation item from that pass in the matching latex_template/5_appendix.tex subsection unless it is exact duplicate setup, non-mathematical repetition, or a genuinely repeated derivation represented by one complete instance plus exact substitutions for each abbreviated instance.
• Removing workflow labels, proof-flow headings, provenance phrases, audit scaffolding, sketch-row fields, or dependency inventories never authorizes deleting the mathematical content beneath them. Rewrite the mathematical content as theorem-style statements, proof text inside proof environments, displayed derivations, cited-result instantiations, or assumption-discharge text; omit the audit packaging itself from public TeX.
• If a sketch step is unnecessary for the final theorem, record the reason in the assembly text; do not silently drop it.
• If a required step, local unit, cited-result application, boundary case, assumption discharge, target-step assembly, source unit, or dependency is missing, stale, rejected, unresolved, or cannot be translated into the appendix, keep the bundle honest, do not present the target as proved, and record the blocker in assembly_report.md.

Step 3: Set Attempted Claim And Assembly Report

• Set assembly_report.md ## Status to COMPLETE only when the accepted step claims and direct assembly-only implications prove the formalized goal in a reviewable way.
• In exact-goal mode, COMPLETE requires the attempted claim to match the exact target claim from setting.md.
• In target-spec mode, COMPLETE requires the attempted claim to be a concrete valid instantiation of the target quantity, claim type, active scope, success criterion, and required dependence.
• If required dependence is explicit in the goal, do not leave placeholder dependence such as "up to constants" or "up to polynomial factors".
• If a needed derived invariant is not proved by accepted steps or direct assembly-only implications, set assembly_report.md ## Status to PARTIAL_BLOCKED and name the missing Assumption Provenance Bridge. Do not repair by adding the derived invariant to the main theorem assumptions unless the formalized goal is explicitly conditional.
• If the assembly proves only a weaker statement, use that exact weaker attempted claim and set assembly_report.md ## Status to PARTIAL_BLOCKED.
• If blocked, keep valid assembled content and name the exact failed target theorem, accepted step block, missing coverage item, notation reconciliation, dependency closure, or final implication in assembly_report.md ## Blockers.

Step 4: Write LaTeX Bundle