From bb9f88e5f3ec4e76410fce30cacd39103e22d973 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 07:56:15 +0300
Subject: [PATCH 1/9] Add square-root-free Section 8 endpoint transport core

---
 .../Section8EndpointTransportCore.lean        | 245 ++++++++++++++++++
 1 file changed, 245 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section8EndpointTransportCore.lean

diff --git a/625/formalization/Erdos625/Section8EndpointTransportCore.lean b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
new file mode 100644
index 00000000..9d6590b6
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
@@ -0,0 +1,245 @@
+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
+    rw [Finset.prod_pow]
+    apply Finset.prod_congr rfl
+    intro i _
+    rw [Finset.prod_pow]
+    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] 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] 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
+  calc
+    ((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) *
+        (fourEndpointLocalProduct alpha hAlpha L ^ 2 *
+          fourEndpointLocalTransportDenProduct alpha hAlpha L) :=
+      mul_le_mul_right
+        (fourEndpoint_global_transport_ennreal n 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
+      rw [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

From 1f97a2b2796fea485ab2e8b2ebf24ed117fa9c37 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 07:56:35 +0300
Subject: [PATCH 2/9] Document the Section 8 transport core

---
 .../SECTION8_ENDPOINT_TRANSPORT_CORE_AUDIT.md | 72 +++++++++++++++++++
 1 file changed, 72 insertions(+)
 create mode 100644 625/formalization/SECTION8_ENDPOINT_TRANSPORT_CORE_AUDIT.md

diff --git a/625/formalization/SECTION8_ENDPOINT_TRANSPORT_CORE_AUDIT.md b/625/formalization/SECTION8_ENDPOINT_TRANSPORT_CORE_AUDIT.md
new file mode 100644
index 00000000..9892fca1
--- /dev/null
+++ b/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.

From 36792b912872763782ebd04e542eb819c510f367 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 07:56:48 +0300
Subject: [PATCH 3/9] Add focused Lean gate for Section 8 endpoint transport

---
 ...os625-section8-endpoint-transport-core.yml | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 .github/workflows/erdos625-section8-endpoint-transport-core.yml

diff --git a/.github/workflows/erdos625-section8-endpoint-transport-core.yml b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
new file mode 100644
index 00000000..bb770f38
--- /dev/null
+++ b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
@@ -0,0 +1,42 @@
+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: true
+          build-args: --wfail
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Compile the module warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          lake env lean -DwarningAsError=true \
+            Erdos625/Section8EndpointTransportCore.lean \
+            -o .lake/build/lib/lean/Erdos625/Section8EndpointTransportCore.olean

From 660900ed7c21c36281f05860fd3917a1c96f8113 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:00:49 +0300
Subject: [PATCH 4/9] Expose Section 8 compiler tail

---
 .../erdos625-section8-endpoint-transport-core.yml          | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/erdos625-section8-endpoint-transport-core.yml b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
index bb770f38..67955665 100644
--- a/.github/workflows/erdos625-section8-endpoint-transport-core.yml
+++ b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
@@ -37,6 +37,11 @@ jobs:
         working-directory: 625/formalization
         shell: bash
         run: |
+          set +e
           lake env lean -DwarningAsError=true \
             Erdos625/Section8EndpointTransportCore.lean \
-            -o .lake/build/lib/lean/Erdos625/Section8EndpointTransportCore.olean
+            -o .lake/build/lib/lean/Erdos625/Section8EndpointTransportCore.olean \
+            > /tmp/section8-endpoint-lean.log 2>&1
+          status=$?
+          tail -n 240 /tmp/section8-endpoint-lean.log
+          exit $status

From 8b5ba99976515813fd24bb884f969f53caed8e21 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:02:00 +0300
Subject: [PATCH 5/9] Use targeted Section 8 dependency closure

---
 .../erdos625-section8-endpoint-transport-core.yml        | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/erdos625-section8-endpoint-transport-core.yml b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
index 67955665..d8dbebfc 100644
--- a/.github/workflows/erdos625-section8-endpoint-transport-core.yml
+++ b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
@@ -28,19 +28,16 @@ jobs:
         with:
           lake-package-directory: 625/formalization
           auto-config: false
-          build: true
-          build-args: --wfail
+          build: false
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Compile the module warning-fatally
+      - name: Build the module and dependency closure warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake env lean -DwarningAsError=true \
-            Erdos625/Section8EndpointTransportCore.lean \
-            -o .lake/build/lib/lean/Erdos625/Section8EndpointTransportCore.olean \
+          lake build Erdos625.Section8EndpointTransportCore --wfail \
             > /tmp/section8-endpoint-lean.log 2>&1
           status=$?
           tail -n 240 /tmp/section8-endpoint-lean.log

From 879a7ccbd220ae63c7c412a73c7a26950bd85dbf Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:07:17 +0300
Subject: [PATCH 6/9] Upload the focused Section 8 compiler log

---
 .../erdos625-section8-endpoint-transport-core.yml          | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/workflows/erdos625-section8-endpoint-transport-core.yml b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
index d8dbebfc..2083be59 100644
--- a/.github/workflows/erdos625-section8-endpoint-transport-core.yml
+++ b/.github/workflows/erdos625-section8-endpoint-transport-core.yml
@@ -42,3 +42,10 @@ jobs:
           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

From 8b30be94a7b40838f3faf81abc32c2f7cea8681b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:12:53 +0300
Subject: [PATCH 7/9] Repair the endpoint transport product assembly

---
 .../Section8EndpointTransportCore.lean        | 42 +++++++++++++------
 1 file changed, 30 insertions(+), 12 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointTransportCore.lean b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
index 9d6590b6..e66b4050 100644
--- a/625/formalization/Erdos625/Section8EndpointTransportCore.lean
+++ b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
@@ -109,13 +109,26 @@ theorem fourEndpointLocalProduct_sq_mul_transportDenProduct
           (fourEndpointLocalCellFactor alpha hAlpha i j) ^ L.toFun i j) ^ 2 =
         ∏ i, ∏ j,
           ((fourEndpointLocalCellFactor alpha hAlpha i j) ^ 2) ^ L.toFun i j := by
-    rw [Finset.prod_pow]
-    apply Finset.prod_congr rfl
-    intro i _
-    rw [Finset.prod_pow]
-    apply Finset.prod_congr rfl
-    intro j _
-    simp only [← pow_mul, Nat.mul_comm]
+    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)
+      _ = ∏ 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)
+      _ = ∏ 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
@@ -125,7 +138,8 @@ theorem fourEndpointLocalProduct_sq_mul_transportDenProduct
     unfold fourEndpointDiagonalLocalProduct
     apply Finset.prod_congr rfl
     intro i _
