Re-audit the full Erdős 625 TeX and specify the corrected Version 2 proof

[SamPetkov]

Purpose

This draft PR performs a new mathematical pass over the entire canonical Erdős 625 TeX, from the phase expansion through the final probability intersection, while incorporating the later Section VIII--IX simplifications and theorem-upgrade work.

It is stacked on PR #43. It does not modify the frozen canonical TeX or claim that Erdos625Statement is proved.

Main verdict

The audit finds one remaining submission-blocking proof seam:

attained physical high skeletons
  <-> block support + deficits + local partial stub matchings,

together with the exact aggregate weight identity needed to sum that reindexing.

PR #41 has already closed the full-endpoint reference normalization and the decorated-to-physical injection. The missing theorem is the reverse/partial physical-fibre assembly and the global all-deficit comparison. Until that theorem is checked, Lemma 8.3, Proposition 9.2, and the final theorem remain conditional.

No second independent fatal gap was found in Sections 2--7 or 10--11, conditional on the normalized second moment. The old canonical Sections VIII--IX should nevertheless be replaced by the shorter aggregate all-deficit and q-only matching-restriction route.

Detailed TeX audit

625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md contains:

• a section-by-section GREEN/AMBER/RED/BLUE classification;
• exact diagnosis of the Section VIII physical-fibre seam;
• validation of the fixed-midpoint logic in Sections 2--7 and 10--11;
• the correct root-gap coefficient ledger;
• a source-level mathematical typo in equation (7.2):

  2^\ell_\bullet

  should be

  2^{\ell_\bullet};

• a replacement for the decimal central-rate check by the exact stronger certificate from PR Isolate verified Section 7 and Section 9 simplifications #30;
• a review of every proposed theorem extension in PR Document the full Erdős 625 theorem-upgrade and follow-up program #43.

Corrected Version 2 proof architecture

625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md gives copy-ready mathematics for the post-closure manuscript.

Main theorem

The phase-resolved statement should be

chi(G_n)-zeta(G_n)
  >= [ (ln 2)^2/8 * (ln 2-D_4(delta_n)) - o(1) ]
     * n/(ln n)^3

with high probability.

The stronger exact entropy certificate gives the uniform coefficient

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

which is about 6.68735 times the coefficient printed in the current candidate TeX.

The same theorem yields the simultaneous complement corollary

min{chi(G_n), chi(complement G_n)} - zeta(G_n)
  >= c n/(ln n)^3.

New Section VIII

For endpoint sizes m,m+d, deficit h, and actual multiplicity m-h, the exact aggregate local ratio is

R_{m,d}(h)
  = C(m,h)/((d+1)...(d+h)) * 2^(-hm+h(h+1)/2).

The one global denominator ratio is

(n)_{J+H}/(n)_J = (n-J)_H <= n^H.

After the missing finite reindexing is proved,

w(P,m-h)/w_full(P)
  <= product_e n^(h_e) R_{m_e,d_e}(h_e).

The high condition 2h<m gives

n^h R_{m,d}(h)
  <= (n m / 2^floor(2m/3))^h.

At the four-size phase,

rho_n = O((ln n)^(7/3)/n^(1/3)) = o(1),

and the all-deficit product plus endpoint transport gives

BareSkeletonSum
  <= exp(O(n^(2/3)(ln n)^(4/3)) + O(sqrt(n ln n)))
  = exp(o(n/(ln n)^4)).

This replaces the old near/middle split, E_mid, Xi_4, and the Section VIII residual-mass dichotomy.

New Section IX

Use injective restriction outside the exposed matching:

sum_even F product_{e in F\M} q_e
  <= product_{e notin M}(1+q_e).

Because the local increment is pointwise at most q, both residual products are charged to one total-q sum. The intrinsic and complementary regimes then give the literal aggregate theorem

AttachmentSum
  <= BareSkeletonSum * exp(epsilon_n n/(ln n)^4),
epsilon_n -> 0.

The canonical simple-cycle decomposition, residual walk kernel, mixed matching-cycle encoding, tau, and h tau are unnecessary in Version 2.

Corrections to the research program

625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md narrows four claims from PR #43.

1. Near-root placement: theta_n ln n -> infinity remains a proposed criterion until every use of the positive signed first-moment margin is replayed uniformly. theta_n=(ln n)^(-1/2) remains a plausible conservative target.
2. Balance stability: the binom(k,rho k) calculation proves stability inside the selected four-size witness family. Global necessity for arbitrary cocolorings requires an all-signed-profile first-moment exclusion theorem.
3. Slow support: the correct requirement is directly Lambda(n,m_n)=o(n/(ln n)^4). Writing Lambda=K(m)n/(ln n)^4 and requiring only K=o(ln n) is insufficient.
4. Cochromatic corridor: the current midpoint proof gives an upper location at (r_4^co+r_+)/2+o(H_n), not r_4^co+o(H_n). The latter is conditional on the near-root theorem.

Deterministic regression layer

625/experiments/full_tex_mathematical_reaudit.py checks under ordinary and optimized Python:

• the /32, /8, /4, and full-support coefficient ledger;
• the exact midpoint rounding inequality;
• the exact aggregate one-cell ratio over thousands of finite cases;
• the global falling-factorial identity and bound;
• the all-high two-thirds exponent budget;
• the geometric deficit-fibre majorant;
• binary-entropy imbalance penalties;
• the endpoint/all-high error scales relative to n/(ln n)^4;
• why K=o(ln n) does not fix an exponent of the form K n/(ln n)^4;
• known stale markers in the canonical TeX.

Files

• 625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md
• 625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md
• 625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md
• 625/experiments/full_tex_mathematical_reaudit.py
• .github/workflows/erdos625-full-tex-mathematical-reaudit.yml

Scope boundary

This PR is an audit and corrected rewrite specification. It does not prove:

• the reverse endpoint physical-fibre equivalence;
• the partial-cell physical-fibre cardinality;
• the global attained all-deficit reindexing;
• Lemma 8.3;
• Proposition 9.2;
• near-root placement;
• global balance necessity;
• the slow-support theorem;
• a matching O(n/(ln n)^3) upper bound;
• Erdos625Statement.

Keep this PR draft until the deterministic audit workflow is green and the RED/AMBER classifications have received independent mathematical review.

[SamPetkov]

Focused validation is green on commit d61a8f70557ea5ce75cbb0d24816c233ca8edb7e: Python compilation, ordinary execution, python -O, and the audit-coverage/classification checks all passed in workflow run 30206912030. The arithmetic regression includes 228,144 midpoint-rounding cases, exact aggregate high-cell ratios, global falling-factorial identities, the two-thirds exponent budget, geometric deficit sums, coefficient propagation, entropy imbalance penalties, and the slow-support scaling countercheck.

[SamPetkov]

Two final statement-hygiene improvements from the last pass: (i) formulate the phase-resolved theorem using an explicit deterministic sequence epsilon_n -> 0 rather than an unbound o(1) inside the probability threshold; (ii) formulate the tunable amplifier tail for a deterministic sequence r_n>0 (usually r_n -> infinity for a whp consequence), not merely a fixed symbol r, and state whether the accompanying o(1) is uniform in that choice. These do not alter the proof architecture.