Kernel-check the Section 8 endpoint transport core

.github/workflows/erdos625-section8-endpoint-transport-core.yml

@@ -0,0 +1,51 @@
+name: Erdős 625 Section 8 endpoint transport core
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section8EndpointTransportCore.lean"
+      - "625/formalization/SECTION8_ENDPOINT_TRANSPORT_CORE_AUDIT.md"
+      - ".github/workflows/erdos625-section8-endpoint-transport-core.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in the new module
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section8EndpointTransportCore.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the module and dependency closure warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section8EndpointTransportCore --wfail \
+            > /tmp/section8-endpoint-lean.log 2>&1
+          status=$?
+          tail -n 240 /tmp/section8-endpoint-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section8-endpoint-transport-lean-log
+          path: /tmp/section8-endpoint-lean.log
+          if-no-files-found: ignore

625/formalization/Erdos625/Section8EndpointTransportCore.lean

@@ -0,0 +1,272 @@
+import Erdos625.Section8EndpointGlobalTransport
+import Erdos625.Section8EndpointLocalCellFactor
+import Mathlib.Tactic
+
+/-!
+# Section VIII: square-root-free endpoint transportation core
+
+This module isolates the exact finite algebra behind manuscript Lemma 8.1.
+The displayed geometric-mean estimate contains square roots and several
+factorial quotients.  Before introducing those divisions, its load-bearing
+content can be written as a denominator-free squared inequality.
+
+The module proves:
+
+* the exact local cell identity relating one endpoint factor to the two
+  diagonal endpoint factors;
+* the corresponding product identity over an arbitrary four-type endpoint
+  table;
+* the global falling-factorial transport in `ENNReal`;
+* their combined square-root-free transportation inequality.
+
+No asymptotic estimate for `Q_ij`, margin summation, near-cell decoration, or
+Section VIII skeleton bound is asserted here.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- The denominator-free local transport factor
+`(t)_d 2^(d s + choose(d,2))` for an endpoint cell. -/
+def fourEndpointLocalTransportDen
+    (alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) : ENNReal :=
+  ((fourEndpointUpperSize alpha hAlpha i j).descFactorial
+      (fourEndpointDistance i j) : ENNReal) *
+    (2 : ENNReal) ^
+      (fourEndpointDistance i j * fourEndpointLowerSize alpha hAlpha i j +
+        (fourEndpointDistance i j).choose 2)
+
+/-- The square of the local binomial choice in the endpoint comparison. -/
+def fourEndpointLocalChooseSquare
+    (alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) : ENNReal :=
+  (Nat.choose (fourEndpointUpperSize alpha hAlpha i j)
+    (fourEndpointDistance i j) : ENNReal) ^ 2
+
+/-- Product of the local transport denominators over a four-type table. -/
+def fourEndpointLocalTransportDenProduct
+    (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : ENNReal :=
+  ∏ i, ∏ j, (fourEndpointLocalTransportDen alpha hAlpha i j) ^ L.toFun i j
+
+/-- Product of the squared local binomial choices over a four-type table. -/
+def fourEndpointLocalChooseSquareProduct
+    (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : ENNReal :=
+  ∏ i, ∏ j, (fourEndpointLocalChooseSquare alpha hAlpha i j) ^ L.toFun i j
+
+/-- Exact square-root-free local identity behind the `Q_ij` factor in (8.8). -/
+theorem fourEndpointLocalCellFactor_sq_mul_transportDen
+    (alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha)
+    (i j : Fin 4) :
+    fourEndpointLocalCellFactor alpha hAlpha i j ^ 2 *
+        fourEndpointLocalTransportDen alpha hAlpha i j =
+      fourEndpointSizeDiagonalFactor (fourEndpointSize alpha hAlpha i) *
+        fourEndpointSizeDiagonalFactor (fourEndpointSize alpha hAlpha j) *
+          fourEndpointLocalChooseSquare alpha hAlpha i j := by
+  have hle (x y : Fin 4)
+      (hxy : fourEndpointSize alpha hAlpha x ≤
+        fourEndpointSize alpha hAlpha y) :
+      fourEndpointLocalCellFactor alpha hAlpha x y ^ 2 *
+          fourEndpointLocalTransportDen alpha hAlpha x y =
+        fourEndpointSizeDiagonalFactor (fourEndpointSize alpha hAlpha x) *
+          fourEndpointSizeDiagonalFactor (fourEndpointSize alpha hAlpha y) *
+            fourEndpointLocalChooseSquare alpha hAlpha x y := by
+    rw [fourEndpointLocalCellFactor_eq_lowerDiagonal_mul_choose]
+    unfold fourEndpointLocalTransportDen fourEndpointLocalChooseSquare
+      fourEndpointLowerSize fourEndpointUpperSize
+    rw [min_eq_left hxy, max_eq_right hxy]
+    rw [fourEndpointSizeDiagonalFactor_ratio alpha hAlpha hHigh x y hxy]
+    ring
+  by_cases hij : fourEndpointSize alpha hAlpha i ≤
+      fourEndpointSize alpha hAlpha j
+  · exact hle i j hij
+  · have hji : fourEndpointSize alpha hAlpha j ≤
+        fourEndpointSize alpha hAlpha i := le_of_not_ge hij
+    have h := hle j i hji
+    simpa [fourEndpointLocalCellFactor, fourEndpointOverlapSize,
+      fourEndpointLocalTransportDen, fourEndpointLocalChooseSquare,
+      fourEndpointLowerSize, fourEndpointUpperSize, fourEndpointDistance,
+      Nat.dist_comm, min_comm, max_comm, mul_comm, mul_left_comm, mul_assoc] using h
+
+/-- The local identities multiply exactly over every cell of a four-type
+endpoint table.  The row and column diagonal products appear with the literal
+endpoint margins. -/
+theorem fourEndpointLocalProduct_sq_mul_transportDenProduct
+    (alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha)
+    (L : FourEndpointFullTable) :
+    fourEndpointLocalProduct alpha hAlpha L ^ 2 *
+        fourEndpointLocalTransportDenProduct alpha hAlpha L =
+      fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun i => fourEndpointRowMargin L i) *
+        fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun j => fourEndpointColumnMargin L j) *
+        fourEndpointLocalChooseSquareProduct alpha hAlpha L := by
+  have hsq :
+      (∏ i, ∏ j,
+          (fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j) ^ 2 =
+        ∏ i, ∏ j,
+          ((fourEndpointLocalCellFactor alpha hAlpha i j) ^ 2) ^ L.toFun i j := by
+    calc
+      (∏ i, ∏ j,
+          (fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j) ^ 2 =
+        ∏ i, (∏ j,
+          (fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j) ^ 2 :=
+        (Finset.prod_pow Finset.univ 2 (fun i =>
+          ∏ j, (fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j)).symm
+      _ = ∏ i, ∏ j,
+          ((fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j) ^ 2 := by
+        apply Finset.prod_congr rfl
+        intro i _
+        exact (Finset.prod_pow Finset.univ 2 (fun j =>
+          (fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j)).symm
+      _ = ∏ i, ∏ j,
+          ((fourEndpointLocalCellFactor alpha hAlpha i j) ^ 2) ^ L.toFun i j := by
+        apply Finset.prod_congr rfl
+        intro i _
+        apply Finset.prod_congr rfl
+        intro j _
+        simp only [← pow_mul, Nat.mul_comm]
+  have hrow :
+      (∏ i, ∏ j,
+          (fourEndpointSizeDiagonalFactor
+            (fourEndpointSize alpha hAlpha i)) ^ L.toFun i j) =
+        fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun i => fourEndpointRowMargin L i) := by
+    unfold fourEndpointDiagonalLocalProduct
+    apply Finset.prod_congr rfl
+    intro i _
+    simpa [fourEndpointRowMargin, fourEndpointDiagonalLocalFactor,
+      fourEndpointSizeDiagonalFactor] using
+      (Finset.prod_pow_eq_pow_sum Finset.univ (L.toFun i)
+        (fourEndpointSizeDiagonalFactor
+          (fourEndpointSize alpha hAlpha i)))
+  have hcol :
+      (∏ i, ∏ j,
+          (fourEndpointSizeDiagonalFactor
+            (fourEndpointSize alpha hAlpha j)) ^ L.toFun i j) =
+        fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun j => fourEndpointColumnMargin L j) := by
+    unfold fourEndpointDiagonalLocalProduct
+    rw [Finset.prod_comm]
+    apply Finset.prod_congr rfl
+    intro j _
+    simpa [fourEndpointColumnMargin, fourEndpointDiagonalLocalFactor,
+      fourEndpointSizeDiagonalFactor] using
+      (Finset.prod_pow_eq_pow_sum Finset.univ
+        (fun i => L.toFun i j)
+        (fourEndpointSizeDiagonalFactor
+          (fourEndpointSize alpha hAlpha j)))
+  unfold fourEndpointLocalProduct fourEndpointLocalTransportDenProduct
+    fourEndpointLocalChooseSquareProduct
+  calc
+    (∏ i, ∏ j,
+        (fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j) ^ 2 *
+        (∏ i, ∏ j,
+          (fourEndpointLocalTransportDen alpha hAlpha i j) ^ L.toFun i j) =
+      ∏ i, ∏ j,
+        ((fourEndpointLocalCellFactor alpha hAlpha i j) ^ 2 *
+          fourEndpointLocalTransportDen alpha hAlpha i j) ^ L.toFun i j := by
+        rw [hsq, ← Finset.prod_mul_distrib]
+        apply Finset.prod_congr rfl
+        intro i _
+        rw [← Finset.prod_mul_distrib]
+        apply Finset.prod_congr rfl
+        intro j _
+        rw [mul_pow]
+    _ = ∏ i, ∏ j,
+        (fourEndpointSizeDiagonalFactor (fourEndpointSize alpha hAlpha i) *
+          fourEndpointSizeDiagonalFactor (fourEndpointSize alpha hAlpha j) *
+          fourEndpointLocalChooseSquare alpha hAlpha i j) ^ L.toFun i j := by
+        apply Finset.prod_congr rfl
+        intro i _
+        apply Finset.prod_congr rfl
+        intro j _
+        rw [fourEndpointLocalCellFactor_sq_mul_transportDen
+          alpha hAlpha hHigh i j]
+    _ = (∏ i, ∏ j,
+          (fourEndpointSizeDiagonalFactor
+            (fourEndpointSize alpha hAlpha i)) ^ L.toFun i j) *
+        (∏ i, ∏ j,
+          (fourEndpointSizeDiagonalFactor
+            (fourEndpointSize alpha hAlpha j)) ^ L.toFun i j) *
+        (∏ i, ∏ j,
+          (fourEndpointLocalChooseSquare alpha hAlpha i j) ^ L.toFun i j) := by
+        simp only [mul_pow, Finset.prod_mul_distrib, mul_assoc]
+    _ = fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun i => fourEndpointRowMargin L i) *
+        fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun j => fourEndpointColumnMargin L j) *
+        (∏ i, ∏ j,
+          (fourEndpointLocalChooseSquare alpha hAlpha i j) ^ L.toFun i j) := by
+        rw [hrow, hcol]
+
+/-- `ENNReal` form of the global falling-factorial transport (8.12). -/
+theorem fourEndpoint_global_transport_ennreal
+    (n alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) :
+    (n.descFactorial (fourEndpointRowMass alpha hAlpha L) : ENNReal) *
+        (n.descFactorial (fourEndpointColumnMass alpha hAlpha L) : ENNReal) ≤
+      ((n.descFactorial (fourEndpointJ alpha hAlpha L) : ENNReal) ^ 2) *
+        (n + 1 : ENNReal) ^ fourEndpointDisplacement L := by
+  exact_mod_cast fourEndpoint_global_transport n alpha hAlpha L
+
+/-- Combined denominator-free squared form of the endpoint transportation
+comparison.  This is the finite algebraic core of manuscript (8.8), before
+introducing square roots or cancelling positive factorial denominators. -/
+theorem fourEndpoint_squareFree_transport
+    (n alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha)
+    (L : FourEndpointFullTable) :
+    ((n.descFactorial (fourEndpointRowMass alpha hAlpha L) : ENNReal) *
+      (n.descFactorial (fourEndpointColumnMass alpha hAlpha L) : ENNReal)) *
+      (fourEndpointLocalProduct alpha hAlpha L ^ 2 *
+        fourEndpointLocalTransportDenProduct alpha hAlpha L) ≤
+    (((n.descFactorial (fourEndpointJ alpha hAlpha L) : ENNReal) ^ 2) *
+      (n + 1 : ENNReal) ^ fourEndpointDisplacement L) *
+      (fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun i => fourEndpointRowMargin L i) *
+        fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun j => fourEndpointColumnMargin L j) *
+        fourEndpointLocalChooseSquareProduct alpha hAlpha L) := by
+  let A : ENNReal :=
+    (n.descFactorial (fourEndpointRowMass alpha hAlpha L) : ENNReal) *
+      (n.descFactorial (fourEndpointColumnMass alpha hAlpha L) : ENNReal)
+  let B : ENNReal :=
+    ((n.descFactorial (fourEndpointJ alpha hAlpha L) : ENNReal) ^ 2) *
+      (n + 1 : ENNReal) ^ fourEndpointDisplacement L
+  let C : ENNReal :=
+    fourEndpointLocalProduct alpha hAlpha L ^ 2 *
+      fourEndpointLocalTransportDenProduct alpha hAlpha L
+  have hAB : A ≤ B := by
+    simpa only [A, B] using
+      fourEndpoint_global_transport_ennreal n alpha hAlpha L
+  calc
+    A * C = C * A := mul_comm _ _
+    _ ≤ C * B := by
+      simpa [mul_comm] using (mul_le_mul_left hAB C)
+    _ = B * C := mul_comm _ _
+    _ = B *
+      (fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun i => fourEndpointRowMargin L i) *
+        fourEndpointDiagonalLocalProduct alpha hAlpha
+          (fun j => fourEndpointColumnMargin L j) *
+        fourEndpointLocalChooseSquareProduct alpha hAlpha L) := by
+      rw [show C =
+        fourEndpointDiagonalLocalProduct alpha hAlpha
+            (fun i => fourEndpointRowMargin L i) *
+          fourEndpointDiagonalLocalProduct alpha hAlpha
+            (fun j => fourEndpointColumnMargin L j) *
+          fourEndpointLocalChooseSquareProduct alpha hAlpha L by
+        simpa only [C] using
+          fourEndpointLocalProduct_sq_mul_transportDenProduct
+            alpha hAlpha hHigh L]
+
+#print axioms fourEndpointLocalCellFactor_sq_mul_transportDen
+#print axioms fourEndpointLocalProduct_sq_mul_transportDenProduct
+#print axioms fourEndpoint_global_transport_ennreal
+#print axioms fourEndpoint_squareFree_transport
+
+end
+
+end Erdos625

