Referee-proofread and harden the Erdős 625 manuscript

[SamPetkov]

Purpose

This PR is a theorem-facing proof-closure pass over the self-contained Erdős 625 manuscript. It replaces the remaining compressed phase/root interfaces by auditable sources, makes the global second-moment exponent an explicit deterministic ledger, synchronizes the reader-facing proof guide with the actual dependency graph, and hardens both the source and PDF validation paths.

The theorem remains fail-closed. This PR does not claim that the full proof is complete or that only Lean remains. The new sources are complete candidate paper interfaces; they still require independent line-by-line mathematical review, exact theorem freezing, private Lean replay, and one integrated dependency audit. Accordingly, this PR remains a draft and \ErdosProofClosedfalse remains mandatory.

Sections 2–3: uniform phase and root geometry

Adds:

• 625/arxiv/SECTION2_PHASE_PACKAGE_V3.tex;
• 625/arxiv/SECTION3_ROOT_GEOMETRY_V3.tex.

Uniform phase package

The independence-number center is written exactly in natural-log coordinates,

q = log 2,
L = log n,
ell = log log n,
alpha = 2(L-ell+C)/q + b.

The phase expansion now has one deterministic uniform error

epsilon_n^ph = C_ph(1+ell^2)/L -> 0,

and the manuscript records

log mu_alpha
  = delta L
    + (2/q-1/2-delta)ell
    + K(delta)
    + E_n(delta),

sup_delta |E_n(delta)| <= epsilon_n^ph.

The exact adjacent-size ratios and the exact identity for 2^alpha yield uniform bounds for mu_{alpha+2} and mu_{alpha-2}. In particular,

mu_{alpha+2} =: epsilon_n^cap -> 0,
mu_{alpha-2} >= c n^2 (log n)^(2/q-5/2).

Thus Section 4 consumes a named independence-cap error rather than a separate anonymous o(1).

Finite dual and root package

The finite unrestricted support is now explicit:

S_+^(n) = {-1,0,...,alpha-1}.

The affine part of -log d_{alpha-i} cancels exactly at finite n under the fixed-mean constraint. The limiting Gaussian dual is introduced only after that exact cancellation.

Uniform convergence of the finite tilted partition functions, means, and variances is proved on one common compact tilt interval. Positivity of the limiting variance gives a uniform inverse-mean Lipschitz constant and the deterministic error

epsilon_n^dual
  = max_S sup_(T in K_*)
      (|F_{n,S}(T)-F_S(T)|
       + |lambda_{n,S}(T)-lambda_S(T)|)
  -> 0.

For the four-point support, the finite optimizer converges coordinatewise and remains uniformly bounded away from zero. The root corridor is proved by a literal sign change and strict monotonicity, and the class-count derivative is packaged as

epsilon_{n,A}^slope
  = sup |(log n)^(-2) d/dk(L_S+ck)-2/log 2|
  -> 0.

This supplies the exact positivity and uniformity needed by Sections 4 and 5.

Sections 4–5: lower tail and finite-target transport

SECTION4_CHROMATIC_LOWER_TAIL_V3.tex now makes explicit:

• the deterministic integer threshold k_chi^- = floor(r_+) - ceil(log n);
• the complete unordered-profile enumeration and all symmetry factors;
• the derivative-corridor check over the whole interval [k_chi^-,r_+];
• the strict event direction P(chi(G_n)>k_chi^-)->1;
• the full-sequence location precision |k_chi^--r_+|=o(n/(log n)^3).

SECTION5_ROOT_TRANSPORT_V3.tex starts from the exact finite identity

Phi_n(r_+) = r_+ {log 2-D_{4,n}(T_+(n))}

before transporting the target to T_0. It now defines

epsilon_n^target = |T_+(n)-T_0|,
omega_n^root
  = 2 epsilon_n^dual
    + 2 C_Lip epsilon_n^target
  -> 0.

The proof therefore identifies the source of the o(1) in the root displacement and proves r_4^co<r_+ before applying the mean-value theorem.

Section 7: complete candidate partial-diagonal package

The empty, central, and full ranges remain separate auditable sources:

• SECTION7_EMPTY_CORNER_V3.tex;
• SECTION7_CENTRAL_EXTRACTION_V3.tex;
• SECTION7_FULL_CORNER_V3.tex.

They return deterministic phase-independent errors

