<< All versions
Skill v1.0.0
currentAutomated scan100/100dechenzhang/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.mdandproof_steps/<Step ID>/review.mdfor every required sketch step
Optional input:
- final
proof_review.mdwhen repairingPROOF_ASSEMBLY_FLAW
Outputs:
perspective_M/idea_N/latex_template/1_intro.texperspective_M/idea_N/latex_template/2_preliminary.texperspective_M/idea_N/latex_template/3_main.texperspective_M/idea_N/latex_template/4_proof_sketch.texperspective_M/idea_N/latex_template/5_appendix.texperspective_M/idea_N/latex_template/main.texperspective_M/idea_N/latex_template/arxiv.styperspective_M/idea_N/latex_template/ims.bstperspective_M/idea_N/latex_template/reference.bibperspective_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 forlatex_template/5_appendix.tex, not a condensed appendix summary. - Write
assembly_report.mdas the controller-private assembly status artifact. Do not put workflow status fields such as## Status,COMPLETE, orPARTIAL_BLOCKEDinto 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 stableassump:<slug>ids assigned to technical assumptions. - Read the accepted
proof_sketch.mdandproof_sketch_review.md. - Read every accepted
proof_steps/<Step ID>/proof.mdandproof_steps/<Step ID>/review.mdrequired 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_FLAWthat 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.mdfiles 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.texsubsection 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## StatustoCOMPLETEonly when the accepted step claims and direct assembly-only implications prove the formalized goal in a reviewable way. - In exact-goal mode,
COMPLETErequires the attempted claim to match the exact target claim fromsetting.md. - In target-spec mode,
COMPLETErequires 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## StatustoPARTIAL_BLOCKEDand 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## StatustoPARTIAL_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, andlatex_template/reference.bibfrom the shared template. Do not drop support files during repair. - Keep
latex_template/main.texas the compile entry using the five content files, style, and bibliography behavior. - Replace the placeholder title
Paper Titleinlatex_template/main.texwith a concise theorem-specific title derived fromsetting.mdor 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.texwith\section{Theoretical Setup}, the formalized setting, numbered theorem-criticalassumptionenvironments, and the formalized goal without raw markdown heading syntax. - Rewrite every theorem-critical setting assumption as a numbered
assumptionenvironment, visible as Assumption 1, Assumption 2, and so on, for example\begin{assumption}[Short name]\label{assump:smoothness} ... \end{assumption}. Use the stableassump:<slug>ids fromsetting.mdas the LaTeX labels, cite them later asAssumption~\ref{assump:...}orAssumptions~\ref{assump:...}, and do not rename them. Do not hide assumptions in prose or introduce new assumptions later. - Write
latex_template/2_preliminary.texwith\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## StatustoPARTIAL_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-localorappendix-localshould 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.texwith\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.textheorem statements and does not apply to proof bodies inlatex_template/5_appendix.tex. State the result using basic setting objects, numbered assumption references such asAssumption~\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.mdto 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.texwhose proof contains the bridge, or a short corollary inlatex_template/3_main.texthat 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.texandlatex_template/2_preliminary.tex: it may use only setting objects, numbered assumptions cited asAssumption~\ref{assump:...}orAssumptions~\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 asAssumption~\ref{assump:...}. - Write
latex_template/4_proof_sketch.texwith 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.texbeginning with\appendixand\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 publicclaim,hypothesis, orinvariantenvironments; 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.texcites an appendix Rate Specialization Bridge, write it as a named theorem-style proposition or corollary inlatex_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, orCited Result Applicationsin 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, orInputs 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 Derivationand## 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 Assemblybefore 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 Applicationsinvoked 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{...}orby 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 Derivationinto 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.texbut 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:...}orAssumptions~\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 Assemblyinto 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 asunit_001. - Write all public mathematical dependencies in paper-ready theorem-style form:
Theorem~\ref{thm:...},Lemma~\ref{lem:...},Proposition~\ref{prop:...},Corollary~\ref{cor:...}, orAssumption~\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~, orInvariant~as proof authority. - Include any cited-result restatements from
## Cited Result Applicationsthat are invoked, cited, or used to supply object mappings, assumptions, or assumption-discharge checks for## Local Derivationor## 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 Applicationsinto 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 namedSource,Restated statement,Object mapping,Assumption discharge, orConclusion 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.texwith\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 assec:,assump:,thm:,lem:,prop:,cor:, andapp:; include the sourceStep IDand local unit ID when labeling translated local units. Do not introduce publicclaim:,hyp:, orinv: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/..., noreview.md, noaccepted 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 inlatex_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.bibentry. - If there are no external citation commands in the public TeX, keep
reference.bibandims.bstpresent 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## StatusisPARTIAL_BLOCKED, do not present the unresolved target as proved in public TeX; record the controlled blocker and smallest repair target inassembly_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.mdusesCOMPLETEonly when the formalized goal or valid target-spec instantiation is proved; otherwise it usesPARTIAL_BLOCKED. - Main theorem self-containedness:
latex_template/3_main.texcan be read after1_intro.texand2_preliminary.texalone; any theorem-local constants are defined inline with explicit dependence; the theorem statement explicitly cites numbered assumptions asAssumption~\ref{assump:...}orAssumptions~\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.texmust 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.texor a named appendix proposition cited from3_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 fromsetting.mdandAssumption~\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 asproof_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{...}, orcitet{...}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 asCited 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, orexact 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 Applicationsappears inlatex_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 = COMPLETErequires 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 Derivationplus## Target-Step Assemblysections only as a diagnostic trigger, not as an acceptance criterion or quota. A substantially shorterlatex_template/5_appendix.texis 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, setassembly_report.md## StatustoPARTIAL_BLOCKEDrather 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/*.texcontain 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.mdfor the controller-private assembly status artifact. - The LaTeX bundle must contain the exact setting and goal content from the corresponding
# Formalized Settingand# Formalized Goalsections insetting.md. - The proof sketch section should summarize the accepted sketch without exposing workflow provenance as proof evidence.
assembly_report.md## Statusmust use onlyCOMPLETEorPARTIAL_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-sketchor/proof-step. - If a needed dependency, accepted-step derivation item, notation reconciliation, or final implication fails, set
assembly_report.md## StatustoPARTIAL_BLOCKEDand name the exact blocker. - In exact-goal mode,
assembly_report.md## Status = COMPLETErequires the final attempted claim to match the formalized goal. - In target-spec mode,
assembly_report.md## Status = COMPLETErequires an explicit concrete claim satisfying the target specification, including required parameter dependence. - For explicit-rate target-spec mode,
assembly_report.md## Status = COMPLETEalso 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 = COMPLETEalso 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.mdblockers are required when## Status = PARTIAL_BLOCKEDand 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.texmust remain the compile entry that inputs the five canonical content files; it usesreference.bibwithims.bstwhen 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, andlatex_template/reference.bibmust be present.reference.bibmust contain every external citation key used in the LaTeX content.latex_template/1_intro.texmust use numberedassumptionenvironments for theorem-critical assumptions and preserve the stableassump:<slug>ids fromsetting.mdas labels;latex_template/2_preliminary.texmust 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.texmust 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.texmust give only a public roadmap;latex_template/5_appendix.texmust 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.texmust be theorem-statement self-contained and notation-economical: all notation and named constants in the theorem are defined in1_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.texmust 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.texandlatex_template/5_appendix.texmust be self-contained: it states the assumption basis with numberedAssumption~\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.texmust 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 Applicationsinvoked 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 inlatex_template/5_appendix.texbut 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 asAssumption~\ref{assump:...}orAssumptions~\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 inlatex_template/reference.bib. - Every proof dependency in public TeX must name the referenced result type in prose, for example
Lemma~\ref{lem:...}orProposition~\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, orCited 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, orexact 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{...}, orcitet{...}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.