625/formalization/SECTION8_ENDPOINT_TRANSPORT_CORE_AUDIT.md

@@ -0,0 +1,72 @@
+# Audit: Section VIII square-root-free endpoint transport core
+
+## Purpose
+
+`Erdos625/Section8EndpointTransportCore.lean` isolates the finite algebraic core
+of manuscript Lemma 8.1.  The manuscript states a geometric-mean inequality
+with square roots and quotient factors.  The new module first proves a
+cross-multiplied squared form, where every factor is finite and no cancellation
+of a possibly zero descending factorial is required.
+
+## New declarations
+
+- `fourEndpointLocalTransportDen`:
+  the exact local factor
+  `(t)_d 2^(d s + choose(d,2))`;
+- `fourEndpointLocalChooseSquare`:
+  the squared binomial choice `choose(t,d)^2`;
+- `fourEndpointLocalCellFactor_sq_mul_transportDen`:
+  the exact one-cell identity;
+- `fourEndpointLocalProduct_sq_mul_transportDenProduct`:
+  multiplication of the local identities over an arbitrary four-type table;
+- `fourEndpoint_global_transport_ennreal`:
+  the accepted global falling-factorial transport cast to `ENNReal`;
+- `fourEndpoint_squareFree_transport`:
+  the combined denominator-free squared endpoint transportation inequality.
+
+## Relation to manuscript (8.8)
+
+For sizes `s <= t=s+d`, the local identity is
+
+\[
+  \bigl(s!g(s)\binom td\bigr)^2
+  \bigl((t)_d2^{ds+\binom d2}\bigr)
+  =
+  \bigl(s!g(s)\bigr)\bigl(t!g(t)\bigr)\binom td^2.
+\]
+
+After multiplication over cells, the diagonal factors collect according to the
+row and column margins.  The accepted falling-factorial theorem supplies
+
+\[
+ (n)_{m_r}(n)_{m_c}
+ \le (n)_{J(L)}^2(n+1)^{\sum |i-j|\ell_{ij}}.
+\]
+
+Their combination is precisely the load-bearing algebra below the square-root
+form of (8.8).  A later theorem may divide by the positive factorial factors
+and take square roots on the feasible domain.
+
+## Trust and validation
+
+The focused workflow:
+
+- rejects placeholders and project-defined axioms/constants;
+- builds the pinned Lean 4.31/mathlib project with `--wfail`;
+- compiles the module directly with warnings fatal.
+
+The module prints the axioms of each public theorem.  The ordinary repository
+Lean workflow also runs.
+
+## Scope boundary
+
+This PR does not yet prove the complete Lemma 8.1 as printed.  It deliberately
+does not:
+
+- cancel the cell-factorial or descending-factorial denominators;
+- introduce the real square roots in the geometric-mean statement;
+- prove the asymptotic bound `Q_ij <= eta_n^d/d!`;
+- perform the Cauchy--multinomial margin summation of Lemma 8.2;
+- address near or middle high cells from Lemma 8.3.
+
+It closes the exact endpoint-transport algebra on which those later steps rely.