epsilon_n^empty -> 0,
epsilon_n^central -> 0,
epsilon_n^full -> 0.

The coordinate box is partitioned literally into disjoint and exhaustive empty, central, and full ranges. No boundary profile is omitted or counted twice. Their normalized output is

epsilon_n^pd
  = exp(epsilon_n^empty)-1
    + epsilon_n^central
    + epsilon_n^full
  -> 0,

sum_r D(r) <= 1+epsilon_n^pd.

This is a complete candidate manuscript proof of E625-11A–D, conditional on the exact midpoint-profile and positive-first-moment inputs. E625-11 remains needs review, not welded.

Sections 8–9: explicit global second-moment ledger

Adds 625/arxiv/SECTION9_EXPLICIT_GLOBAL_LEDGER_V3.tex.

The endpoint transport is recorded with the explicit row bound

sum_j Q_ij <= 1+3 tau_n^end.

The bare-skeleton sum is defined on the exact canonical high-skeleton domain and bounded by

BareSkeletonSum_n <= exp(Gamma_n^skel),

where

Gamma_n^skel
  = K log(1+(alpha+1)rho_16)
    + K log(1+3 tau_n^end)
    + log(1+epsilon_n^pd).

The three terms pay, respectively, the unique ambient deficit charge, endpoint transport, and partial-diagonal reference mass.

The conditioned residual estimate is packaged as

Gamma_n^att
  = max(C_att U^2,
        (log 2) U 2^(U/3)/2),

A(M,j) <= exp(Gamma_n^att).

This includes the zero-residual branch, the intrinsic regime, and the complementary regime. The normalized errors satisfy

epsilon_n^skel = (log n)^4 Gamma_n^skel/n -> 0,
epsilon_n^att  = (log n)^4 Gamma_n^att/n  -> 0.

The exact conditional decomposition then gives the theorem-facing seed exponent

Lambda_n = Gamma_n^skel + Gamma_n^att
         = o(n/(log n)^4),

1 <= E[Z^2]/E[Z]^2 <= exp(Lambda_n).

The two logarithmic ledgers have disjoint responsibilities. High-cell deficits and endpoint transportation occur only in Gamma_n^skel; residual local rewards and cycle-space contributions occur only in Gamma_n^att. No factor is charged twice.

Constant ledger and final adapter

The exact rational certificate remains

A_4(delta) > log(20000/12777)
           = log(1000/639)+log(12780/12777).

The final positive term is a fixed phase-independent slack that absorbs the deterministic final error while preserving the displayed theorem coefficient. The tangent correction changes only the four type multiplicities and preserves the fixed total class count. The simultaneous complement corollary carries the same coefficient without a second asymptotic loss.

Reader-facing and formalization-facing improvements

• The abstract and introduction now describe the named phase, dual, root, partial-diagonal, skeleton, and attachment errors.
• The proof guide follows the actual dependency chain from epsilon_n^ph through Lambda_n.
• FORMALIZATION_STATUS_ADDENDUM_2026_08_07_V3.tex records every new candidate interface as Needs review, gives the deterministic error chain, and specifies the recommended Lean theorem sequence.
• PHASE_ROOT_CLOSURE_AUDIT_2026-08-07.md and GLOBAL_SECOND_MOMENT_LEDGER_AUDIT_2026-08-07.md record the mathematical contracts and remaining review boundary.

Generator and validation hardening

The canonical manuscript source remains frozen. The theorem-facing wrapper

625/scripts/build_phase_root_self_contained_v3.py

invokes the canonical generator, replaces Sections 2–3 exactly once, and inserts the global second-moment ledger between Sections 9 and 10.

The existing generator was corrected so Section 4 and Section 5 replacements are required only in the source slices that actually contain them. The structural checker now validates the complete modular source set rather than relying on a stale monolithic prose proxy.

The checkers reject:

• source-marker drift;
• hidden control bytes;
• legacy ln or malformed log2 notation;
• duplicate semantic labels and equation tags;
• unbalanced TeX environments or braces;
• placeholders and compressed legacy passages;
• unresolved references or citations;
• duplicate Hyperref destinations;
• material overfull boxes;
• truncated or non-extractable PDFs.

Exact-head validation

Both final workflows completed successfully on head bbe1a9441d16364aad94d9fa547f6282594be62b:

