Kernel-check the Section 8 endpoint transport core

[SamPetkov]

Summary

This PR attacks the remaining Section VIII boundary directly. It formalizes the exact, square-root-free algebra beneath the geometric-mean transportation comparison in manuscript Lemma 8.1.

No canonical manuscript, PDF, or theorem statement is changed.

Files

• 625/formalization/Erdos625/Section8EndpointTransportCore.lean
• 625/formalization/SECTION8_ENDPOINT_TRANSPORT_CORE_AUDIT.md
• .github/workflows/erdos625-section8-endpoint-transport-core.yml

Main results

For a cell joining endpoint sizes s <= t=s+d, the module proves the exact identity

(local endpoint factor)^2
  * ((t)_d * 2^(d*s + choose(d,2)))
=
(diagonal factor at s)
  * (diagonal factor at t)
  * choose(t,d)^2.

It then multiplies this identity over an arbitrary four-type endpoint table, where the diagonal factors collect according to the literal row and column margins.

The accepted global falling-factorial transport is cast to ENNReal and combined with the local product identity. The result is fourEndpoint_squareFree_transport, a denominator-free squared form of the load-bearing inequality behind manuscript (8.8).

Why this form

The printed geometric-mean comparison contains square roots and factorial quotients. Cancelling those factors before their feasible-domain positivity has been stated creates avoidable formal risk. The cross-multiplied squared theorem is total, includes endpoint cases, and records the exact algebra needed for the later square-root theorem.

Validation

The focused workflow rejects placeholders/project axioms, builds the pinned Lean 4.31/mathlib project with --wfail, and compiles the module directly with warnings fatal. The full repository Lean workflow also runs.

Scope boundary

This PR does not yet:

• divide by the positive factorial factors and take square roots;
• prove the numerical/asymptotic bound on Q_ij in (8.9);
• perform the Cauchy--multinomial table summation in Lemma 8.2;
• handle the near and middle high-cell ranges in Lemma 8.3;
• prove the complete Section VIII skeleton estimate or Erdos625Statement.

It is intended as the exact finite endpoint-transport core for the next Section VIII integration step.

[SamPetkov]

Validation result: PASS within the stated endpoint-transport scope on head f702b646ad7fd88f63e294b905286f2a6a8cbbc1.

The following checks are green:

• placeholder/project-axiom rejection;
• focused warning-fatal build of Erdos625.Section8EndpointTransportCore and its dependency closure;
• full repository Lean 4.31 build with --wfail;
• generated self-contained source freshness;
• warning-fatal compilation of Erdos625SelfContained.lean;
• arXiv artifact synchronization and publication verification.

The final compiler iterations changed only proof orientation/definitional normalization. The theorem statements were not weakened. This PR kernel-checks the denominator-free squared endpoint-transport algebra beneath manuscript (8.8); it does not claim the later square-root/cancellation step, Lemma 8.2, Lemma 8.3, or the global Section VIII sum.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: f702b646ad

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Import this module from the accepted-project root

The new module is not imported by 625/formalization/Erdos625.lean (nor by AxiomAudit.lean). Consequently, clients using the canonical import Erdos625 cannot access any of these declarations, and generate_self_contained.py excludes the entire module because it follows the root's transitive import closure; the generated checkpoint and its freshness/compilation gates therefore continue to pass without containing or checking these claimed public results. Add the root and audit imports and regenerate Erdos625SelfContained.lean.

Useful? React with 👍 / 👎.

[SamPetkov]

Follow-up simplification: PR #38 builds on this square-free transport core. It replaces the table-family Cauchy step by termwise AM--GM and proposes one all-high-deficit geometric expansion, removing the near/middle split and the Section 8 residual model. The concise replacement draft and exact/Lean audit boundary are included there; #36 remains the independently reviewable finite transport layer.