-    simpa [fourEndpointRowMargin] using
+    simpa [fourEndpointRowMargin, fourEndpointDiagonalLocalFactor,
+      fourEndpointSizeDiagonalFactor] using
       (Finset.prod_pow_eq_pow_sum Finset.univ (L.toFun i)
         (fourEndpointSizeDiagonalFactor
           (fourEndpointSize alpha hAlpha i)))
@@ -139,7 +153,8 @@ theorem fourEndpointLocalProduct_sq_mul_transportDenProduct
     rw [Finset.prod_comm]
     apply Finset.prod_congr rfl
     intro j _
-    simpa [fourEndpointColumnMargin] using
+    simpa [fourEndpointColumnMargin, fourEndpointDiagonalLocalFactor,
+      fourEndpointSizeDiagonalFactor] using
       (Finset.prod_pow_eq_pow_sum Finset.univ
         (fun i => L.toFun i j)
         (fourEndpointSizeDiagonalFactor
@@ -222,9 +237,12 @@ theorem fourEndpoint_squareFree_transport
       (((n.descFactorial (fourEndpointJ alpha hAlpha L) : ENNReal) ^ 2) *
         (n + 1 : ENNReal) ^ fourEndpointDisplacement L) *
         (fourEndpointLocalProduct alpha hAlpha L ^ 2 *
-          fourEndpointLocalTransportDenProduct alpha hAlpha L) :=
-      mul_le_mul_right
-        (fourEndpoint_global_transport_ennreal n alpha hAlpha L) _
+          fourEndpointLocalTransportDenProduct alpha hAlpha L) := by
+      simpa [mul_comm] using
+        (mul_le_mul_right
+          (fourEndpoint_global_transport_ennreal n alpha hAlpha L)
+          (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

From b8e43fc6637255b8da8c7fd2437fa3a601b699f3 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:18:46 +0300
Subject: [PATCH 8/9] Fix product-power direction and final monotonicity

---
 .../Section8EndpointTransportCore.lean        | 50 +++++++++++--------
 1 file changed, 29 insertions(+), 21 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointTransportCore.lean b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
index e66b4050..491baa32 100644
--- a/625/formalization/Erdos625/Section8EndpointTransportCore.lean
+++ b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
@@ -114,14 +114,14 @@ theorem fourEndpointLocalProduct_sq_mul_transportDenProduct
           (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)
+        (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)
+        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
@@ -229,29 +229,37 @@ theorem fourEndpoint_squareFree_transport
         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
-    ((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) *
-        (fourEndpointLocalProduct alpha hAlpha L ^ 2 *
-          fourEndpointLocalTransportDenProduct alpha hAlpha L) := by
-      simpa [mul_comm] using
-        (mul_le_mul_right
-          (fourEndpoint_global_transport_ennreal n alpha hAlpha L)
-          (fourEndpointLocalProduct alpha hAlpha L ^ 2 *
-            fourEndpointLocalTransportDenProduct alpha hAlpha L))
-    _ = (((n.descFactorial (fourEndpointJ alpha hAlpha L) : ENNReal) ^ 2) *
-        (n + 1 : ENNReal) ^ fourEndpointDisplacement L) *
+    A * C = C * A := mul_comm _ _
+    _ ≤ C * B := 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 [fourEndpointLocalProduct_sq_mul_transportDenProduct
-        alpha hAlpha hHigh L]
+      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

From f702b646ad7fd88f63e294b905286f2a6a8cbbc1 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:26:01 +0300
Subject: [PATCH 9/9] Normalize the final endpoint-product orientation

---
 625/formalization/Erdos625/Section8EndpointTransportCore.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/625/formalization/Erdos625/Section8EndpointTransportCore.lean b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
index 491baa32..c456ded5 100644
--- a/625/formalization/Erdos625/Section8EndpointTransportCore.lean
+++ b/625/formalization/Erdos625/Section8EndpointTransportCore.lean
@@ -243,7 +243,8 @@ theorem fourEndpoint_squareFree_transport
       fourEndpoint_global_transport_ennreal n alpha hAlpha L
   calc
     A * C = C * A := mul_comm _ _
-    _ ≤ C * B := mul_le_mul_left hAB C
+    _ ≤ C * B := by
+      simpa [mul_comm] using (mul_le_mul_left hAB C)
     _ = B * C := mul_comm _ _
     _ = B *
       (fourEndpointDiagonalLocalProduct alpha hAlpha