• primary self-contained manuscript run 31214090275;
• independent theorem-facing package run 31214090236.

The final head passed:

• generator and replacement-marker replay;
• exact four-support rational ledger;
• exact partial-diagonal scalar ledger;
• the complete structural checker under ordinary Python and python -O;
• the theorem-facing package checker under ordinary Python and python -O;
• 45 guarded theorem-facing equation tags;
• 83 unique semantic labels;
• AMS/BibTeX compilation;
• unresolved-reference and unresolved-citation rejection;
• duplicate-PDF-destination rejection;
• material-overfull-box rejection;
• full-paper size and text-extractability gates;
• representative rendering and artifact upload.

Remaining proof-closure sequence

The remaining work is narrower, but still mathematical:

1. independently verify the new Sections 2–3 asymptotic algebra and finite-support dominated-convergence argument;
2. freeze and replay exact Lean theorems for the Section 4 lower-tail adapter and Section 5 finite-target root transport;
3. independently review and formalize the complete Section 7 three-range package;
4. replay the endpoint phase estimates and conditioned residual theorem against the welded private Section 8 finite chain;
5. formalize the explicit Gamma_n^skel, Gamma_n^att, and Lambda_n assembly on the exact skeleton domain;
6. regenerate the curated theorem-facing Lean root, run the axiom audit, and replay the final adapter on one integrated commit.

The manuscript now has a substantially more explicit and internally connected candidate proof. It is not yet publication-ready by verification alone, and presentation quality does not substitute for the remaining independent mathematical and formal replay.

[SamPetkov]

Updated readiness boundary after the theorem-facing closure pass

PR #58 has moved materially beyond the status recorded in the earlier readiness note. The manuscript now contains complete candidate paper interfaces for the phase/root package, chromatic lower tail, finite-target signed root transport, the three partial-diagonal ranges, and the global normalized second-moment ledger.

Newly explicit mathematical interfaces

1. Uniform phase and cap package. SECTION2_PHASE_PACKAGE_V3.tex defines a phase-uniform remainder epsilon_n^ph, proves the adjacent-size estimates, and exports the deterministic independence-cap error epsilon_n^cap.
2. Finite dual and root geometry. SECTION3_ROOT_GEOMETRY_V3.tex distinguishes the finite support S_+^(n) from its limiting support, proves exact finite affine cancellation, defines epsilon_n^dual, proves optimizer positivity, and exports the normalized slope error epsilon_{n,A}^slope.
3. Root transport. SECTION5_ROOT_TRANSPORT_V3.tex now uses the exact finite support loss and the explicit error

   omega_n^root
     = 2 epsilon_n^dual
       + 2 C_Lip epsilon_n^target.
   

4. Complete partial diagonals. The empty, central, and full ranges return deterministic errors and are assembled as a literal disjoint partition into epsilon_n^pd.
5. Global second moment. SECTION9_EXPLICIT_GLOBAL_LEDGER_V3.tex defines

   Lambda_n = Gamma_n^skel + Gamma_n^att
            = o(n/(log n)^4)
   

   on the exact canonical skeleton domain. Skeleton deficits and endpoint transport are paid only in Gamma_n^skel; residual local rewards and cycle space are paid only in Gamma_n^att.

Validation

Both final GitHub Actions workflows are green on head bbe1a9441d16364aad94d9fa547f6282594be62b:

• self-contained manuscript run 31214090275;
• independent theorem-facing package run 31214090236.

The final head passed ordinary and optimized structural replay, both exact rational ledgers, 45 guarded theorem-facing equation tags, 83 unique semantic labels, AMS/BibTeX compilation, unresolved-reference/citation rejection, duplicate-destination rejection, material-overfull-box rejection, full-paper size and extractability checks, and representative rendering.

Correct current boundary

The manuscript no longer lacks readable candidate arguments for E625-08 through E625-13. The remaining work is nevertheless genuine mathematical closure:

• independent line-by-line review of the new analytic interfaces;
• exact Lean theorem design with the same domains, constants, and quantifier order;
• replay of the Section 7 package and the explicit skeleton/attachment ledger against the welded private finite chain;
• one integrated theorem-facing root replay and axiom audit.

Thus the current statement is:

The candidate proof is substantially more complete, explicit, and internally connected, but it is not yet independently certified. PR #58 should remain a draft and \ErdosProofClosedfalse remains mandatory.