Fuse endpoint transport and sharpen the seed exponent

[SamPetkov]

Purpose

This stacked draft PR builds on PR #58 and targets genuine mathematical simplifications in the Section 8--9 second-moment argument. It removes two avoidable losses, reduces the number of theorem interfaces needed for Lean, and derives a sharper quantitative seed bound.

The random variable, four-size profile, canonical high-cell decomposition, main theorem, and displayed coefficient are unchanged. The publication gate remains fail-closed and \ErdosProofClosedfalse remains mandatory.

Result 1: type-preserving deficit summation

The coarse ledger forgets endpoint type, bounds every deficit by rho_16, counts up to alpha+1 possible deficits, and only later performs endpoint transport. This introduces an artificial factor alpha+1.

For endpoint type (i,j), define

B_ij = 1/(1-rho_ij).

The local geometric sum gives

sum_{h: m-h high} w(P,m-h)
  <= w_full(P) product_{e in P} B_type(e).

After weighted regrouping by the realized endpoint table L,

BareSkeletonSum_n <= sum_L W(L) B^L.

Result 2: a single fused 4 x 4 kernel

Define

Qtilde_ij = B_ij Q_ij,
Sigma_n   = max_i sum_j Qtilde_ij.

Multiplying the square-free endpoint inequality by (B^L)^2, followed by one arithmetic--geometric mean step and one multinomial sum, gives

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

This single proposition replaces the separate alpha+1 deficit count, support-cardinality loss, unweighted table regrouping, and endpoint row-sum estimate.

Using the exact phase formula,

rho_16 = O((log n)^(5/2)/sqrt(n)),
Sigma_n = 1+O((log n)^(5/2)/sqrt(n)),

so

Gamma_skel^sharp
  = O(sqrt(n) (log n)^(3/2)).

The previous coarse deficit contribution was O(n^(3/4) log n).

Result 3: fixed-buffer critical-quarter residual split

The previous residual proof splits at m_0=2^(U/3). The exponent 1/3 is convenient but not structural. The endpoint reward has quadratic exponent U^2/8, so the critical exponential scale is 2^(U/4).

This PR uses the explicit threshold

T_U = 64 U 2^(U/4).

If m_0>=T_U, then

theta_ab <= (eU/64)2^(-U/4).

For R=floor(U/2), log-convexity reduces the higher activity to the two endpoint terms. The full endpoint uses

binom(R,2)-U(R-2)/4 <= R/2,
U <= (7/3)R,
log_2(R!) >= R log_2 R-R log_2 e.

With 1<log_2 e<3/2 and 1<log_2(7/3)<5/4, its logarithm is at most

7-5R/4-log_2 R,

which is negative for R>=6. Hence

q_ab <= C theta_ab^2,
A(M,j) <= exp(CU^2).

If m_0<T_U, the existing crude estimate gives

A(M,j)
  <= exp(32 (log 2) U^2 2^(U/4)).

Therefore

Gamma_att^sharp
  = O(sqrt(n) (log n)^(3/2)).

This improves the previous complementary order O(n^(2/3)(log n)^(1/3)).

Quantitative seed corollary

Combining the exact conditioned decomposition with the two sharpened exponents yields a fixed C_sharp such that

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

P(Z>0)
  >= exp(-C_sharp sqrt(n) (log n)^(3/2)).

This is strictly stronger than the o(n/(log n)^4) exponent required by the existing amplifier and does not alter the final theorem coefficient.

Files

• 625/arxiv/SECTION9_SHARPENED_TRANSPORT_ATTACHMENT_V4.tex
• 625/experiments/check_sharpened_transport_attachment_v4.py
• 625/audits/FUSED_TRANSPORT_CRITICAL_QUARTER_AUDIT_2026-08-10.md
• 625/scripts/build_phase_root_self_contained_v3.py

The generator inserts the refinement after the explicit Section 9 ledger and before rare-event amplification. It executes the new checker before manuscript assembly.

Fail-closed checks

The checker verifies:

• source hygiene, balanced TeX, unique labels, and the complete tag range (9.43)--(9.57);
• the exact cancellation binom(R,2)-U(R-2)/4 <= R/2 for 8<=U<=4096;
• both endpoint ratios at theta=(eU/64)2^(-U/4) for 12<=U<=4096;
• the exponent arithmetic for the fused skeleton and critical-quarter attachment;
• normal and optimized-Python replay through both manuscript validation paths.

The finite sweep is a regression check, not a replacement for the analytic factorial argument.

Verification boundary

This is a candidate strengthening, not a welded proof claim. Promotion still requires independent line-by-line review, replay against the private welded Section 8 chain, exact Lean declarations with the same finite domains and quantifier order, and the final axiom/dependency audit.

[SamPetkov]

Final exact-head validation

Final head: 8d04a88889932fd7c7182ad7a73c8f14040f1ac9.

Both independent workflows completed successfully:

• self-contained manuscript run 31362257655;
• theorem-facing package run 31362257662.

The final head passed:

• the sharpened transport/attachment checker under ordinary and optimized Python;
• the exact cancellation ledger through U=4096;
• both existing exact rational ledgers;
• both structural manuscript replay paths;
• full AMS/BibTeX compilation in both workflows;
• 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 final candidate bound on this branch is

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

with the corresponding Paley--Zygmund seed lower bound. The PR remains a draft because integrated private Lean replay and independent mathematical review are still required.