Make the Erdős 625 manuscript self-contained and verification-safe

[SamPetkov]

Purpose

This PR is stacked on PR #56 and upgrades the 13-page AMS proof synopsis into a generated, self-contained manuscript draft. It is not another prose-only roadmap. The complete canonical Sections 1–7 and 10 are imported deterministically from the frozen TeX, Sections 8–9 are replaced by the audited simplified route, Section 11 is replaced by the phase-resolved constant ledger, and Appendix A records the exact private Lean frontier and publication gates.

The canonical 625/arxiv/main.tex remains frozen. The new draft is compiled in verification mode by default and cannot silently present the still-incomplete top-level proof as closed.

Main changes

Visible theorem status

AMS_SELF_CONTAINED_DRAFT_V3.tex defines

\newif\ifErdosProofClosed
\ErdosProofClosedfalse

The default PDF contains an explicit verification banner, an audit-safe abstract, and a conditional target theorem. Publication mode may be enabled only after the checklist in Appendix A is green on one integrated commit.

Complete manuscript generation

625/scripts/build_self_contained_ams_v3.py verifies the exact Git-blob SHA of the frozen canonical TeX and extracts the complete Sections 1–7 and 10 by semantic section markers. It converts the legacy ruled statement boxes to the ordinary amsthm hierarchy, normalizes notation and mathematical English, and inserts the new Sections 8, 9, and 11.

The generator fails closed if the canonical source changes. The resulting PDF is a full paper rather than an introduction plus two replacement sections.

Definitions and proof-object dictionary

The manuscript now defines before use:

• cocoloring and cochromatic number;
• signed cocoloring witness;
• falling factorial conventions;
• profiles and overlap tables;
• the configuration matching;
• physical partial matchings;
• block supports;
• support graph, even subgraph, and binary cycle rank;
• canonical high cells, deficits, endpoint tables, bare skeletons, and residual attachments.

It explicitly separates the three meanings of “matching” and explains why the positive-support matching hypothesis is necessary for cellwise factorization.

Canonical Section VIII route

The earlier prose mixed two valid finite routes. The main proof now uses the coarse common charge

rho_16 = sum_(i,j) rho_ij

and the finite factor

(1 + (alpha+1) rho_16)^K.

This is the route consumed by the canonical private finite reduction and requires only rho_16 <= 1. The sharper table-preserving product

product_(i,j) (1 + 2 rho_ij)^(L_ij)

is retained as a separate stronger corollary.

The new Section VIII supplies complete statements and proofs for:

1. the completion-free physical-fiber aggregate;
2. the exact one-cell deficit ratio;
3. the single global falling-factorial loss;
4. the optional-deficit product;
5. the coarse local deficit sum;
6. unweighted and weighted realized-table regrouping;
7. square-free endpoint transport and multinomial summation;
8. the coarse phase corridor and rho_16 = O(log n / n^(1/4));
9. the bare-skeleton estimate.

The previous sentence asserting that endpoint transportation “absorbs” the remaining factor has been replaced by a named proposition with the actual formulas and proof.

Self-contained q-only Section IX

The residual section now defines theta_ab, Delta_x, lambda_ab, and q_ab explicitly and proves:

• the exact conditional attachment decomposition;
• the fixed-even-set threshold expansion;
• injectivity of deletion outside the exposed matching;
• the restriction-product bound;
• lambda_ab <= q_ab;
• the one-total-q attachment envelope;
• the intrinsic O(U^2) regime;
• the complementary residual-size regime;
• the uniform attachment error;
• the normalized signed second moment.

The legacy simple-cycle, walk-kernel, mixed-cycle, and tau calculations do not appear in the main exposition.

Stronger theorem ledger

The final section first states the phase-resolved coefficient

(log 2)^2/8 * (log 2 - D_4(delta_n)),

then records the exact four-support certificate

D_4(delta) < log(639/500),
log 2 - D_4(delta) > log(1000/639),

and obtains

(log 2)^2/8 * log(1000/639)
  = 0.026896409808379...

The /8 factor is justified directly from the /4 root separation and midpoint placement; no additional fixed halving is inserted.

Formalization appendix

Appendix A maps manuscript results to exact private Lean declarations and distinguishes welded, running, needs review, and blocked.

It records that:

• the Section VIII finite chain through the realized-table deficit sum is welded privately;
• the coarse phase corridor is welded;
• eventually_fourEndpointThreeQuarterRho_le_one has one approved running request and is not yet proof evidence;
• the concrete phase/chromatic-tail package, signed first-moment assembly, complete partial-diagonal asymptotics, and global final attachment assembly remain open.

It also proposes a small theorem-facing Lean root and recommends splitting the remaining broad DAG nodes before further proof search.

Files

625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex
625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex
625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex
625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex
625/arxiv/SECTION8_SELF_CONTAINED_V3.tex
625/arxiv/SECTION9_SELF_CONTAINED_V3.tex
625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex
625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex
625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex
625/scripts/build_self_contained_ams_v3.py
625/experiments/check_self_contained_manuscript_v3.py
625/audits/SELF_CONTAINED_BULLETPROOF_MANUSCRIPT_PASS_2026-08-04.md
.github/workflows/erdos625-self-contained-manuscript.yml

Validation

The dedicated workflow:

• verifies the frozen canonical source SHA;
• generates the complete manuscript body;
• runs fail-closed structural checks under ordinary and optimized Python;
• checks unique labels, balanced environments, visible status language, and required proof-object definitions;
• rejects synopsis-only transition phrases and unresolved placeholders;
• compiles the complete AMS manuscript with BibTeX;
• rejects undefined references and citations;
• rejects material overfull boxes;
• requires at least 30 pages and 15,000 extracted words;
• uploads the complete PDF, generated TeX body, log, and representative renders.

A green TeX workflow validates the manuscript assembly and editorial invariants. It does not promote the remaining mathematical or Lean proof obligations.

Scope boundary

This PR does not change the canonical theorem status, merge private proof branches, or assert that Erdős Problem 625 has been formally closed. It creates the self-contained, expert-facing manuscript that should become canonical only after the exact Appendix A publication gates are satisfied.

[SamPetkov]

Final validation record

Validated head:

13ed9a966ae60f6819f4d88f87a6d5281f9db300

Workflow run 30913278550 passed both jobs:

• fail-closed structural checker under ordinary Python;
• the same checker under python -O;
• frozen canonical Git-blob verification;
• complete body generation;
• full amsart/BibTeX/latexmk compilation;
• no undefined references or citations;
• no overfull box wider than 5 pt;
• 39-page PDF;
• 18,252 extracted words;
• representative first/last-page rendering;
• complete artifact upload.

Independent artifact inspection:

PDF SHA-256:
e756451599bb9e1b35a4f8be89d45e7debd68d0870018cfc9c843fae07e2c8ad

The first page, dense Section VIII and IX pages, formalization appendix, and final references were rendered and inspected. No clipping, overlap, black box, broken glyph, or unresolved layout defect was observed.

The publication switch remains disabled. This validates the manuscript assembly and auditability; it does not promote the still-open mathematical or Lean gates.