Remove the midpoint loss in the Erdős 625 gap

[SamPetkov]

Purpose

This stacked draft PR builds on PR #59 and turns the earlier near-root research target into a concrete theorem-facing candidate. The previous manuscript placed the signed four-size profile at the midpoint between the signed and ordinary first-moment roots, retaining one half of the leading root separation. This PR shows that the midpoint margin is substantially stronger than the proof consumes.

The replacement profile is

k_co = ceil(r_4^co)+1.

Its distance from the signed real root lies in [1,2). The uniform root slope therefore gives a signed first-moment exponent of order (log n)^2. That margin is sufficient for both actual consumers in the partial-diagonal proof, so the full leading root separation is retained.

The random variable, four-size support, exact overlap identity, fused endpoint kernel, critical-quarter residual estimate, and final entropy certificate are unchanged. The publication switch remains fail-closed.

New result 1: a one-part-buffer profile

Let

d_n = k_co-r_4^co.

Then exactly

1 <= d_n < 2.

Since r_4^co,k_co=Theta(n/log n), every intermediate point satisfies

|n/k-n/r_4^co| = O((log n)^2/n)
               = o(log log n/log n).

Thus the complete segment remains in the common slope corridor. Integrating

d/dk [L_{S_4}(n,k)+(log 2)k]
  = (2/log 2)(log n)^2+O(log n log log n)

over a displacement in [1,2) gives

Phi_n(k_co)=Theta((log n)^2).

After the existing exact tangent correction and Stirling extraction, the integer profile satisfies

log E Z_k^sgn = Theta((log n)^2)

uniformly across the complete phase.

New result 2: the smaller first moment is sufficient

The audit identifies only two load-bearing uses of the midpoint first-moment margin.

Central partial diagonals

The affine extraction uses (log E Z)/k_co. At the one-part profile,

(log E Z)/k_co
  = O((log n)^3/n)
  = o(1),

so the same phase-uniform bound on the affine profile term follows.

Full corner

The reverse recurrence gives B(h)<=1, hence

D(k-h) <= 1/E Z <= exp(-c(log n)^2).

There are at most (k_co+1)^4 residual profiles, so

sum_full D(k-h)
  <= (k_co+1)^4 exp(-c(log n)^2)
  = o(1).

The logarithm of the profile count is only O(log n). The empty corner, central rate, endpoint transport, and residual attachment require only the same root corridor, coordinate positivity, and k_i=Theta(n/log n).

New result 3: full leading root separation

The chromatic lower threshold satisfies

k_chi^- = r_+ + O(log n),

while the new signed profile satisfies

k_co = r_4^co + O(1).

Therefore

k_chi^- - k_co
  = [(log 2)^2 A_4(delta_n)/4+o(1)] n/(log n)^3.

The former midpoint factor 1/2 disappears.

New result 4: explicit amplification loss

PR #59 gives

E[Z^2]/E[Z]^2
  <= exp(C_sharp sqrt(n)(log n)^(3/2)).

Using this seed exponent in the arbitrary-seed amplifier with r_n=log n adds

O(n^(3/4)(log n)^(-1/4))
  = o(n/(log n)^3)

classes, with failure probability tending to zero. Thus amplification consumes none of the leading root coefficient.

Quantitative strengthening

The exact certificate remains

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

The candidate uniform coefficient becomes

((log 2)^2/4) log(1000/639)
  = 0.053792819616758...

and the stronger pre-slack coefficient is

((log 2)^2/4) log(20000/12777)
  = 0.053821018526027...

The first number is exactly twice the midpoint coefficient in PR #58.

Formal simplification

The near-root interface removes the midpoint selector and the theorem propagating exactly half the root gap. The proposed exact formal spine is:

1. 1 <= ceil(x)+1-x < 2;
2. a bounded class-count displacement stays in the root corridor;
3. integrate the existing slope estimate over [1,2);
4. reuse finite optimizer positivity and tangent rounding;
5. replace the full-corner denominator by exp(-c(log n)^2);
6. consume the sharpened PR Fuse endpoint transport and sharpen the seed exponent #59 seed exponent in the final amplifier.

Files

• 625/arxiv/AMS_NEAR_ROOT_DRAFT_V4.tex
• 625/arxiv/FRONTMATTER_INTRODUCTION_NEAR_ROOT_V4.tex
• 625/arxiv/PROOF_ARCHITECTURE_NEAR_ROOT_V4.tex
• 625/arxiv/SECTION5_NEAR_ROOT_PROFILE_V4.tex
• 625/arxiv/SECTION7_FULL_CORNER_NEAR_ROOT_V4.tex
• 625/arxiv/FINAL_ASSEMBLY_NEAR_ROOT_V4.tex
• 625/arxiv/FORMALIZATION_STATUS_NEAR_ROOT_ADDENDUM_2026_08_11_V4.tex
• 625/scripts/build_near_root_self_contained_v4.py
• 625/experiments/check_near_root_full_gap_v4.py
• 625/audits/NEAR_ROOT_FULL_GAP_AUDIT_2026-08-11.md
• .github/workflows/erdos625-near-root-full-gap.yml

The Version 3/PR #59 manuscript remains unchanged as a verified fallback. The V4 wrapper invokes that generator and replaces only the profile-placement block, the full-corner adapter, and the final assembly.

Pre-PR checks

Before opening the PR, the new sources passed:

• isolated AMS compilation of the complete new source set;
• balanced TeX environment and brace checks;
• hidden-control and logarithm-notation scans;
• exact rational regression of 1 <= ceil(x)+1-x < 2 on more than 100,000 rational inputs;
• exact exponent arithmetic for the amplification loss;
• numerical coefficient and fixed-slack regression;
• Python bytecode compilation;
• workflow YAML parsing.

The dedicated PR workflow now performs the integrated exact-head build and replays the PR #59 sharpened checker under ordinary and optimized Python.

Verification boundary

This is a candidate strengthening, not a proof-closure declaration. Promotion still requires independent line-by-line mathematical review, exact Lean statements with the same ceiling convention and quantifier order, replay of the revised full corner against the exact complementary identity, integrated replay of the fused skeleton and attachment packages at the same integer profile, and the final axiom/dependency audit.

\ErdosProofClosedfalse remains mandatory.

[SamPetkov]

Final exact-head validation

Final head: f89e643ca8f4a431526b0fd50af991a03be0b3cb.

Dedicated workflow run 31478569323 completed successfully in both jobs:

• structural-replay;
• build-complete-pdf.

The exact head passed:

• the inherited PR Fuse endpoint transport and sharpen the seed exponent #59 fused-kernel and critical-quarter checker under ordinary and optimized Python;
• the near-root checker under ordinary and optimized Python;
• 100,100 exact rational ceiling cases verifying 1 <= ceil(x)+1-x < 2;
• the central-range normalization ledger and the revised full-corner domination;
• the amplification monomial calculation O(n^(3/4)(log n)^(-1/4));
• exact coefficient and fixed-slack regression;
• full 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.

The generated V4 manuscript has 57 pages and 26,308 extracted words. The manuscript artifact is erdos625-near-root-manuscript-v4 (artifact ID 9096311323).

The candidate strengthened statement on this branch is

chi(G_n)-zeta(G_n)
  >= ((log 2)^2/4) log(1000/639) n/(log n)^3

with coefficient

0.053792819616758...

The stronger pre-slack certificate is 0.053821018526027....

The PR remains a draft and fail-closed. The one-part-buffer slope integration, revised full corner, and full-coefficient adapter still require independent mathematical review and exact private Lean replay before promotion.