Simplify Sections 8 and 9 to endpoint AM--GM, all deficits, and q-only residuals

[SamPetkov]

Summary

This is a stacked review follow-up to PR #36. It develops a shorter replacement route for manuscript Sections 8 and 9. No canonical manuscript, PDF, or theorem statement is changed.

The proposed architecture is:

1. endpoint transport in square-free form;
2. square-free AM--GM linearization and one-sided multinomial sums;
3. one geometric expansion for every high deficit;
4. q-only residual attachment by matching restriction;
5. the intrinsic finite residual dichotomy 2^U <= m^3 versus its complement.

Section 8 simplification I: AM--GM instead of Cauchy

From

W(L) <= sqrt(D(r) A_L * D(c) C_L) * Q^L,

use termwise AM--GM:

W(L) <= (D(r) A_L + D(c) C_L) * Q^L / 2.

Each half is summed by dropping only one family of margin constraints and applying the multinomial theorem. This yields directly

sum_L W(L)
  <= (1 + C eta_n)^k_co * sum_r D(r),

removing the table-family Cauchy inequality, (sum sqrt D)^2, and the polynomial margin-count loss.

Section8SquareFreeAMGM.lean isolates the ordered-real implication

x^2 <= y z  ->  2x <= y+z

and its weighted version, so the formal endpoint route does not need to introduce square roots.

Section 8 simplification II: one all-high-deficit sum

A high multiplicity j=m-e satisfies 2e<m. The formalization-first exponent budget is

e * floor(2m/3) <= e*m - e*(e+1)/2.

Consequently

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

Uniformly over the four endpoint sizes,

rho_n = O((log n)^(7/3) / n^(1/3)) = o(1).

All high multiplicities are summed by one geometric series. Their total cost is

exp(O(n^(2/3) * (log n)^(4/3)))
  = exp(o(n/(log n)^4)).

This removes the near/middle split, N(S), E_mid(S), Xi_4, and the residual large/small split from Section 8. Section 8 becomes a purely exposed-skeleton calculation.

Section 9 simplification

The concise replacement records PR #37's q-only route:

A(M,j) <= exp(2 * sum q_e) <= exp(C U^2)

in the intrinsic regime 2^U <= m^3, with the complementary exact bound

m < 2^ceil(U/3)

when that regime fails.

Files

• 625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
• 625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md
• 625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md
• 625/formalization/Erdos625/Section8SquareFreeAMGM.lean
• 625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
• 625/formalization/Erdos625/Section8SimplificationCore.lean
• 625/experiments/sections8_9_simplification_check.py
• .github/workflows/erdos625-sections8-9-simplification-check.yml

Finite formal targets

The simplification core is intended to prove:

• square-free AM--GM linearization, including a weighted form;
• every strict high multiplicity is above half of its own endpoint size;
• its deficit satisfies 2e<m;
• the all-high deficit window is exact in both directions;
• endpoint subtraction/restoration is exact and injective;
• the two-thirds binary exponent budget.

Exact verification

The standard-library checker uses exact Fraction arithmetic and explicit exceptions under python -O. It verifies:

• 89,700 high-deficit exponent cases;
• 70,800 exact local-ratio instances;
• 90,000 exact square-free AM--GM instances;
• 44,100 exact q-absorption instances;
• diagnostic phase scans from n=10^10 through 10^200.

The phase scans are diagnostics, not substitutes for the manuscript's phase asymptotics.

Validation status and scope boundary

The latest focused workflow builds the aggregate Section8SimplificationCore under Lean 4.31 and --wfail; current jobs are queued. Keep this PR draft until that run is green.

Before canonical replacement, independent review must still verify:

1. the linear endpoint inequality through the exact physical/type-table quotient;
2. the full-range local geometric ratio bound in the repository's ENNReal language;
3. the physical endpoint-decoration bijection and global product assembly;
4. the complementary Section 9 phase-asymptotic adapter.

PR #36 supplies the square-free endpoint transport core; PR #37 supplies the q-only attained-profile residual route.