<< All versions

Skill v1.0.0

currentAutomated scan100/100
dechenzhang/valg-ml-theory-agent/proof-assembly
──Details
PublishedNovember 1, 2026 at 11:38 AM
Content Hashsha256:03ace1a094bb8063...
Git SHAb4363f768c36
──Files
Files (1 file, 54.6 KB)
SKILL.md54.6 KBactive
SKILL.md · 214 lines · 54.6 KB

name: proof-assembly description: Assemble accepted proof-step artifacts into a self-contained, paper-ready LaTeX bundle without introducing unreviewed lemmas. metadata: version: "1.0.0"


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

  • Use ../_shared/templates/latex_template/ as the canonical public proof template.
  • Copy or instantiate the support files latex_template/main.tex, latex_template/arxiv.sty, latex_template/ims.bst, and latex_template/reference.bib from the shared template. Do not drop support files during repair.
  • Keep latex_template/main.tex as the compile entry using the five content files, style, and bibliography behavior.
  • Replace the placeholder title Paper Title in latex_template/main.tex with a concise theorem-specific title derived from setting.md or the attempted claim. Keep \author{} empty unless reliable author metadata already exists; do not invent authors.
  • Present the supported theorem, assumptions, intermediate results, and assembly across the five content files in latex_template/, while adding the full local derivations required for a self-contained paper proof.
  • Write latex_template/1_intro.tex with \section{Theoretical Setup}, the formalized setting, numbered theorem-critical assumption environments, and the formalized goal without raw markdown heading syntax.
  • Rewrite every theorem-critical setting assumption as a numbered assumption environment, visible as Assumption 1, Assumption 2, and so on, for example \begin{assumption}[Short name]\label{assump:smoothness} ... \end{assumption}. Use the stable assump:<slug> ids from setting.md as the LaTeX labels, cite them later as Assumption~\ref{assump:...} or Assumptions~\ref{assump:...}, and do not rename them. Do not hide assumptions in prose or introduce new assumptions later.
  • Write latex_template/2_preliminary.tex with \section{Preliminaries}. Define only useful and meaningful notation explicitly derived from the formalized setting that is needed to state or read the main theorem. For every new notation, state what original setting objects define it, why it is introduced, and where it is used in the main theorem. Do not add new assumptions, proof claims, proof obligations, proof-only shorthand, component radii, or one-off/non-conceptual constants in preliminaries; define such constants directly in the main theorem or local proof where needed.
  • Do not define theorem-facing admissibility, good-event, local-validity, stability, boundedness, recurrence, membership, or invariant packages in preliminaries if they contain unproved derived invariants. Such facts must be stated and proved as appendix theorem-style results from primitive conditions, or set assembly_report.md ## Status to PARTIAL_BLOCKED.
  • Use notation economy and notation provenance in public TeX. Prefer the original setting notation and full definitions when an alias is used only once or only abbreviates a simple norm, radius, probability level, or bookkeeping quantity. Do not generate or assume notation that is not explicitly expressed from original setting quantities. Heavy helper notation may appear in appendix proofs when it clarifies a derivation, but if it is not expressible from original setting notation or accepted translated objects, the appendix must first derive or prove its existence/bound in a named theorem-style result.
  • Use derivation-over-notation discipline. When notation and derivational detail conflict, prefer fewer helper symbols and more visible derivation. New notation may shorten repeated complex expressions or name stable conceptual objects, but it must not replace visible proof lines for boundedness, finiteness, rates, parameter dependence, cited-result assumption discharge, or theorem implications.
  • Respect proof-step public-surface classifications. Objects marked proof-local or appendix-local should not appear in the main theorem unless assembly proves they are essential public quantities; when many helper objects are needed, put them in named appendix results and expose a compact theorem-level interface.
  • Write latex_template/3_main.tex with \section{Main Theorem} and one main theorem matching the strongest claim actually supported by accepted step artifacts and direct assembly-only reasoning.
  • Keep the main theorem statement compact and readable. This compactness rule applies only to latex_template/3_main.tex theorem statements and does not apply to proof bodies in latex_template/5_appendix.tex. State the result using basic setting objects, numbered assumption references such as Assumption~\ref{assump:...}, and only essential theorem-local quantities. Theorem-critical assumptions and admissibility conditions must still be stated before or inside the theorem; move only proof-local helper dictionaries, component radii, margins, thresholds, or bookkeeping expansions into appendix lemmas/propositions, and cite those appendix results in the proof of the theorem rather than expanding every helper definition in the theorem statement.
  • The main theorem may assume primitive conditions and explicit theorem-local scalar or static conditions, but it must not assume derived invariants for an unconditional target. Derived invariants include generated-object membership, realized event membership, recurrence applicability, contraction, stability, boundedness, local model validity, basin/tube/core membership, and similar facts whose truth depends on proof-produced objects.
  • The main theorem should be reader-first: it should expose the claim, assumption basis, admissibility or specialization conditions, rate or remainder shape, probability mode, horizon mode, norm mode, and allowed dependence without becoming a long dictionary of helper quantities. If a technical admissibility package is lengthy, state it as a named theorem-local condition and prove or expand it in a named appendix result plus bridge.
  • If a technical admissibility package is theorem-facing, its contents must satisfy the Assumption Provenance Contract. Put derived-invariant parts in named appendix results and expose only primitive conditions, or explicitly mark the final theorem as conditional when the formalized goal is conditional.
  • If the supported technical main theorem is still long, difficult to read, or dominated by admissibility dictionaries after applying notation economy, also include a readable simplified theorem or corollary in latex_template/3_main.tex. The simplified result must be explicitly theorem-local: it may impose domain-appropriate simplifying assumptions that are explicitly stated and bridged, but it must not replace, silently weaken, or be presented as the full technical target.
  • A readable corollary is not enough if it still depends on an unreadable theorem-level admissibility dictionary. In that case, move the dictionary into named appendix theorem-style results and expose a concise public theorem or bridge statement.
  • Apply the shared Explicit Rate Contract from ../_shared/checklists/artifact-contracts.md to every public explicit rate. The main theorem, simplified theorem, or corollary must declare exposed variables, hidden-constant dependence, fixed quantities, probability mode, horizon mode, and norm mode.
  • If a public theorem or corollary states a simplified explicit rate derived from a more technical appendix theorem, include a named Rate Specialization Bridge. Use one of two public shapes: either a self-contained corollary in latex_template/3_main.tex whose proof contains the bridge, or a short corollary in latex_template/3_main.tex that states the auxiliary choices and cites a named appendix proposition proving the bridge.
  • The Rate Specialization Bridge must explicitly cover auxiliary parameter choice, technical condition verification, term absorption/simplification inequalities, probability conversion, and the final simplified rate statement. It must prove that the public theorem assumptions imply every appendix technical condition and must state the final hidden-constant dependence.
  • Do not drop any required structural, data/sampling, algorithmic/horizon, regularity/stability, numerical/stochastic/approximation/modeling-error, auxiliary-tolerance, or confidence/probability dependence while moving from appendix theorem to public rate unless the bridge proves the specialization. Every absorbed term needs a displayed inequality and admissibility threshold; prose-only absorption is an assembly blocker.
  • When the assembled theorem extends, perturbs, or specializes a prior theorem, dependency result, simpler regime, or limiting regime, include a baseline-reduction statement in the main theorem, corollary, or bridge proof. It must state how the new result reduces to the corresponding baseline result under the relevant specialization, or explicitly justify any conservative loss. If the baseline is an inherited theorem-facing recovery, reduction, specialization, zero-defect, exact-limit, exact/noiseless, or baseline-case conclusion, preserve that original conclusion; a conservative loss or weaker surrogate is target-changing.
  • Make the main theorem statement self-contained relative to latex_template/1_intro.tex and latex_template/2_preliminary.tex: it may use only setting objects, numbered assumptions cited as Assumption~\ref{assump:...} or Assumptions~\ref{assump:...}, and preliminary notation defined before the theorem, plus theorem-local constants or functions fully defined inline before use. Inline theorem constants must state their dependence explicitly and may depend only on setting/preliminary objects.
  • Use explicit self-contained statement shape for the main theorem and appendix theorem-style results. Each public theorem, lemma, proposition, or corollary must state its assumption basis, local conditions, and conclusion in the statement itself, normally in the form "Under Assumption~\ref{assump:...} and [named prior theorem-style results], if [specific conditions], then [conclusion]." Do not rely on surrounding prose, subsection titles, proof-step IDs, local unit IDs, or hidden proof context to supply assumptions or conditions.
  • Every constant, radius, threshold, rate, margin, admissibility parameter, bounded quantity, finite-tube quantity, event, or helper object introduced in the public LaTeX bundle must have clear provenance: it is either 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 lemma/proposition. Do not introduce a free "choose finite constants" or "let bounded quantities exist" statement unless that boundedness is an explicit theorem condition or is proved from the setting.
  • Every theorem-facing generated-object, event, local-validity, stability, boundedness, recurrence, membership, or invariant condition must have assumption provenance: primitive setting condition, accepted dependency conclusion, direct assembly consequence, or named appendix proof. If it is only a conditional hypothesis, do not use it to prove an unconditional main theorem.
  • Do not let the main theorem statement refer forward to appendix-local lemmas, propositions, claims, corollaries, hypotheses, invariants, step-assembly results, proof-step IDs, or constants introduced only inside latex_template/5_appendix.tex. In the theorem environment, do not use references with local-proof prefixes such as \ref{lem:...}, \ref{prop:...}, \ref{claim:...}, \ref{cor:...}, \ref{hyp:...}, \ref{inv:...}, or \ref{app:...}; references to numbered assumptions are allowed only in paper-ready form such as Assumption~\ref{assump:...}.
  • Write latex_template/4_proof_sketch.tex with a public proof sketch that summarizes the proof roadmap without replacing the appendix proofs and without naming internal workflow artifacts.
  • Write latex_template/5_appendix.tex beginning with \appendix and \section{Proof Details}. Create one subsection per accepted sketch step, titled by the step name or goal. Each subsection may contain multiple lemmas, theorems, propositions, corollaries, and proofs when the step requires several theorem-style units. Public appendix proof content must use only lemma, theorem, proposition, corollary, and proof environments, apart from appendix headings and concise mathematical exposition needed to introduce a result. Do not use public claim, hypothesis, or invariant environments; convert such local proof-step units into lemmas, theorems, propositions, or corollaries when they appear in the appendix. Appendix proof bodies should be long enough to reproduce the accepted local derivations in complete journal-style proof detail, not shortened into a concise appendix summary.
  • Begin each appendix subsection with theorem-style units or concise mathematical exposition needed to read those units. Do not start subsections with workflow scaffolding, dependency inventory, proof-flow narration, provenance narration, or reviewer-style audit text; integrate necessary assumptions, object mappings, dependency uses, and any mathematical content under removed workflow wording into statements and proofs.
  • When latex_template/3_main.tex cites an appendix Rate Specialization Bridge, write it as a named theorem-style proposition or corollary in latex_template/5_appendix.tex, not as prose. The statement and proof must include the auxiliary parameter choices, every technical condition inherited from the appendix theorem, all term-absorption inequalities, the probability conversion, and the final simplified rate.
  • Apply stepwise appendix assembly: for each accepted sketch step used in the main theorem, assemble that step's appendix subsection independently before starting the next step. Read that step's source proof body and translate the sections already required by the appendix rules together so local derivations and target assembly reasoning stay in the same paper-facing subsection.
  • Critical guardrail: do not write 5_appendix.tex from a whole-proof memory summary or only from final step claims. Draft each appendix subsection from the corresponding proof-step source body first, then polish grammar, prose, and notation without condensing the source derivation.
  • Use a private proof-obligation pass for each used step before drafting its appendix subsection. In source order, identify each displayed equation block, inequality chain, definition, constant/radius/threshold construction, case split, induction or invariant transition, limit argument, cited-result instantiation, object mapping, assumption discharge, boundary check, and target-assembly inference under the sections required by the appendix rules. Translate those obligations into the subsection in dependency order, while omitting audit wording such as dependency inventories, proof-flow summaries, sketch-row field labels, and reviewer-facing provenance. Keep this pass internal; do not add a public table or workflow label to the LaTeX bundle.
  • Do not sample representative steps, representative local units, or representative derivation blocks when building appendix coverage. The appendix coverage gate covers every used accepted step and every mathematical source unit in the required source sections.
  • A source unit is not preserved merely because its final conclusion appears. If the source unit contains a derivation, assumption check, parameter-dependence explanation, substitution, or bound, the appendix must include the corresponding proof text, displayed mathematics, and dependencies rather than only a theorem statement, citation, or reference to another result.
  • Use public mathematical names for visible appendix subsections and theorem-style titles. Do not put internal markers such as unit_001, unit 001, Step ID, target assembly, Target-Step Assembly, target claim, proof specification, or Cited Result Applications in visible public titles or proof prose; keep step/unit IDs only in stable labels.
  • Do not expose public appendix audit scaffolding in latex_template/*.tex. The public TeX must not contain visible labels or headings such as \emph{Source.}, Restated statement, Object mapping, Assumption discharge, Conclusion used, Local Result Applications, or Inputs and assumption checks. These checks may be performed internally, but public citations and dependency checks must be integrated into lemma, theorem, proposition, corollary statements and proof text inside proof environments.
  • Write the appendix directly from the accepted proof-step derivations, not from a checklist table. Every used local claim, hypothesis, invariant, lemma, proposition, theorem, corollary, cited-result application, and target-step assembly from the accepted proof-step files must become either a labeled public lemma, theorem, proposition, or corollary with full substantive proof/justification, or paper-facing proof text inside a proof environment in the appropriate appendix subsection. Translate target-step assembly as paper-facing concluding proof text inside a proof environment in that subsection unless it is a genuinely reusable mathematical bridge that deserves a separate theorem-style proposition. Do not omit local derivations from accepted proof steps when the omission would leave a gap in the appendix proof.
  • Use proof-obligation-preserving translation as the default for ## Local Derivation and ## Target-Step Assembly: keep the source proof's mathematical dependency order and carry over its displayed definitions, displayed equations, inequality chains, substitutions, constants, radius or envelope constructions, compactness or continuity arguments, recursion unrolling, induction or invariant transitions, case reasoning, boundary checks, cited-result object mappings, assumption-discharge steps, and final implication into paper-ready LaTeX.
  • Use source proof body first, then polish. For each used accepted step, draft the appendix subsection from the source proof body under ## Local Derivation, invoked ## Cited Result Applications, and ## Target-Step Assembly before tightening prose. Theorem-style environment count is not evidence of derivation preservation: the proof bodies themselves must carry the source equations, inequalities, constants, substitutions, induction steps, boundary cases, object mappings, and assumption discharges.
  • In latex_template/5_appendix.tex, once an accepted proof step is used in the final theorem proof, presume all proof-obligation content under that step's ## Local Derivation, ## Target-Step Assembly, and any ## Cited Result Applications invoked by those sections is needed. Proof-obligation content includes displayed equations, definitions, assumptions needed by the proof, inequalities, case checks, recursions, limits, constants, parameter dependence, object mappings, cited-result assumption checks, and target assembly reasoning. Audit packaging, status/provenance narration, sketch-row metadata, dependency inventories, exact duplicate setup, and non-mathematical repetition are not proof-obligation content and should not be emitted publicly.
  • A derivation-preserving appendix proof is not satisfied by matching the source unit with a theorem-style label and then citing other results in place of the source argument. When an accepted local unit or target-step assembly contains concrete mathematical work, the corresponding appendix proof must visibly include that work. Do not replace a long source derivation by follows from Lemma~\ref{...} or by Proposition~\ref{...} unless the source derivation itself contained only that citation and no additional proof work.
  • For each accepted proof_steps/<Step ID>/proof.md, translate the full substantive content of ## Local Derivation into that step's appendix subsection. Every local lemma, proposition, claim, theorem, corollary, hypothesis, or invariant that is used directly or transitively in the proof of the main theorem must appear publicly as a lemma, theorem, proposition, or corollary LaTeX environment with its statement and full proof or justification. Target-step assembly must appear as paper-facing proof text that explicitly derives the step conclusion from those results. The count of theorem-style environments is not enough: the proof-obligation content inside the accepted derivations must also appear.
  • Preserve full local derivations from step artifacts. Do not collapse long local proofs into a short summary, provenance note, accepted-step narration, or statement that the step was accepted. Translate definitions, inequalities, recursions, induction or invariant arguments, boundary cases, constants, parameter dependence, cited-result checks, object mappings, and assumption-discharge reasoning into paper-ready LaTeX.
  • Do not compact or summarize a local derivation for any theorem-style result used in the main theorem proof unless the omitted part is genuinely repetitive. Repetition compression is allowed only after one complete instance of the repeated derivation has been written; the abbreviated instance must cite the exact earlier displayed derivation and state precisely what substitutions or unchanged steps make the repetition valid. Distinct proof obligations, different boundary cases, different assumptions, or different cited-result discharges are not repetitions. Paper cleanup may delete workflow metadata, status/provenance narration, sketch-row field labels, dependency inventories, exact duplicate setup, and non-mathematical repetition. Non-mathematical repetition means repeated prose with no proof role; do not classify derivation paragraphs, equations, definitions, parameter-dependence explanations, cited-result mappings, assumption checks, or target-step assembly arguments as cleanup. When unsure, preserve the mathematical obligation in latex_template/5_appendix.tex but rewrite or omit the audit wording.
  • When translating local units into LaTeX theorem-style environments, make each statement self-contained: cite governing numbered assumptions as Assumption~\ref{assump:...} or Assumptions~\ref{assump:...}, name any accepted dependency result or earlier local theorem-style result it uses, list local conditions before the conclusion, and state the exact result proved. The proof may then cite prior results, but the reader must not need to inspect the proof body or surrounding prose to learn the statement's assumptions, conditions, or conclusion.
  • Translate each step artifact's ## Target-Step Assembly into the end of the corresponding appendix subsection as paper-facing proof text inside a proof environment, using \ref{...} to cite that subsection's local units and earlier appendix results. Do not emit copied sketch-row metadata or a boilerplate "assembled conclusion" proposition unless the target-step assembly contains a genuinely reusable mathematical bridge. Atomic steps still require a complete in-file proof of the target step claim.
  • Treat appendix subsections as navigation only, not proof authorities. Every step-level conclusion used outside its subsection must be stated as a named theorem-style result, usually a proposition, and later proofs must cite that result with \ref{...}; do not justify a proof by referring to "this subsection", "the previous subsection", a proof-step ID, or a local unit ID such as unit_001.
  • Write all public mathematical dependencies in paper-ready theorem-style form: Theorem~\ref{thm:...}, Lemma~\ref{lem:...}, Proposition~\ref{prop:...}, Corollary~\ref{cor:...}, or Assumption~\ref{assump:...}. Labels may include source step or local-unit IDs for traceability, but visible proof prose must not use subsection names, proof-step IDs, local unit IDs, Claim~, Hypothesis~, or Invariant~ as proof authority.
  • Include any cited-result restatements from ## Cited Result Applications that are invoked, cited, or used to supply object mappings, assumptions, or assumption-discharge checks for ## Local Derivation or ## Target-Step Assembly. Public external citations must use BibTeX-backed citation commands, while dependency-step and local-unit uses must be restated or referenced through in-bundle labels.
  • Translate ## Cited Result Applications into public proof content. For each nontrivial standard fact, theorem family, paper/book result, or named inequality used in a local derivation, either prove it inline or restate it in current notation with assumptions and a BibTeX-backed citation; never cite the internal section name or a vague "standard result" as public proof authority. Cited results must appear as integrated lemmas, theorems, propositions, corollaries, or proof text inside proof environments with citations inside the statement or proof, not as standalone audit blocks named Source, Restated statement, Object mapping, Assumption discharge, or Conclusion used.
  • Apply an internal per-step self-check immediately after drafting each appendix subsection: make a second source-order pass over that same step's source proof body, especially local derivations and target-step assembly. Repair the subsection before moving on if any source unit is missing, reordered in a way that hides a dependency, compressed into a shorter summary, converted into a citation-only proof, converted into a theorem-style statement without substantive proof, or replaced by a public reference to internal artifacts. Use source length only as an internal diagnostic trigger, never as an acceptance threshold.
  • End latex_template/5_appendix.tex with \subsection{Proof of the Main Theorem}, whose proof cites the exact earlier theorem-style results in the LaTeX bundle and performs only direct assembly reasoning.
  • Give every internally referenced section, assumption, theorem, lemma, proposition, corollary, and step-assembly result a unique stable ASCII \label{...}. Use conventional public prefixes such as sec:, assump:, thm:, lem:, prop:, cor:, and app:; include the source Step ID and local unit ID when labeling translated local units. Do not introduce public claim:, hyp:, or inv: labels except when preserving an existing nonpublic source handle inside a larger allowed public label.
  • Use \ref{...} for internal references to the main theorem, assumptions, and theorem-style results. Appendix subsection references may be used only for navigation, not as mathematical proof dependencies. Do not use citation commands for internal proof references.
  • Do not use workflow-only language in the LaTeX bundle: no branch-local file paths, no proof_steps/..., no review.md, no accepted step, no reviewer/provenance narration, and no instruction to inspect internal artifacts for proof content.
  • Fully instantiate the shared LaTeX template. The final public TeX bundle must not contain template placeholders or instructional filler such as Paper Title, Statement:, State the strongest rigorously supported theorem, Do not state a stronger target, If a readable public corollary, Use this proposition only, Verify every technical condition from the source theorem, Replace this placeholder, Give the full mathematical derivation, Name Or Goal Of The Step, Step ID: Step Goal, Local Lemma Title, Local Hypothesis Title, Each appendix subsection should, State the local, Translate the full local derivation, or placeholder reference/citation commands such as \ref{...}, \ref{assump:example}, or \citep{...}.
  • Public citations in the LaTeX bundle may refer to external papers or standard results only when the corresponding accepted step artifact already validated the statement, object mapping, and assumption discharge; restate the cited result in current notation before use.
  • For every external citation, use a LaTeX citation command such as \citep{...}, \citet{...}, or \cite{...} and ensure the cited key has a valid BibTeX entry in latex_template/reference.bib. If the source is not already in the template bibliography, add a complete entry with a stable ASCII key.
  • Do not mention an external source, author-year result, paper, book, or standard theorem family in public prose without a matching citation command and reference.bib entry.
  • If there are no external citation commands in the public TeX, keep reference.bib and ims.bst present for template consistency but suppress any visible empty bibliography section.
  • Place step proof derivations in the appendix subsections by default; do not replace them by an internal artifact reference.
  • If assembly_report.md ## Status is PARTIAL_BLOCKED, do not present the unresolved target as proved in public TeX; record the controlled blocker and smallest repair target in assembly_report.md.
  • Keep latex_template/ editable and paper-ready; do not add new claims, new assumptions, or unreviewed lemmas.

Step 5: Self-Check Before Finalizing

Before finalizing latex_template/, verify:

  • Artifact coverage: every required sketch step is accepted, used, or explicitly declared unnecessary with a reason.
  • Dependency closure: every dependency of each used accepted step is accepted and accounted for.
  • Source traceability: every theorem-level block is sourced from an accepted step artifact or direct assembly-only reasoning.
  • Claim preservation: accepted step statements, assumptions, and dependency meaning are not changed.
  • Structure: the LaTeX bundle contains a target theorem, named theorem-level blocks, and a proof of the target theorem.
  • Assembly closure: the target theorem proof cites the exact earlier theorem-style results it uses.
  • No unreviewed proof content: assembly introduces no independent lemma, inequality, assumption discharge, convergence upgrade, or stronger theorem-level claim.
  • Goal alignment: the attempted claim matches exactly what the assembled proof establishes.
  • Status honesty: assembly_report.md uses COMPLETE only when the formalized goal or valid target-spec instantiation is proved; otherwise it uses PARTIAL_BLOCKED.
  • Main theorem self-containedness: latex_template/3_main.tex can be read after 1_intro.tex and 2_preliminary.tex alone; any theorem-local constants are defined inline with explicit dependence; the theorem statement explicitly cites numbered assumptions as Assumption~\ref{assump:...} or Assumptions~\ref{assump:...}, states local conditions, and gives the conclusion; the theorem statement contains no forward references to appendix-local results, proof-step IDs, or appendix-only constants.
  • Assumption provenance: public theorem assumptions and preliminary admissibility definitions contain only primitive conditions unless the formalized goal is explicitly conditional; every derived invariant used in final assembly is proved by an accepted step, direct assembly consequence, or named appendix result.
  • Notation economy, notation provenance, derivation-over-notation, and constant provenance: public preliminaries define only stable notation explicitly derived from original setting quantities; the main theorem is not a long dictionary of helper constants; when notation and derivational detail conflict, the public proof uses fewer helper symbols and more visible derivation; heavy notation does not replace derivations needed to check bounds, finiteness, rates, dependence, cited-result assumption discharge, or implications; every constant, radius, threshold, rate, margin, admissibility parameter, bounded quantity, finite-tube quantity, event, or helper object is directly defined from the setting, explicitly stated as a theorem/admissibility condition, translated from a checked dependency/citation, or proved/bounded by a named local result.
  • Public-surface discipline: the main theorem uses only essential public-facing quantities; proof-local and appendix-local helper dictionaries stay in appendix results unless assembly proves they are essential to the public claim.
  • Main-theorem readability fallback: if latex_template/3_main.tex must retain a dense technical theorem with long admissibility dictionaries, it also includes a readable simplified theorem or corollary under domain-appropriate theorem-local simplifying assumptions that are explicitly stated and bridged; this fallback is insufficient if it merely points back to the unreadable dictionary without a concise public interface.
  • Explicit-rate contract: every public explicit rate declares exposed variables, hidden constants, fixed quantities, probability mode, horizon mode, and norm mode. Any simplified public rate has a complete Rate Specialization Bridge in latex_template/3_main.tex or a named appendix proposition cited from 3_main.tex; every dropped or absorbed term has an inequality proving absorption.
  • Baseline reduction: when a meaningful prior, simpler, or limiting regime is part of the proof context, the theorem, corollary, or bridge states how the result reduces to that baseline result, or states and justifies any conservative loss. Inherited theorem-facing baseline/recovery conclusions must be preserved rather than replaced by weaker surrogates.
  • Paper-readiness: latex_template/ has support files, numbered assumptions with \label{assump:...} targets matching the stable ids from setting.md and Assumption~\ref{assump:...} citations, meaningful preliminaries before the theorem, a main theorem section, a proof sketch, appendix subsections that may each contain multiple public lemma, theorem, proposition, or corollary units with proofs, a final appendix proof of the main theorem, BibTeX-backed external citations when external citations are used, internal \label{...}/\ref{...} pairs to theorem-style proof authorities, and no workflow-only proof references such as proof_steps/, review.md, accepted step, or instructions to inspect internal artifacts.
  • Public-TeX hygiene: visible public TeX has mathematical theorem titles rather than workflow titles, no malformed command fragments such as bare ef{...}, ref{...}, cite{...}, citep{...}, or citet{...} without a leading backslash, no unresolved references or citations after compilation when compilation logs are available, no duplicate labels, no internal section-name leakage such as Cited Result Applications, and no visible empty References section when no external citations are used. It also contains no public audit-scaffolding or sketch-row phrases such as \emph{Source.}, Restated statement, Object mapping, Assumption discharge, Conclusion used, Local Result Applications, Inputs and assumption checks, Intended claim:, Depends on:, Assumptions used:, Technical challenge:, Output target:, This result is used as follows, required assumptions are supplied, assembled conclusion, the the, or exact the.
  • Appendix full-derivation coverage: once an accepted proof step is used in the final theorem proof, all mathematical proof-obligation content under that step's ## Local Derivation, ## Target-Step Assembly, and invoked ## Cited Result Applications appears in latex_template/5_appendix.tex. Each local lemma, proposition, claim, theorem, corollary, hypothesis, or invariant used by the proof is converted into a public lemma, theorem, proposition, or corollary with statement and full substantive proof, or into complete proof text inside a proof environment where a separate statement is unnecessary; each accepted step artifact's target-step assembly is translated into paper-facing concluding proof text inside a proof environment in the same subsection. Do not omit local derivations from accepted proof steps when omission would leave a gap; no detailed local derivation may be replaced by a short summary, provenance note, accepted-step narration, citation-only proof, or "similar/routine" shortcut except under the explicit repetition rule. Matching theorem-style environment counts is not sufficient when the proof bodies have dropped source derivation content.
  • No representative-only appendix acceptance: assembly_report.md ## Status = COMPLETE requires the internal source-unit pass to account for all used accepted steps. Whole-proof-memory summaries, representative sampling, theorem-environment-count matching, and checking only that the conclusion appears are never evidence of preservation.
  • Appendix compression sanity: use the total source line count of used ## Local Derivation plus ## Target-Step Assembly sections only as a diagnostic trigger, not as an acceptance criterion or quota. A substantially shorter latex_template/5_appendix.tex is acceptable only after direct comparison with the accepted source derivations shows that the omitted text is workflow metadata, status/provenance narration, sketch-row metadata, dependency inventory, exact duplicate setup, non-mathematical repetition, or a genuinely repeated derivation handled under the explicit repetition rule. Complete journal-style proof detail must not remove definitions, displayed equations, inequalities, substitutions, recursions, compactness or continuity arguments, induction steps, case splits, boundary cases, constants, radius or envelope constructions, slack or margin checks, cited-result checks, object mappings, assumption-discharge reasoning, parameter-dependence explanations, or target-step assembly arguments. If the appendix omits such proof-obligation content, set assembly_report.md ## Status to PARTIAL_BLOCKED rather than presenting the bundle as complete.
  • If an appendix subsection is plainly much shorter than the corresponding source proof body, treat it as a blocker unless the shortened material is only workflow metadata, sketch-row metadata, dependency inventory, exact duplicate setup, non-mathematical repetition, or a repeated derivation already handled by the explicit repetition rule. Keep this check internal to assembly and review; do not add public audit tables, workflow status labels, or numeric-threshold language to the LaTeX bundle.
  • Template instantiation: latex_template/*.tex contain no shared-template placeholder title, placeholder text, placeholder subsection titles, placeholder theorem statements, or placeholder \ref{...}/citation commands.

Assembly Rules

  • Use ../_shared/templates/latex_template/ for the canonical LaTeX source files and support files.
  • Use ../_shared/templates/assembly-report.md for the controller-private assembly status artifact.
  • The LaTeX bundle must contain the exact setting and goal content from the corresponding # Formalized Setting and # Formalized Goal sections in setting.md.
  • The proof sketch section should summarize the accepted sketch without exposing workflow provenance as proof evidence.
  • assembly_report.md ## Status must use only COMPLETE or PARTIAL_BLOCKED.
  • The derivation must contain a target theorem, named theorem-level blocks corresponding to accepted steps, and assembly of the target theorem.
  • Each theorem-level block must preserve the accepted step claim, assumptions, and dependency meaning unless the controller routes back to step proof/review.
  • The target theorem proof must cite the exact earlier theorem-style blocks it uses.
  • Assembly-only reasoning may reconcile notation, combine accepted claims, or prove direct implications from accepted claims.
  • Assembly must not introduce a new independent nontrivial lemma, inequality, convergence-mode upgrade, assumption discharge, or theorem-level claim. If such a claim is needed, route back to /proof-sketch or /proof-step.
  • If a needed dependency, accepted-step derivation item, notation reconciliation, or final implication fails, set assembly_report.md ## Status to PARTIAL_BLOCKED and name the exact blocker.
  • In exact-goal mode, assembly_report.md ## Status = COMPLETE requires the final attempted claim to match the formalized goal.
  • In target-spec mode, assembly_report.md ## Status = COMPLETE requires an explicit concrete claim satisfying the target specification, including required parameter dependence.
  • For explicit-rate target-spec mode, assembly_report.md ## Status = COMPLETE also requires the Explicit Rate Contract and, when the public rate is simplified from a technical theorem, a Rate Specialization Bridge with auxiliary choices, technical condition verification, term absorption/simplification inequalities, probability conversion, and final hidden-constant dependence.
  • assembly_report.md ## Status = COMPLETE also requires the Assumption Provenance Contract: theorem-facing assumptions may not include unproved derived invariants unless the formalized goal is explicitly conditional.
  • The attempted claim must state exactly the strongest theorem-level claim supported by accepted step artifacts and direct assembly-only reasoning.
  • assembly_report.md blockers are required when ## Status = PARTIAL_BLOCKED and must name the exact failed assembly item and whether it requires /proof-assembly, /proof-step, or /proof-sketch.
  • The LaTeX bundle must present the same mathematical content in self-contained, paper-oriented LaTeX form and must not add stronger claims, new assumptions, or unreviewed lemmas.
  • latex_template/main.tex must remain the compile entry that inputs the five canonical content files; it uses reference.bib with ims.bst when external citations are present and suppresses a visible empty bibliography when they are not.
  • latex_template/main.tex, latex_template/arxiv.sty, latex_template/ims.bst, and latex_template/reference.bib must be present. reference.bib must contain every external citation key used in the LaTeX content.
  • latex_template/1_intro.tex must use numbered assumption environments for theorem-critical assumptions and preserve the stable assump:<slug> ids from setting.md as labels; latex_template/2_preliminary.tex must define only useful notation explicitly derived from original setting quantities and needed to state or read the main theorem, with proof-only shorthand, component radii, and one-off bookkeeping quantities left to the relevant local proof; latex_template/3_main.tex must state the main theorem compactly, and if the technical theorem remains dense it must add a readable simplified theorem or corollary under explicit theorem-local simplifying assumptions; latex_template/4_proof_sketch.tex must give only a public roadmap; latex_template/5_appendix.tex must place substantive derivations in appendix subsections named by accepted step names or goals, preserve complete journal-style proof detail from accepted local derivations, use only public lemma, theorem, proposition, corollary, and proof environments for theorem-style units, and end with \subsection{Proof of the Main Theorem}.
  • latex_template/3_main.tex must be theorem-statement self-contained and notation-economical: all notation and named constants in the theorem are defined in 1_intro.tex, 2_preliminary.tex, or inline inside the theorem statement before use, but proof-only helper dictionaries should be moved to appendix results. The theorem statement must not refer to appendix-local lemmas, propositions, claims, hypotheses, invariants, step assemblies, proof-step IDs, or constants introduced only after the theorem.
  • latex_template/3_main.tex must not present a simplified explicit rate as the public theorem unless it also includes a self-contained bridge proof there, or a short corollary that states the auxiliary choices and cites a named appendix Rate Specialization Bridge proposition. The public shape must make the bridge visible to a reader of the main theorem section.
  • Every theorem-style statement in latex_template/3_main.tex and latex_template/5_appendix.tex must be self-contained: it states the assumption basis with numbered Assumption~\ref{assump:...} references or named prior theorem-style results, states any local "if" conditions, and then states the "then" conclusion. Do not leave assumptions, regimes, parameter restrictions, or conclusions implicit in prose outside the environment.
  • Constants and bounded quantities in latex_template/ must not be free-floating. Each one must be visibly tied to an expression in original setting notation, a checked dependency/citation translation, an explicit theorem/admissibility condition, or a named proof result that establishes its bound or existence. If the object cannot be expressed from original setting notation, derive it rigorously before using it.
  • The main theorem, preliminaries, and final proof must not use named admissibility, good-event, regularity, stability, local-validity, recurrence, or membership packages to hide derived invariants as assumptions. Prove those facts first, or mark the assembly blocked.
  • Derivation-over-notation rule: prefer fewer helper symbols and more visible derivation when notation would obscure a proof obligation. Do not compress boundedness, finiteness, rate calculation, parameter dependence, implication, cited-result assumption discharge, or step-to-theorem assembly into a named constant or alias unless the supporting derivation is still present in the theorem statement or appendix proof.
  • latex_template/5_appendix.tex must contain a derivation-preserving LaTeX translation of every accepted proof step used in the proof of the main theorem. Use proof-obligation-preserving translation by default, preserving all mathematical proof-obligation content under each used step's ## Local Derivation, ## Target-Step Assembly, and any ## Cited Result Applications invoked by those sections. Mathematical proof-obligation content includes displayed equations, definitions, assumptions needed by the proof, inequalities, case checks, recursions, limits, constants, parameter dependence, object mappings, cited-result assumption checks, and target assembly reasoning. It may improve notation and exposition for paper readability, but appendix paper-readiness means complete journal-style proof detail, not concise summarization or copied audit prose. Paper readability may rephrase and format source material into theorem-style LaTeX, but it must not merge multiple source proof obligations into a shorter summary or preserve only representative examples. It must not omit substantive proof lines that the accepted step artifact needed for review. When unsure whether source material is proof content or cleanup, preserve the mathematical obligation in latex_template/5_appendix.tex but rewrite or omit the audit wording. Do not replace a derivation by "similarly", "routinely", "as above", citation-only prose, or "accepted in the step artifact" unless a complete prior derivation is present and the abbreviated repetition states the exact substitutions and unchanged arguments.
  • Internal proof references must use unique \label{...} and \ref{...} pairs pointing to public lemma, theorem, proposition, corollary results or numbered assumptions; assumption dependencies must be cited in prose as Assumption~\ref{assump:...} or Assumptions~\ref{assump:...}. Subsection references are allowed only for navigation and must not replace lemma/theorem/proposition/corollary references in proof arguments. External citations must use BibTeX-backed citation commands and entries in latex_template/reference.bib.
  • Every proof dependency in public TeX must name the referenced result type in prose, for example Lemma~\ref{lem:...} or Proposition~\ref{prop:...}. Do not write proof arguments that depend on a bare \ref{...}, an appendix subsection, "the previous subsection", a proof-step ID, or a local unit ID.
  • The LaTeX bundle must not rely on branch-local artifact paths, reviewer decisions, accepted-step narration, or workflow provenance as public proof evidence.
  • Visible public TeX must use paper-facing mathematical names, not workflow titles such as unit 001, target assembly, Target-Step Assembly, target claim, proof specification, or Cited Result Applications.
  • Visible public TeX must not use workflow, audit, sketch-row, or mechanical translation labels such as Proof ingredients, Local proof flow, Local result flow, \emph{Source.}, Restated statement, Object mapping, Assumption discharge, Conclusion used, Used by, Local Result Applications, Inputs and assumption checks, Intended claim:, Depends on:, Assumptions used:, Technical challenge:, Output target:, This result is used as follows, required assumptions are supplied, assembled conclusion, the the, or exact the. Integrate necessary mathematical details into statements and proofs instead, then do a final paper-facing prose cleanup pass.
  • Public TeX must not contain malformed command fragments such as bare ef{...}, ref{...}, cite{...}, citep{...}, or citet{...} without a leading backslash, duplicate labels, unresolved refs/citations after compilation, or a visible empty References section when no external citations are used.
  • The LaTeX bundle must not retain shared-template placeholder text such as Paper Title, Statement:, State the strongest rigorously supported theorem, Do not state a stronger target, If a readable public corollary, Use this proposition only, Verify every technical condition from the source theorem, Replace this placeholder, Give the full mathematical derivation, Name Or Goal Of The Step, Step ID: Step Goal, Local Lemma Title, Local Hypothesis Title, Each appendix subsection should, State the local, Translate the full local derivation, \ref{...}, \ref{assump:example}, or placeholder citation keys.
All versions