From 2d932c59e76e20019bf8d46dc852efb92b373c37 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:51:32 +0300
Subject: [PATCH 01/34] Add simplified Sections 8 and 9 route

---
 625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md | 298 +++++++++++++++++++++
 1 file changed, 298 insertions(+)
 create mode 100644 625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md

diff --git a/625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md b/625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md
new file mode 100644
index 00000000..c3f47cd9
--- /dev/null
+++ b/625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md
@@ -0,0 +1,298 @@
+# A simpler route through Sections 8 and 9
+
+This note records three compatible simplifications of the current candidate
+proof.  They are designed to reduce both the manuscript's conceptual load and
+the number of distinct objects that must be carried through Lean.
+
+The first two concern the bare high-skeleton sum in Section 8.  The third
+concerns the residual attachment in Section 9.
+
+## 1. Replace the Cauchy step by termwise AM--GM
+
+Retain the notation of manuscript (8.8).  For a feasible endpoint table
+\(\mathbf L\), let
+
+\[
+ A_{\mathbf L}=\frac{\prod_i r_i!}{\prod_{ij}\ell_{ij}!},
+ \qquad
+ C_{\mathbf L}=\frac{\prod_j c_j!}{\prod_{ij}\ell_{ij}!},
+ \qquad
+ Q^{\mathbf L}=\prod_{ij}Q_{ij}^{\ell_{ij}}.
+\]
+
+Equation (8.8) is
+
+\[
+ W(\mathbf L)
+ \le
+ \sqrt{D(r)A_{\mathbf L}\,D(c)C_{\mathbf L}}\,Q^{\mathbf L}.
+\]
+
+Apply \(2\sqrt{xy}\le x+y\) term by term:
+
+\[
+ W(\mathbf L)
+ \le
+ \frac12\bigl(D(r)A_{\mathbf L}+D(c)C_{\mathbf L}\bigr)
+ Q^{\mathbf L}.                                      \tag{S8.1}
+\]
+
+For the first term, group by the row margin and drop only the column-margin
+constraint.  The multinomial theorem gives
+
+\[
+ \sum_{\mathbf L:\,\operatorname{row}(\mathbf L)=r}
+ A_{\mathbf L}Q^{\mathbf L}
+ \le
+ \prod_i\left(\sum_jQ_{ij}\right)^{r_i}.
+\]
+
+The symmetric statement holds for the second term.  Since every row and column
+sum of \(Q\) is at most \(1+C\eta_n\), and every margin has total mass at most
+\(k_{\mathrm{co}}\), summing (S8.1) yields directly
+
+\[
+ \boxed{
+ \sum_{\mathbf L}W(\mathbf L)
+ \le
+ (1+C\eta_n)^{k_{\mathrm{co}}}
+ \sum_rD(r).}                                         \tag{S8.2}
+\]
+
+Lemma 7.1 then gives
+
+\[
+ \sum_{\mathbf L}W(\mathbf L)
+ \le \exp\{O(\eta_nk_{\mathrm{co}})\}
+ =\exp\{O(\sqrt{n\ln n})\}.
+\]
+
+This removes:
+
+- Cauchy's inequality on the table family;
+- the quantity \((\sum_r\sqrt{D(r)})^2\);
+- the polynomial margin-count factor \(O(k_{\mathrm{co}}^4)\);
+- one layer of square-root bookkeeping in the formalization.
+
+The endpoint comparison itself may remain in the square-free form proved in
+PR #36.  The formal target corresponding to (S8.1) is the elementary
+linearization
+
+\[
+ x^2\le yz\quad\Longrightarrow\quad 2x\le y+z
+\]
+
+for the finite nonnegative quantities appearing after the positive factorial
+factors have been exposed.
+
+## 2. Charge every high multiplicity directly to an endpoint cell
+
+The current manuscript treats deficits \(e<m/4\) cellwise and sends the
+remaining high multiplicities to a residual middle-strip argument.  The latter
+is unnecessary if one accepts a slightly weaker, but still ample, error term.
+
+Let a high cell join sizes \(m\) and \(m+d\), where \(0\le d\le3\), and write
+its multiplicity as \(j=m-e\).  Since
+
+\[
+ j>R_0=\lfloor a/2\rfloor\ge\lfloor m/2\rfloor,
+\]
+
+we always have
+
+\[
+ 2e<m.                                                   \tag{S8.3}
+\]
+
+The exact local ratio from (8.21), including the global denominator charge
+from (8.22), is
+
+\[
+ A_{m,d}(e)
+ :=n^eR_{m,d}(e)
+ =n^e\frac{\binom me}{(d+1)\cdots(d+e)}
+   2^{-em+e(e+1)/2}.                                    \tag{S8.4}
+\]
+
+Put
+
+\[
+ b_m=\left\lfloor\frac{3m-1}{4}\right\rfloor.
+\]
+
+From (S8.3),
+
+\[
+ em-\frac{e(e+1)}2\ge e b_m.                            \tag{S8.5}
+\]
+
+Moreover \(\binom me\le m^e\), while
+\((d+1)\cdots(d+e)\ge1\).  Therefore
+
+\[
+ \boxed{
+ A_{m,d}(e)
+ \le
+ \left(\frac{nm}{2^{b_m}}\right)^e.}                   \tag{S8.6}
+\]
+
+All four endpoint sizes lie in \([a-3,a]\).  Define
+
+\[
+ b_*:=\left\lfloor\frac{3a-10}{4}\right\rfloor,
+ \qquad
+ \rho_n:=\frac{na}{2^{b_*}}.
+\]
+
+Then (S8.6) is at most \(\rho_n^e\) uniformly in the cell type.  Using
+\(2^a=\Theta(n^2/(\ln n)^2)\),
+
+\[
+ \rho_n=O\!\left(\frac{(\ln n)^{5/2}}{\sqrt n}\right)=o(1).
+                                                               \tag{S8.7}
+\]
+
+Hence, for every endpoint cell,
+
+\[
+ \sum_{\substack{e\ge1\\m-e>R_0}}A_{m,d}(e)
+ \le\sum_{e\ge1}\rho_n^e
+ \le 2\rho_n                                           \tag{S8.8}
+\]
+
+for all sufficiently large \(n\).  Distinguish the cells of an endpoint table,
+assign either \(e=0\) or any allowed high deficit, and then forget the labels.
+As in the current near-cell argument, this is exactly the multinomial
+expansion and introduces no extra multiplicity.  Since an endpoint skeleton
+contains at most \(k_{\mathrm{co}}\) cells,
+
+\[
+ \prod_c\left(1+\sum_eA_{m_c,d_c}(e)\right)
+ \le
+ \exp\{O(k_{\mathrm{co}}\rho_n)\}
+ =
+ \exp\{O(\sqrt n(\ln n)^{3/2})\}.                       \tag{S8.9}
+\]
+
+The exponent in (S8.9) is still
+
+\[
+ o\!\left(\frac{n}{(\ln n)^4}\right).
+\]
+
+Combining (S8.2) and (S8.9) gives the complete bare high-skeleton estimate
+without a residual middle strip:
+
+\[
+ \boxed{
+ \sum_{(\mathcal M,j)}w_{\mathrm{hi}}(\mathcal M,j)
+ \le
+ \exp\{O(\sqrt n(\ln n)^{3/2})\}
+ =
+ \exp\!\left\{o\!\left(\frac{n}{(\ln n)^4}\right)\right\}.}
+                                                               \tag{S8.10}
+\]
+
+This removes from Section 8:
+
+- the near/middle classification at \(e=m/4\);
+- the event \(\mathcal N(S)\);
+- the truncated residual factor \(E_{\mathrm{mid}}(S)\);
+- the joint middle-threshold quantity \(\Xi_4\);
+- the large/small residual split inside Section 8;
+- equations (8.26a)--(8.29b).
+
+It also restores a clean conceptual boundary: Section 8 is purely a sum over
+exposed high cells; Section 9 alone treats the residual configuration model.
+
+## 3. Absorb the Section 9 local product into the q mass
+
+After the threshold expansion, the current direct route gives
+
+\[
+ \mathcal A(\mathcal M,j)
+ \le
+ \exp(\Lambda_{\mathrm{loc}})
+ \sum_{F\text{ even}}
+   \prod_{e\in F\setminus\mathcal M}q_e,
+ \qquad
+ \Lambda_{\mathrm{loc}}=\sum_e\lambda_e.                \tag{S9.1}
+\]
+
+By definition,
+
+\[
+ q_e=\frac{\theta_e^2}{2}+\lambda_e,
+ \qquad
+ \lambda_e\le q_e.                                      \tag{S9.2}
+\]
+
+Restriction to the residual edges is injective on the even family because a
+nonempty subset of a matching cannot be even.  Thus
+
+\[
+ \sum_{F\text{ even}}\prod_{e\in F\setminus\mathcal M}q_e
+ \le
+ \prod_{e\notin\mathcal M}(1+q_e)
+ \le
+ \exp\left(\sum_eq_e\right).                             \tag{S9.3}
+\]
+
+Equations (S9.1)--(S9.3) give
+
+\[
+ \mathcal A(\mathcal M,j)
+ \le
+ \exp\left(2\sum_eq_e\right).                            \tag{S9.4}
+\]
+
+The pointwise quadratic estimate and the degree caps imply
+
+\[
+ \sum_eq_e
+ \le C\sum_{a,b}\theta_{ab}^2
+ =\frac{C}{m_0^2}
+   \left(\sum_ad_a^2\right)
+   \left(\sum_b(d'_b)^2\right)
+ \le C u_{\max}^2.                                       \tag{S9.5}
+\]
+
+Consequently the large-residual branch is simply
+
+\[
+ \boxed{
+ \mathcal A(\mathcal M,j)
+ \le \exp(Cu_{\max}^2)
+ =\exp(O((\ln n)^2)).}                                   \tag{S9.6}
+\]
+
+This removes the separate cubic lambda estimate
+\(C u_{\max}^4/m_0\).  Together with the matching-restriction injection, it
+also removes all cycle and walk estimates from the proof of Lemma 9.1.
+PR #37 kernel-checks the finite q-only version of this argument.
+
+## Proposed manuscript organization
+
+A clearer final organization is:
+
+1. **Endpoint transportation:** state the square-free finite core and its
+   geometric-mean corollary.
+2. **Endpoint summation:** apply termwise AM--GM and one-sided multinomial
+   expansions.
+3. **All high deficits:** use the single geometric bound (S8.6)--(S8.9).
+4. **Residual attachment:** perform the threshold expansion, matching
+   restriction, and q-only total-mass estimate.
+5. **Two residual regimes:** retain only the simple deterministic small-residual
+   estimate and the q-only large-residual estimate.
+
+Under this organization, Section 8 no longer contains a conditional residual
+expectation, while Section 9 no longer contains a cycle decomposition or a
+separate cubic-moment branch.
+
+## Remaining checks before canonical integration
+
+The main new point requiring independent mathematical review is the extension
+of the endpoint charging from \(e<m/4\) to the full high range via (S8.3)--(S8.8).
+The accompanying exact checker verifies the finite exponent inequality and the
+local ratio domination over a large exhaustive integer range; its phase scans
+are diagnostics, not a proof of the asymptotic use of (8.15).

From 5647ae2ab931d6da5124a0501ed4d352d9c1971a Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:52:26 +0300
Subject: [PATCH 02/34] Add exact checker for Section 8 and 9 simplifications

---
 .../sections8_9_simplification_check.py       | 190 ++++++++++++++++++
 1 file changed, 190 insertions(+)
 create mode 100644 625/experiments/sections8_9_simplification_check.py

diff --git a/625/experiments/sections8_9_simplification_check.py b/625/experiments/sections8_9_simplification_check.py
new file mode 100644
index 00000000..33fd204d
--- /dev/null
+++ b/625/experiments/sections8_9_simplification_check.py
@@ -0,0 +1,190 @@
+#!/usr/bin/env python3
+"""Finite regression checks for the simplified Sections 8--9 route.
+
+The exact gates use only the Python standard library and remain active under
+``python -O``.  Floating-point phase scans are diagnostics and are labelled as
+such; they are not used to certify an asymptotic theorem.
+"""
+
+from __future__ import annotations
+
+from fractions import Fraction
+from math import comb, e, exp, lgamma, log, log2
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise RuntimeError(message)
+
+
+def denominator_product(d: int, deficit: int) -> int:
+    result = 1
+    for t in range(1, deficit + 1):
+        result *= d + t
+    return result
+
+
+def local_ratio_with_global_charge(n: int, m: int, d: int, deficit: int) -> Fraction:
+    exponent = deficit * m - deficit * (deficit + 1) // 2
+    return Fraction(
+        (n**deficit) * comb(m, deficit),
+        denominator_product(d, deficit) * (2**exponent),
+    )
+
+
+def exact_high_deficit_checks() -> tuple[int, int]:
+    """Check the exact geometric domination used in (S8.5)--(S8.6)."""
+
+    exponent_cases = 0
+    ratio_cases = 0
+
+    for m in range(2, 601):
+        b_m = (3 * m - 1) // 4
+        for deficit in range(1, m):
+            if 2 * deficit >= m:
+                continue
+
+            exponent = deficit * m - deficit * (deficit + 1) // 2
+            require(
+                exponent >= deficit * b_m,
+                f"exponent budget failed: m={m}, e={deficit}",
+            )
+            require(
+                comb(m, deficit) <= m**deficit,
+                f"choose bound failed: m={m}, e={deficit}",
+            )
+            exponent_cases += 1
+
+            # Exact Fraction checks on a representative range.  The preceding
+            # componentwise inequalities prove the same comparison generally;
+            # these cases guard the implemented formula and integer floors.
+            if m <= 120:
+                for d in range(4):
+                    for n in (2, 3, 10, 97, 10_000):
+                        lhs = local_ratio_with_global_charge(n, m, d, deficit)
+                        rho = Fraction(n * m, 2**b_m)
+                        require(
+                            lhs <= rho**deficit,
+                            f"local geometric bound failed: n={n}, m={m}, "
+                            f"d={d}, e={deficit}",
+                        )
+                        ratio_cases += 1
+
+    return exponent_cases, ratio_cases
+
+
+def exact_amgm_checks() -> int:
+    """Check the square-free form of termwise AM--GM: 4xy <= (x+y)^2."""
+
+    cases = 0
+    rationals = [Fraction(a, b) for b in range(1, 13) for a in range(0, 25)]
+    for x in rationals:
+        for y in rationals:
+            require(4 * x * y <= (x + y) ** 2, f"AM-GM failed: x={x}, y={y}")
+            cases += 1
+    return cases
+
+
+def exact_q_absorption_checks() -> int:
+    """Check lambda <= q and the corresponding product domination exactly."""
+
+    cases = 0
+    values = [Fraction(a, b) for b in range(1, 11) for a in range(0, 21)]
+    for lam in values:
+        for theta in values:
+            q = theta * theta / 2 + lam
+            require(lam <= q, f"lambda <= q failed: lambda={lam}, theta={theta}")
+            require(
+                (1 + lam) * (1 + q) <= (1 + q) ** 2,
+                f"product absorption failed: lambda={lam}, q={q}",
+            )
+            cases += 1
+    return cases
+
+
+def alpha_zero(n: int) -> float:
+    ell = log2(n)
+    return 2 * ell - 2 * log2(ell) + 2 * log2(e / 2) + 1
+
+
+def log2_local_ratio(n: int, m: int, d: int, deficit: int) -> float:
+    exponent = deficit * m - deficit * (deficit + 1) / 2
+    return (
+        deficit * log2(n)
+        + (lgamma(m + 1) - lgamma(deficit + 1) - lgamma(m - deficit + 1)) / log(2)
+        - (lgamma(d + deficit + 1) - lgamma(d + 1)) / log(2)
+        - exponent
+    )
+
+
+def log2_sum(values: list[float]) -> float:
+    maximum = max(values)
+    return maximum + log2(sum(2 ** (value - maximum) for value in values))
+
+
+def phase_diagnostics() -> list[str]:
+    lines: list[str] = []
+    for power in (10, 20, 50, 100, 200):
+        n = 10**power
+        alpha = int(alpha_zero(n))
+        a = alpha - 2
+        cutoff = a // 2
+        b_star = (3 * a - 10) // 4
+        log2_rho = log2(n) + log2(a) - b_star
+
+        worst_log_sum = float("-inf")
+        worst_type: tuple[int, int] | None = None
+        for i in range(4):
+            for j in range(4):
+                m = min(a - i, a - j)
+                d = abs(i - j)
+                max_deficit = m - (cutoff + 1)
+                if max_deficit < 1:
+                    continue
+                terms = [
+                    log2_local_ratio(n, m, d, deficit)
+                    for deficit in range(1, max_deficit + 1)
+                ]
+                value = log2_sum(terms)
+                if value > worst_log_sum:
+                    worst_log_sum = value
+                    worst_type = (i, j)
+
+        # Once rho < 1, the exact geometric majorant is rho/(1-rho).
+        if log2_rho < 0:
+            rho = 2**log2_rho
+            log2_majorant = log2(rho / (1 - rho))
+            require(
+                worst_log_sum <= log2_majorant + 1e-9,
+                f"phase diagnostic exceeds geometric majorant at 10^{power}",
+            )
+            majorant_text = f"log2 geometric majorant={log2_majorant:.6f}"
+        else:
+            majorant_text = "rho >= 1 (pre-asymptotic diagnostic only)"
+
+        lines.append(
+            f"  n=10^{power}: a={a}, worst type={worst_type}, "
+            f"log2 full-deficit sum={worst_log_sum:.6f}, "
+            f"log2 rho={log2_rho:.6f}, {majorant_text}"
+        )
+    return lines
+
+
+def main() -> None:
+    exponent_cases, ratio_cases = exact_high_deficit_checks()
+    amgm_cases = exact_amgm_checks()
+    q_cases = exact_q_absorption_checks()
+    diagnostics = phase_diagnostics()
+
+    print("ERDOS 625 SECTIONS 8--9 SIMPLIFICATION CHECK: PASS")
+    print(f"  high-deficit exponent cases: {exponent_cases}")
+    print(f"  exact local-ratio cases: {ratio_cases}")
+    print(f"  exact AM-GM cases: {amgm_cases}")
+    print(f"  exact q-absorption cases: {q_cases}")
+    print("  phase diagnostics:")
+    for line in diagnostics:
+        print(line)
+
+
+if __name__ == "__main__":
+    main()

From 6d816dd285345e4104ab6f86280c7acd7225103b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:52:58 +0300
Subject: [PATCH 03/34] Add Sections 8 and 9 simplification checker workflow

---
 ...os625-sections8-9-simplification-check.yml | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 .github/workflows/erdos625-sections8-9-simplification-check.yml

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
new file mode 100644
index 00000000..4e729fa8
--- /dev/null
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -0,0 +1,24 @@
+name: Erdős 625 Sections 8--9 simplification check
+
+on:
+  pull_request:
+    paths:
+      - "625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md"
+      - "625/experiments/sections8_9_simplification_check.py"
+      - ".github/workflows/erdos625-sections8-9-simplification-check.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  exact-checks:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Compile checker
+        run: python -m py_compile 625/experiments/sections8_9_simplification_check.py
+      - name: Run exact and diagnostic checks
+        run: python 625/experiments/sections8_9_simplification_check.py
+      - name: Run with optimization enabled
+        run: python -O 625/experiments/sections8_9_simplification_check.py

From 2a2511a483fd50fdae431bf8da65ae163b89bae9 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:58:21 +0300
Subject: [PATCH 04/34] Kernel-check the full high-deficit parametrization

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

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean b/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
new file mode 100644
index 00000000..2f997aa8
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
@@ -0,0 +1,77 @@
+import Erdos625.Section8NearArithmeticFoundation
+import Mathlib.Tactic
+
+/-!
+# Section VIII: one deficit parametrization for the full high range
+
+A high cell of smaller endpoint size `m` has multiplicity `j` above the global
+cutoff `a / 2`.  Writing `e = m - j` parametrizes every such multiplicity by a
+single endpoint deficit.  This file records the exact finite arithmetic needed
+to replace the near/middle split by one all-deficit sum.
+
+No weight estimate or asymptotic statement is asserted here.
+-/
+
+namespace Erdos625
+
+set_option autoImplicit false
+
+/-- Largest endpoint deficit compatible with the strict high-cell cutoff. -/
+def allHighDeficitCut (a m : Nat) : Nat := m - (a / 2 + 1)
+
+/-- A multiplicity above the global cutoff is also above the half-size cutoff
+of every smaller endpoint size `m <= a`. -/
+theorem highMultiplicity_above_half_size
+    (a m j : Nat) (hm : m <= a) (hj : a / 2 < j) :
+    m / 2 < j := by
+  have hhalf : m / 2 <= a / 2 := Nat.div_le_div_right hm
+  exact lt_of_le_of_lt hhalf hj
+
+/-- The endpoint deficit of a high multiplicity is strictly below half the
+smaller endpoint size. -/
+theorem highMultiplicity_deficit_twice_lt
+    (a m j : Nat) (hm : m <= a) (hj : a / 2 < j) (hjm : j <= m) :
+    2 * (m - j) < m := by
+  have hjhalf := highMultiplicity_above_half_size a m j hm hj
+  omega
+
+/-- Every strict high multiplicity yields a deficit in the single finite window
+`0, ..., allHighDeficitCut a m`. -/
+theorem endpointDeficit_le_allHighDeficitCut
+    (a m j : Nat) (hj : a / 2 < j) (hjm : j <= m) :
+    m - j <= allHighDeficitCut a m := by
+  unfold allHighDeficitCut
+  omega
+
+/-- Conversely, every deficit in the all-high window reconstructs a strict high
+multiplicity, provided the endpoint itself lies above the cutoff. -/
+theorem allHighDeficit_reconstructs_highMultiplicity
+    (a m e : Nat) (hmHigh : a / 2 < m)
+    (he : e <= allHighDeficitCut a m) :
+    a / 2 < m - e := by
+  unfold allHighDeficitCut at he
+  omega
+
+/-- Subtracting and then restoring a feasible endpoint deficit recovers the
+endpoint size exactly. -/
+theorem endpointDeficit_reconstruction
+    (m j : Nat) (hjm : j <= m) :
+    m - (m - j) = j := by
+  omega
+
+/-- For a fixed endpoint size, the deficit encoding is injective on feasible
+multiplicities. -/
+theorem endpointDeficit_injective
+    (m j₁ j₂ : Nat) (hj₁ : j₁ <= m) (hj₂ : j₂ <= m)
+    (hdef : m - j₁ = m - j₂) :
+    j₁ = j₂ := by
+  omega
+
+#print axioms highMultiplicity_above_half_size
+#print axioms highMultiplicity_deficit_twice_lt
+#print axioms endpointDeficit_le_allHighDeficitCut
+#print axioms allHighDeficit_reconstructs_highMultiplicity
+#print axioms endpointDeficit_reconstruction
+#print axioms endpointDeficit_injective
+
+end Erdos625

From ba9d06c89f88b06a50d82ad2c4bc212e995eb6fa Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:58:55 +0300
Subject: [PATCH 05/34] Add focused Lean check for all-high deficit arithmetic

---
 ...os625-sections8-9-simplification-check.yml | 39 +++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index 4e729fa8..dcf0006b 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -5,6 +5,7 @@ on:
     paths:
       - "625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md"
       - "625/experiments/sections8_9_simplification_check.py"
+      - "625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean"
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"
   workflow_dispatch:
 
@@ -22,3 +23,41 @@ jobs:
         run: python 625/experiments/sections8_9_simplification_check.py
       - name: Run with optimization enabled
         run: python -O 625/experiments/sections8_9_simplification_check.py
+
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section8AllHighDeficitArithmetic.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 arithmetic module warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section8AllHighDeficitArithmetic --wfail \
+            > /tmp/section8-all-deficit-lean.log 2>&1
+          status=$?
+          tail -n 220 /tmp/section8-all-deficit-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section8-all-deficit-lean-log
+          path: /tmp/section8-all-deficit-lean.log
+          if-no-files-found: ignore

From ccffa492b7ff7e8507ba09a3b82583e321c6e11f Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:10:14 +0300
Subject: [PATCH 06/34] Add a formal two-thirds high-deficit exponent budget

---
 .../Section8AllHighDeficitArithmetic.lean     | 40 ++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean b/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
index 2f997aa8..42f1fb81 100644
--- a/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
+++ b/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
@@ -9,7 +9,10 @@ cutoff `a / 2`.  Writing `e = m - j` parametrizes every such multiplicity by a
 single endpoint deficit.  This file records the exact finite arithmetic needed
 to replace the near/middle split by one all-deficit sum.
 
-No weight estimate or asymptotic statement is asserted here.
+The final theorem also supplies a deliberately coarse exponent budget with
+coefficient `2/3`.  It is weaker than the sharper `3/4` estimate in the review
+note, but already yields a geometric all-deficit sum of the required
+asymptotic scale and has a substantially simpler integer proof.
 -/
 
 namespace Erdos625
@@ -67,11 +70,46 @@ theorem endpointDeficit_injective
     j₁ = j₂ := by
   omega
 
+/-- A deficit below half the endpoint pays at least two thirds of the endpoint
+size in the local binary exponent:
+
+`e * floor(2m/3) <= e*m - e*(e+1)/2`.
+
+This weaker replacement for the sharper `floor((3m-1)/4)` budget is sufficient
+for a uniform geometric all-high-deficit bound and avoids parity-sensitive
+quarter arithmetic. -/
+theorem highDeficit_twoThird_exponent_budget
+    (m e : Nat) (hhalf : 2 * e < m) :
+    e * ((2 * m) / 3) <= e * m - e * (e + 1) / 2 := by
+  by_cases he : e = 0
+  · simp [he]
+  have hepos : 0 < e := Nat.pos_of_ne_zero he
+  have hlinear : 3 * (e + 1) <= 2 * m := by
+    omega
+  have hmul : 3 * (e * (e + 1)) <= 2 * (e * m) := by
+    nlinarith [Nat.mul_le_mul_left e hlinear]
+  have hdiv := Nat.div_mul_le_self (e * (e + 1)) 2
+  have hpenalty : 3 * (e * (e + 1) / 2) <= e * m := by
+    nlinarith
+  have hpenalty_le : e * (e + 1) / 2 <= e * m := by
+    omega
+  have hsub :
+      (e * m - e * (e + 1) / 2) + e * (e + 1) / 2 = e * m :=
+    Nat.sub_add_cancel hpenalty_le
+  have hthird := Nat.div_mul_le_self (2 * m) 3
+  have hbudget : 3 * (e * ((2 * m) / 3)) <= 2 * (e * m) := by
+    nlinarith [Nat.mul_le_mul_left e hthird]
+  have hexponent :
+      2 * (e * m) <= 3 * (e * m - e * (e + 1) / 2) := by
+    omega
+  omega
+
 #print axioms highMultiplicity_above_half_size
 #print axioms highMultiplicity_deficit_twice_lt
 #print axioms endpointDeficit_le_allHighDeficitCut
 #print axioms allHighDeficit_reconstructs_highMultiplicity
 #print axioms endpointDeficit_reconstruction
 #print axioms endpointDeficit_injective
+#print axioms highDeficit_twoThird_exponent_budget
 
 end Erdos625

From c55188fbe1de41894e7376d0ff929ff4a262e2b0 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:11:19 +0300
Subject: [PATCH 07/34] Add a formalization-first all-deficit bound

---
 ...ECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md | 115 ++++++++++++++++++
 1 file changed, 115 insertions(+)
 create mode 100644 625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md

diff --git a/625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md b/625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md
new file mode 100644
index 00000000..0bdf3077
--- /dev/null
+++ b/625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md
@@ -0,0 +1,115 @@
+# Formalization-first all-high-deficit bound
+
+The sharper review estimate uses the binary exponent budget
+
+\[
+em-\frac{e(e+1)}2
+\ge e\left\lfloor\frac{3m-1}{4}\right\rfloor
+\qquad(2e<m).
+\]
+
+That bound is correct and is checked exhaustively in
+`sections8_9_simplification_check.py`.  It is, however, stronger than the proof
+needs and introduces quarter floors and parity bookkeeping.  A weaker bound is
+substantially easier to formalize and still has ample asymptotic room.
+
+## Kernel-checked exponent budget
+
+PR #38 proves in Lean:
+
+\[
+\boxed{
+ e\left\lfloor\frac{2m}{3}\right\rfloor
+ \le em-\frac{e(e+1)}2
+ \qquad\text{whenever }2e<m.}
+\tag{F8.1}
+\]
+
+The proof is pure natural-number arithmetic.  Its key observation is that for
+`e>0`, the condition `2e<m` gives
+
+\[
+3(e+1)\le2m.
+\]
+
+Together with
+
+\[
+2\left\lfloor\frac{e(e+1)}2\right\rfloor\le e(e+1),
+\]
+
+this yields
+
+\[
+3\left\lfloor\frac{e(e+1)}2\right\rfloor\le em,
+\]
+
+which is equivalent to retaining at least two thirds of the endpoint exponent.
+The declaration is
+`highDeficit_twoThird_exponent_budget`.
+
+## One geometric series for the entire high range
+
+For the exact local ratio
+
+\[
+A_{m,d}(e)
+=n^e\frac{\binom me}{(d+1)\cdots(d+e)}
+ 2^{-em+e(e+1)/2},
+\]
+
+use \(\binom me\le m^e\), the denominator lower bound by one, and (F8.1):
+
+\[
+A_{m,d}(e)
+\le
+\left(\frac{nm}{2^{\lfloor2m/3\rfloor}}\right)^e.
+\tag{F8.2}
+\]
+
+All four endpoint sizes satisfy \(a-3\le m\le a\).  Set
+
+\[
+b_*:=\left\lfloor\frac{2(a-3)}3\right\rfloor,
+\qquad
+\rho_n:=\frac{na}{2^{b_*}}.
+\]
+
+Then every allowed high deficit is bounded by \(\rho_n^e\).  From
+\(2^a=\Theta(n^2/(\ln n)^2)\),
+
+\[
+\rho_n
+=O\!\left(\frac{(\ln n)^{7/3}}{n^{1/3}}\right)
+=o(1).
+\tag{F8.3}
+\]
+
+Consequently the complete deficit sum of one endpoint cell is at most
+\(2\rho_n\) eventually.  Since an endpoint high skeleton contains at most
+\(k_{\mathrm{co}}=O(n/\ln n)\) cells, all high deficits cost
+
+\[
+\exp\{O(k_{\mathrm{co}}\rho_n)\}
+=
+\exp\{O(n^{2/3}(\ln n)^{4/3})\}
+=
+\exp\!\left\{o\!\left(\frac n{(\ln n)^4}\right)\right\}.
+\tag{F8.4}
+\]
+
+## Recommendation for the paper
+
+Use (F8.1)--(F8.4) in the canonical manuscript unless a sharper exponent is
+needed later.  The two-thirds budget is weaker numerically than the
+three-quarters budget, but it has four practical advantages:
+
+1. it is already kernel-checked at the integer-arithmetic level;
+2. it has no parity-sensitive quarter floor;
+3. it covers the full high range in one statement;
+4. it still removes the complete middle-strip residual argument with a large
+   asymptotic margin.
+
+The resulting Section 8 proof becomes: endpoint transport, termwise AM--GM,
+one multinomial expansion, and one all-deficit geometric series.  No
+near/middle partition or residual configuration model is needed in Section 8.

From b6f9b5ddf1245488fcb3c3af0197ce787d9fdc2e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:14:03 +0300
Subject: [PATCH 08/34] Track the formalization-first Section 8 note

---
 .github/workflows/erdos625-sections8-9-simplification-check.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index dcf0006b..23f633c2 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -4,6 +4,7 @@ on:
   pull_request:
     paths:
       - "625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md"
+      - "625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md"
       - "625/experiments/sections8_9_simplification_check.py"
       - "625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean"
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"

From e09dc3c9dc91283e50b3ec3f3fa8634ea6aa7e3a Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:16:53 +0300
Subject: [PATCH 09/34] Draft a concise replacement for manuscript Sections 8
 and 9

---
 625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md | 407 ++++++++++++++++++
 1 file changed, 407 insertions(+)
 create mode 100644 625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md

diff --git a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
new file mode 100644
index 00000000..190f57a7
--- /dev/null
+++ b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
@@ -0,0 +1,407 @@
+# Concise replacement draft for Sections 8 and 9
+
+This draft is intended to replace the present high-skeleton and residual
+attachment arguments after the supporting PRs have been reviewed.  It retains
+the exact canonical exposure, but removes the table-family Cauchy step, the
+near/middle split, the Section 8 residual model, the cycle decomposition, and
+the separate cubic lambda estimate.
+
+Throughout, \(N=\ln n\),
+
+\[
+U=\alpha-2,
+\qquad
+R_0=\lfloor U/2\rfloor,
+\]
+
+and the four block sizes are \(u_i=U-i\), \(0\le i\le3\).
+
+## 8. Canonical high cells
+
+For an overlap table \(r=(r_{ab})\), let
+
+\[
+\mathcal M(r)=\{(a,b):r_{ab}>R_0\}.
+\]
+
+Because every row and column sum is at most \(U\), the support
+\(\mathcal M(r)\) is a bipartite matching.  Write its cell multiplicities as
+\(j_{ab}=r_{ab}\), and let \(J=\sum_{(a,b)\in\mathcal M}j_{ab}\).
+Exposing the corresponding stub pairs has incidence
+
+\[
+\pi(\mathcal M,j)
+=
+\frac{\prod_{(a,b)\in\mathcal M}(s_a)_{j_{ab}}(t_b)_{j_{ab}}}
+     {(n)_J\prod_{(a,b)\in\mathcal M}j_{ab}!}.
+\tag{8.1}
+\]
+
+Conditional on those pairs, the remaining matching is uniform with the
+induced residual degrees, is zero on \(\mathcal M\), and is capped by \(R_0\).
+Multiplying (8.1) by the exact residual configuration-table law recovers the
+original overlap probability.  Thus the decomposition is exact and every
+overlap table occurs once.
+
+### 8.1 Endpoint transportation
+
+First suppose every high cell is a full-containment cell.  Aggregate the
+physical block pairs by their endpoint types into a table
+\(L=(\ell_{ij})_{0\le i,j\le3}\).  Let \(r_i=\sum_j\ell_{ij}\),
+\(c_j=\sum_i\ell_{ij}\), and let \(W(L)\) be the exact endpoint incidence and
+local signed reward.  Let \(D(r)\) be the common-subprofile weight from
+Section 7.  Define
+
+\[
+A_L=\frac{\prod_i r_i!}{\prod_{ij}\ell_{ij}!},
+\qquad
+C_L=\frac{\prod_j c_j!}{\prod_{ij}\ell_{ij}!}.
+\]
+
+The endpoint transport calculation gives
+
+\[
+W(L)
+\le
+\sqrt{D(r)A_L\,D(c)C_L}\,Q^L,
+\qquad
+Q^L:=\prod_{ij}Q_{ij}^{\ell_{ij}},
+\tag{8.2}
+\]
+
+where \(Q_{ii}=1\) and, for \(d=|i-j|\in\{1,2,3\}\),
+
+\[
+Q_{ij}\le\frac{\eta_n^d}{d!},
+\qquad
+\eta_n=O\!\left(\frac{N^{3/2}}{\sqrt n}\right).
+\tag{8.3}
+\]
+
+The square-free finite algebra behind (8.2) is the statement formalized in
+PR #36.  For summation, apply \(2\sqrt{xy}\le x+y\) termwise:
+
+\[
+W(L)
+\le
+\frac12\bigl(D(r)A_L+D(c)C_L\bigr)Q^L.
+\tag{8.4}
+\]
+
+Fixing \(r\) and dropping only the column-margin constraint gives the exact
+multinomial bound
+
+\[
+\sum_{L:\operatorname{row}(L)=r}A_LQ^L
+\le
+\prod_i\left(\sum_jQ_{ij}\right)^{r_i}.
+\tag{8.5}
+\]
+
+The symmetric estimate holds after fixing \(c\).  Every row and column sum of
+\(Q\) is at most \(1+C\eta_n\), while the total number of selected blocks is at
+most \(k_{\mathrm{co}}\).  Hence
+
+\[
+\sum_LW(L)
+\le
+(1+C\eta_n)^{k_{\mathrm{co}}}\sum_rD(r).
+\tag{8.6}
+\]
+
+Lemma 7.1 gives \(\sum_rD(r)=1+o(1)\), and therefore
+
+\[
+\sum_LW(L)
+\le
+\exp\{O(\eta_nk_{\mathrm{co}})\}
+=
+\exp\{O(\sqrt{nN})\}.
+\tag{8.7}
+\]
+
+This proves the endpoint sum without Cauchy's inequality, without
+\((\sum_r\sqrt{D(r)})^2\), and without a polynomial count of margin vectors.
+
+### 8.2 All high multiplicities in one geometric expansion
+
+Let a high cell join endpoint sizes \(m\) and \(m+d\), \(0\le d\le3\), and
+write its multiplicity as \(j=m-e\).  Since \(j>R_0\ge\lfloor m/2\rfloor\),
+
+\[
+2e<m.
+\tag{8.8}
+\]
+
+Filling the cell from \(m-e\) to its endpoint multiplicity \(m\) changes the
+local factor by the exact ratio
+
+\[
+R_{m,d}(e)
+=
+\frac{\binom me}{(d+1)\cdots(d+e)}
+2^{-em+e(e+1)/2}.
+\tag{8.9}
+\]
+
+For several cells, if \(E=\sum e\), the single global denominator ratio is at
+most \(n^E\).  Thus each cell may be charged the factor
+\(A_{m,d}(e)=n^eR_{m,d}(e)\).
+
+The formalization-first integer estimate is
+
+\[
+e\left\lfloor\frac{2m}{3}\right\rfloor
+\le
+em-\frac{e(e+1)}2
+\qquad(2e<m).
+\tag{8.10}
+\]
+
+It is kernel-checked in PR #38.  Since
+\(inom me\le m^e\) and the denominator in (8.9) is at least one,
+
+\[
+A_{m,d}(e)
+\le
+\left(
+\frac{nm}{2^{\lfloor2m/3\rfloor}}
+\right)^e.
+\tag{8.11}
+\]
+
+All endpoint sizes satisfy \(U-3\le m\le U\).  Put
+
+\[
+b_*:=\left\lfloor\frac{2(U-3)}3\right\rfloor,
+\qquad
+\rho_n:=\frac{nU}{2^{b_*}}.
+\]
+
+The phase relation \(2^U=\Theta(n^2/N^2)\) gives
+
+\[
+\rho_n
+=O\!\left(\frac{N^{7/3}}{n^{1/3}}\right)
+=o(1).
+\tag{8.12}
+\]
+
+Consequently the sum of all nonzero high deficits of one endpoint cell is at
+most \(2\rho_n\) eventually.  A high skeleton is a matching, so filling all its
+cells to their endpoints produces a feasible endpoint skeleton.  Conversely,
+an endpoint skeleton together with one allowed deficit per cell reconstructs
+the original high skeleton uniquely.  Distinguishing identical typed cells and
+then forgetting the labels is exactly the multinomial expansion; no further
+multiplicity is introduced.
+
+There are at most \(k_{\mathrm{co}}\) endpoint cells.  Therefore all high
+multiplicities cost at most
+
+\[
+(1+2\rho_n)^{k_{\mathrm{co}}}
+\le
+\exp\{O(k_{\mathrm{co}}\rho_n)\}
+=
+\exp\{O(n^{2/3}N^{4/3})\}.
+\tag{8.13}
+\]
+
+Combining (8.7) and (8.13),
+
+\[
+\boxed{
+\sum_{(\mathcal M,j)}w_{\mathrm{hi}}(\mathcal M,j)
+\le
+\exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}.}
+\tag{8.14}
+\]
+
+No near/middle partition or residual configuration-model argument is needed in
+Section 8.
+
+## 9. Residual attachment
+
+Fix an attained high skeleton \((\mathcal M,j)\), and let \(m_0=n-J\) be its
+residual stub mass.  Its exact residual attachment is
+
+\[
+\mathcal A(\mathcal M,j)
+=
+\mathbb E_{\mathrm{res}}\!\left[
+\prod_e g(r'_e)
+2^{\beta(\mathcal M\cup H_{\mathrm{res}})}
+\mathbf1_{\mathcal E(\mathcal M,j)}
+\right].
+\tag{9.1}
+\]
+
+For cells outside \(\mathcal M\), set
+
+\[
+\theta_{ab}=\frac{e\,d_ad'_b}{m_0},
+\qquad
+q_{ab}
+=
+\frac{\theta_{ab}^2}{2}
++
+\sum_{x=3}^{R_0}\bigl(g(x)-g(x-1)\bigr)
+\frac{\theta_{ab}^x}{x!},
+\tag{9.2}
+\]
+
+and put \(q_{ab}=0\) on \(\mathcal M\).
+
+The threshold expansion for a fixed even edge set \(F\) is bounded by a product
+of selected \(q\)-weights and unselected local increments.  Every local
+increment is at most \(q_{ab}\).  Hence
+
+\[
+\mathcal A(\mathcal M,j)
+\le
+\left(\prod_{e\notin\mathcal M}(1+q_e)\right)
+\sum_{F\text{ even}}
+\prod_{e\in F\setminus\mathcal M}q_e.
+\tag{9.3}
+\]
+
+The restriction map \(F\mapsto F\setminus\mathcal M\) is injective on even edge
+sets: two completions with the same residual restriction differ by an even
+subset of a matching, and the only such subset is empty.  Therefore
+
+\[
+\sum_{F\text{ even}}
+\prod_{e\in F\setminus\mathcal M}q_e
+\le
+\prod_{e\notin\mathcal M}(1+q_e).
+\tag{9.4}
+\]
+
+Combining (9.3)--(9.4),
+
+\[
+\boxed{
+\mathcal A(\mathcal M,j)
+\le
+\exp\left(2\sum_eq_e\right).}
+\tag{9.5}
+\]
+
+### 9.1 Intrinsic quadratic regime
+
+If
+
+\[
+2^U\le m_0^3,
+\tag{9.6}
+\]
+
+then the finite endpoint estimate gives \(q_{ab}\le C\theta_{ab}^2\).  The
+square mass factorizes exactly:
+
+\[
+\sum_{a,b}\theta_{ab}^2
+=
+\frac{e^2}{m_0^2}
+\left(\sum_ad_a^2\right)
+\left(\sum_b(d'_b)^2\right)
+\le e^2U^2.
+\tag{9.7}
+\]
+
+Thus
+
+\[
+\boxed{
+\mathcal A(\mathcal M,j)
+\le\exp(CU^2)
+=\exp(O(N^2)).}
+\tag{9.8}
+\]
+
+PR #37 kernel-checks the finite q-only bound and its attained-profile
+specialization.
+
+### 9.2 Complementary small-power regime
+
+If (9.6) fails, the exact arithmetic dichotomy in PR #37 gives
+
+\[
+m_0<2^{\lceil U/3\rceil}.
+\tag{9.9}
+\]
+
+The deterministic residual estimate gives
+
+\[
+\mathcal A(\mathcal M,j)
+\le2^{Um_0/2}
+\le
+\exp\{O(U2^{U/3})\}.
+\tag{9.10}
+\]
+
+Since \(U=(2+o(1))\log_2n\), the exponent in (9.10) is
+\(n^{2/3+o(1)}\), and hence is \(o(n/N^4)\).  Together with (9.8), there is a
+deterministic sequence \(\varepsilon_n\to0\) such that uniformly over all
+attained high skeletons,
+
+\[
+\boxed{
+\mathcal A(\mathcal M,j)
+\le
+\exp\!\left\{\varepsilon_n\frac n{N^4}\right\}.}
+\tag{9.11}
+\]
+
+This regime split is intrinsic to the finite q estimate and avoids introducing
+the auxiliary threshold \(n/N^6\).
+
+## 9.3 Completion of the normalized second moment
+
+The exact canonical decomposition gives
+
+\[
+\frac{\mathbb E(Z_k^{\mathrm{sgn}})^2}
+     {(\mathbb EZ_k^{\mathrm{sgn}})^2}
+=
+\sum_{(\mathcal M,j)}
+ w_{\mathrm{hi}}(\mathcal M,j)
+ \mathcal A(\mathcal M,j).
+\tag{9.12}
+\]
+
+Equations (8.14) and (9.11) imply
+
+\[
+\frac{\mathbb E(Z_k^{\mathrm{sgn}})^2}
+     {(\mathbb EZ_k^{\mathrm{sgn}})^2}
+\le
+\exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}.
+\tag{9.13}
+\]
+
+This is the normalized second-moment estimate required by the seed and
+amplification argument.
+
+## Formalization map
+
+The concise route is supported by the following focused developments:
+
+- PR #34: matching-restriction injectivity and subset-product bound;
+- PR #35: literal attachment, attained-profile transport, and
+  `exp(O((log n)^2))` specialization;
+- PR #36: square-free endpoint transportation core;
+- PR #37: q-only absorption and intrinsic finite residual dichotomy;
+- PR #38: one all-high-deficit parametrization, its injectivity, and the
+  two-thirds exponent budget.
+
+The remaining formal work is concentrated in two bridges:
+
+1. derive the linear endpoint inequality (8.4) from the square-free theorem and
+   sum it through the exact physical/type-table quotient;
+2. transport the local geometric bound (8.11) through the physical endpoint
+   decoration map and prove its phase-uniform asymptotic form.
+
+Those two obligations are considerably narrower than the current separate
+endpoint, near, middle, residual-cycle, and cubic-moment proof branches.

From 7a4542933c61a598dcd9d6d9a5d76a332de0e4c2 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:17:30 +0300
Subject: [PATCH 10/34] Track the concise Sections 8 and 9 replacement draft

---
 .github/workflows/erdos625-sections8-9-simplification-check.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index 23f633c2..9114957c 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -5,6 +5,7 @@ on:
     paths:
       - "625/proofs/SECTIONS8_9_SIMPLIFIED_ROUTE.md"
       - "625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md"
+      - "625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md"
       - "625/experiments/sections8_9_simplification_check.py"
       - "625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean"
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"

From 9cfd2d093b898f100ae2f219d8648946533bb028 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:29:38 +0300
Subject: [PATCH 11/34] Kernel-check the square-free AM-GM linearization

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

diff --git a/625/formalization/Erdos625/Section8SquareFreeAMGM.lean b/625/formalization/Erdos625/Section8SquareFreeAMGM.lean
new file mode 100644
index 00000000..6ea68a2e
--- /dev/null
+++ b/625/formalization/Erdos625/Section8SquareFreeAMGM.lean
@@ -0,0 +1,41 @@
+import Mathlib.Tactic
+
+/-!
+# Section VIII: square-free AM--GM linearization
+
+The endpoint transport is most naturally formalized as a squared,
+cross-multiplied inequality.  The manuscript sum, however, only needs its
+linear AM--GM consequence.  This file isolates that elementary ordered-real
+bridge without introducing square roots.
+-/
+
+namespace Erdos625
+
+set_option autoImplicit false
+
+/-- A nonnegative square-product bound linearizes by AM--GM without taking a
+square root.  This is the abstract bridge used after the endpoint factorial
+normalizations have been exposed. -/
+theorem two_mul_le_add_of_sq_le_mul
+    (x y z : Real)
+    (hx : 0 <= x) (hy : 0 <= y) (hz : 0 <= z)
+    (h : x ^ 2 <= y * z) :
+    2 * x <= y + z := by
+  have hsq : (2 * x) ^ 2 <= (y + z) ^ 2 := by
+    nlinarith [sq_nonneg (y - z)]
+  nlinarith [sq_nonneg (2 * x + y + z)]
+
+/-- Weighted form used when the same nonnegative table factor multiplies both
+one-sided endpoint contributions. -/
+theorem two_mul_weight_le_add_of_sq_le_mul
+    (x y z weight : Real)
+    (hx : 0 <= x) (hy : 0 <= y) (hz : 0 <= z) (hw : 0 <= weight)
+    (h : x ^ 2 <= y * z) :
+    2 * (x * weight) <= y * weight + z * weight := by
+  have hlinear := two_mul_le_add_of_sq_le_mul x y z hx hy hz h
+  nlinarith
+
+#print axioms two_mul_le_add_of_sq_le_mul
+#print axioms two_mul_weight_le_add_of_sq_le_mul
+
+end Erdos625

From 5a439f22e94df0f9b3c3ecff2f47dcd0f9138bc7 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:29:54 +0300
Subject: [PATCH 12/34] Aggregate the Section 8 simplification core

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

diff --git a/625/formalization/Erdos625/Section8SimplificationCore.lean b/625/formalization/Erdos625/Section8SimplificationCore.lean
new file mode 100644
index 00000000..947a103f
--- /dev/null
+++ b/625/formalization/Erdos625/Section8SimplificationCore.lean
@@ -0,0 +1,10 @@
+import Erdos625.Section8SquareFreeAMGM
+import Erdos625.Section8AllHighDeficitArithmetic
+
+/-!
+# Section VIII simplification core
+
+This aggregate module checks the two finite bridges used by the shortened
+Section VIII route: square-free AM--GM linearization and one all-high-deficit
+parametrization with a uniform binary exponent budget.
+-/

From 7b7fd2e4557980ca092996ec5604fb26138520c0 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:30:33 +0300
Subject: [PATCH 13/34] Validate the complete Section 8 simplification core

---
 ...dos625-sections8-9-simplification-check.yml | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index 9114957c..a4320710 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -7,7 +7,9 @@ on:
       - "625/proofs/SECTION8_FORMALIZATION_FIRST_ALL_DEFICIT.md"
       - "625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md"
       - "625/experiments/sections8_9_simplification_check.py"
+      - "625/formalization/Erdos625/Section8SquareFreeAMGM.lean"
       - "625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean"
+      - "625/formalization/Erdos625/Section8SimplificationCore.lean"
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"
   workflow_dispatch:
 
@@ -35,7 +37,9 @@ jobs:
         run: |
           if grep -nE \
             '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
-            625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean; then
+            625/formalization/Erdos625/Section8SquareFreeAMGM.lean \
+            625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean \
+            625/formalization/Erdos625/Section8SimplificationCore.lean; then
             exit 1
           fi
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
@@ -46,20 +50,20 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build arithmetic module warning-fatally
+      - name: Build Section 8 simplification core warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake build Erdos625.Section8AllHighDeficitArithmetic --wfail \
-            > /tmp/section8-all-deficit-lean.log 2>&1
+          lake build Erdos625.Section8SimplificationCore --wfail \
+            > /tmp/section8-simplification-lean.log 2>&1
           status=$?
-          tail -n 220 /tmp/section8-all-deficit-lean.log
+          tail -n 260 /tmp/section8-simplification-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: section8-all-deficit-lean-log
-          path: /tmp/section8-all-deficit-lean.log
+          name: section8-simplification-lean-log
+          path: /tmp/section8-simplification-lean.log
           if-no-files-found: ignore

From 6ef95b87592c69e84d1138c08b0da3836c1c8e9e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:43:26 +0300
Subject: [PATCH 14/34] Polish the concise Sections 8 and 9 replacement

---
 625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md | 229 ++++++++++--------
 1 file changed, 129 insertions(+), 100 deletions(-)

diff --git a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
index 190f57a7..18861e6c 100644
--- a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
+++ b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
@@ -1,14 +1,23 @@
 # Concise replacement draft for Sections 8 and 9
 
-This draft is intended to replace the present high-skeleton and residual
-attachment arguments after the supporting PRs have been reviewed.  It retains
-the exact canonical exposure, but removes the table-family Cauchy step, the
-near/middle split, the Section 8 residual model, the cycle decomposition, and
-the separate cubic lambda estimate.
+This draft records the shortest proof route currently supported by the focused
+review PRs.  It keeps the exact canonical exposure but removes four separate
+layers of machinery:
 
-Throughout, \(N=\ln n\),
+- the table-family Cauchy inequality;
+- the near/middle high-cell split;
+- the residual configuration-model argument inside Section 8;
+- the cycle decomposition and separate cubic lambda estimate in Section 9.
+
+The notation is chosen to avoid collisions.  We use \(U=\alpha-2\) for the
+largest block size, \(\mathcal M\) for the exposed matching, \(h\) for an endpoint
+deficit, \(m_0\) for residual mass, and \(\mathrm e\) for Euler's number.
+
+Throughout,
 
 \[
+N=\ln n,
+\qquad
 U=\alpha-2,
 \qquad
 R_0=\lfloor U/2\rfloor,
@@ -18,39 +27,50 @@ and the four block sizes are \(u_i=U-i\), \(0\le i\le3\).
 
 ## 8. Canonical high cells
 
-For an overlap table \(r=(r_{ab})\), let
+For an overlap table \(r=(r_{ab})\), define
 
 \[
 \mathcal M(r)=\{(a,b):r_{ab}>R_0\}.
 \]
 
-Because every row and column sum is at most \(U\), the support
-\(\mathcal M(r)\) is a bipartite matching.  Write its cell multiplicities as
-\(j_{ab}=r_{ab}\), and let \(J=\sum_{(a,b)\in\mathcal M}j_{ab}\).
+Every row and column sum is at most \(U\), so \(\mathcal M(r)\) is a bipartite
+matching.  Write its cell multiplicities as \(j_{ab}=r_{ab}\), and put
+
+\[
+J=\sum_{(a,b)\in\mathcal M}j_{ab}.
+\]
+
 Exposing the corresponding stub pairs has incidence
 
 \[
 \pi(\mathcal M,j)
 =
-\frac{\prod_{(a,b)\in\mathcal M}(s_a)_{j_{ab}}(t_b)_{j_{ab}}}
+\frac{\prod_{(a,b)\in\mathcal M}
+      (s_a)_{j_{ab}}(t_b)_{j_{ab}}}
      {(n)_J\prod_{(a,b)\in\mathcal M}j_{ab}!}.
 \tag{8.1}
 \]
 
-Conditional on those pairs, the remaining matching is uniform with the
-induced residual degrees, is zero on \(\mathcal M\), and is capped by \(R_0\).
+Conditional on those pairs, the remaining matching is uniform with the induced
+residual degrees, is zero on \(\mathcal M\), and is capped by \(R_0\).
 Multiplying (8.1) by the exact residual configuration-table law recovers the
 original overlap probability.  Thus the decomposition is exact and every
 overlap table occurs once.
 
-### 8.1 Endpoint transportation
+### 8.1 Endpoint transportation without a global Cauchy step
+
+First suppose that every high cell is a full-containment cell.  Aggregate the
+physical block pairs by endpoint type into a table
+\(L=(\ell_{ij})_{0\le i,j\le3}\).  Let
+
+\[
+r_i=\sum_j\ell_{ij},
+\qquad
+c_j=\sum_i\ell_{ij},
+\]
 
-First suppose every high cell is a full-containment cell.  Aggregate the
-physical block pairs by their endpoint types into a table
-\(L=(\ell_{ij})_{0\le i,j\le3}\).  Let \(r_i=\sum_j\ell_{ij}\),
-\(c_j=\sum_i\ell_{ij}\), and let \(W(L)\) be the exact endpoint incidence and
-local signed reward.  Let \(D(r)\) be the common-subprofile weight from
-Section 7.  Define
+and let \(W(L)\) denote its exact endpoint incidence and local signed reward.
+Let \(D(r)\) be the common-subprofile weight from Section 7, and define
 
 \[
 A_L=\frac{\prod_i r_i!}{\prod_{ij}\ell_{ij}!},
@@ -65,11 +85,11 @@ W(L)
 \le
 \sqrt{D(r)A_L\,D(c)C_L}\,Q^L,
 \qquad
-Q^L:=\prod_{ij}Q_{ij}^{\ell_{ij}},
+Q^L=\prod_{ij}Q_{ij}^{\ell_{ij}},
 \tag{8.2}
 \]
 
-where \(Q_{ii}=1\) and, for \(d=|i-j|\in\{1,2,3\}\),
+where \(Q_{ii}=1\), and for \(d=|i-j|\in\{1,2,3\}\),
 
 \[
 Q_{ij}\le\frac{\eta_n^d}{d!},
@@ -78,8 +98,8 @@ Q_{ij}\le\frac{\eta_n^d}{d!},
 \tag{8.3}
 \]
 
-The square-free finite algebra behind (8.2) is the statement formalized in
-PR #36.  For summation, apply \(2\sqrt{xy}\le x+y\) termwise:
+PR #36 proves the square-free finite algebra underlying (8.2).  For the table
+sum, apply \(2\sqrt{xy}\le x+y\) term by term:
 
 \[
 W(L)
@@ -88,8 +108,8 @@ W(L)
 \tag{8.4}
 \]
 
-Fixing \(r\) and dropping only the column-margin constraint gives the exact
-multinomial bound
+Fix \(r\).  Dropping only the column-margin constraint and using the
+multinomial theorem gives
 
 \[
 \sum_{L:\operatorname{row}(L)=r}A_LQ^L
@@ -99,8 +119,8 @@ multinomial bound
 \]
 
 The symmetric estimate holds after fixing \(c\).  Every row and column sum of
-\(Q\) is at most \(1+C\eta_n\), while the total number of selected blocks is at
-most \(k_{\mathrm{co}}\).  Hence
+\(Q\) is at most \(1+C\eta_n\), while every margin uses at most
+\(k_{\mathrm{co}}\) blocks.  Therefore
 
 \[
 \sum_LW(L)
@@ -109,7 +129,7 @@ most \(k_{\mathrm{co}}\).  Hence
 \tag{8.6}
 \]
 
-Lemma 7.1 gives \(\sum_rD(r)=1+o(1)\), and therefore
+Lemma 7.1 gives \(\sum_rD(r)=1+o(1)\), so
 
 \[
 \sum_LW(L)
@@ -120,57 +140,66 @@ Lemma 7.1 gives \(\sum_rD(r)=1+o(1)\), and therefore
 \tag{8.7}
 \]
 
-This proves the endpoint sum without Cauchy's inequality, without
-\((\sum_r\sqrt{D(r)})^2\), and without a polynomial count of margin vectors.
+Thus the endpoint sum needs neither a Cauchy inequality over the table family,
+nor \((\sum_r\sqrt{D(r)})^2\), nor a polynomial count of margin vectors.
+
+### 8.2 One geometric expansion for all high multiplicities
+
+Let a high cell join endpoint sizes \(m\) and \(m+d\), where \(0\le d\le3\),
+and write its multiplicity as
 
-### 8.2 All high multiplicities in one geometric expansion
+\[
+j=m-h.
+\]
 
-Let a high cell join endpoint sizes \(m\) and \(m+d\), \(0\le d\le3\), and
-write its multiplicity as \(j=m-e\).  Since \(j>R_0\ge\lfloor m/2\rfloor\),
+Since \(j>R_0\ge\lfloor m/2\rfloor\),
 
 \[
-2e<m.
+2h<m.
 \tag{8.8}
 \]
 
-Filling the cell from \(m-e\) to its endpoint multiplicity \(m\) changes the
+Filling the cell from \(m-h\) to its endpoint multiplicity \(m\) changes the
 local factor by the exact ratio
 
 \[
-R_{m,d}(e)
+R_{m,d}(h)
 =
-\frac{\binom me}{(d+1)\cdots(d+e)}
-2^{-em+e(e+1)/2}.
+\frac{\binom mh}{(d+1)\cdots(d+h)}
+2^{-hm+h(h+1)/2}.
 \tag{8.9}
 \]
 
-For several cells, if \(E=\sum e\), the single global denominator ratio is at
-most \(n^E\).  Thus each cell may be charged the factor
-\(A_{m,d}(e)=n^eR_{m,d}(e)\).
+For several cells, if \(H=\sum h\), the single global denominator ratio is at
+most \(n^H\).  Hence each cell may be charged
+
+\[
+A_{m,d}(h)=n^hR_{m,d}(h).
+\]
 
 The formalization-first integer estimate is
 
 \[
-e\left\lfloor\frac{2m}{3}\right\rfloor
+h\left\lfloor\frac{2m}{3}\right\rfloor
 \le
-em-\frac{e(e+1)}2
-\qquad(2e<m).
+hm-\frac{h(h+1)}2
+\qquad(2h<m).
 \tag{8.10}
 \]
 
-It is kernel-checked in PR #38.  Since
-\(inom me\le m^e\) and the denominator in (8.9) is at least one,
+PR #38 isolates this arithmetic statement.  Since
+\(inom mh\le m^h\), while the denominator in (8.9) is at least one,
 
 \[
-A_{m,d}(e)
+A_{m,d}(h)
 \le
 \left(
 \frac{nm}{2^{\lfloor2m/3\rfloor}}
-\right)^e.
+\right)^h.
 \tag{8.11}
 \]
 
-All endpoint sizes satisfy \(U-3\le m\le U\).  Put
+All endpoint sizes satisfy \(U-3\le m\le U\).  Set
 
 \[
 b_*:=\left\lfloor\frac{2(U-3)}3\right\rfloor,
@@ -187,13 +216,13 @@ The phase relation \(2^U=\Theta(n^2/N^2)\) gives
 \tag{8.12}
 \]
 
-Consequently the sum of all nonzero high deficits of one endpoint cell is at
-most \(2\rho_n\) eventually.  A high skeleton is a matching, so filling all its
-cells to their endpoints produces a feasible endpoint skeleton.  Conversely,
-an endpoint skeleton together with one allowed deficit per cell reconstructs
-the original high skeleton uniquely.  Distinguishing identical typed cells and
-then forgetting the labels is exactly the multinomial expansion; no further
-multiplicity is introduced.
+Thus the sum of all nonzero high deficits of one endpoint cell is at most
+\(2\rho_n\) eventually.  Because the high support is a matching, filling all
+its cells to their endpoints produces a feasible endpoint skeleton.
+Conversely, an endpoint skeleton together with one allowed deficit per cell
+reconstructs the original high skeleton uniquely.  Distinguishing identical
+typed cells and then forgetting the labels is exactly the multinomial
+expansion; no additional multiplicity appears.
 
 There are at most \(k_{\mathrm{co}}\) endpoint cells.  Therefore all high
 multiplicities cost at most
@@ -229,7 +258,7 @@ residual stub mass.  Its exact residual attachment is
 \mathcal A(\mathcal M,j)
 =
 \mathbb E_{\mathrm{res}}\!\left[
-\prod_e g(r'_e)
+\prod_{a,b} g(r'_{ab})
 2^{\beta(\mathcal M\cup H_{\mathrm{res}})}
 \mathbf1_{\mathcal E(\mathcal M,j)}
 \right].
@@ -239,7 +268,7 @@ residual stub mass.  Its exact residual attachment is
 For cells outside \(\mathcal M\), set
 
 \[
-\theta_{ab}=\frac{e\,d_ad'_b}{m_0},
+\theta_{ab}=\frac{\mathrm e\,d_ad'_b}{m_0},
 \qquad
 q_{ab}
 =
@@ -252,16 +281,16 @@ q_{ab}
 
 and put \(q_{ab}=0\) on \(\mathcal M\).
 
-The threshold expansion for a fixed even edge set \(F\) is bounded by a product
-of selected \(q\)-weights and unselected local increments.  Every local
-increment is at most \(q_{ab}\).  Hence
+The threshold expansion for a fixed even edge set \(F\) is bounded by selected
+\(q\)-weights and unselected local increments.  Every local increment is at
+most \(q_{ab}\).  Hence
 
 \[
 \mathcal A(\mathcal M,j)
 \le
-\left(\prod_{e\notin\mathcal M}(1+q_e)\right)
+\left(\prod_{(a,b)\notin\mathcal M}(1+q_{ab})\right)
 \sum_{F\text{ even}}
-\prod_{e\in F\setminus\mathcal M}q_e.
+\prod_{(a,b)\in F\setminus\mathcal M}q_{ab}.
 \tag{9.3}
 \]
 
@@ -271,41 +300,41 @@ subset of a matching, and the only such subset is empty.  Therefore
 
 \[
 \sum_{F\text{ even}}
-\prod_{e\in F\setminus\mathcal M}q_e
+\prod_{(a,b)\in F\setminus\mathcal M}q_{ab}
 \le
-\prod_{e\notin\mathcal M}(1+q_e).
+\prod_{(a,b)\notin\mathcal M}(1+q_{ab}).
 \tag{9.4}
 \]
 
-Combining (9.3)--(9.4),
+Combining (9.3) and (9.4),
 
 \[
 \boxed{
 \mathcal A(\mathcal M,j)
 \le
-\exp\left(2\sum_eq_e\right).}
+\exp\left(2\sum_{a,b}q_{ab}\right).}
 \tag{9.5}
 \]
 
 ### 9.1 Intrinsic quadratic regime
 
-If
+Assume
 
 \[
-2^U\le m_0^3,
+2^U\le m_0^3.
 \tag{9.6}
 \]
 
-then the finite endpoint estimate gives \(q_{ab}\le C\theta_{ab}^2\).  The
-square mass factorizes exactly:
+The finite endpoint estimate gives \(q_{ab}\le C\theta_{ab}^2\).  Moreover,
 
 \[
 \sum_{a,b}\theta_{ab}^2
 =
-\frac{e^2}{m_0^2}
+\frac{\mathrm e^2}{m_0^2}
 \left(\sum_ad_a^2\right)
 \left(\sum_b(d'_b)^2\right)
-\le e^2U^2.
+\le
+\mathrm e^2U^2.
 \tag{9.7}
 \]
 
@@ -319,19 +348,19 @@ Thus
 \tag{9.8}
 \]
 
-PR #37 kernel-checks the finite q-only bound and its attained-profile
+PR #37 formalizes the finite q-only bound and its attained-profile
 specialization.
 
 ### 9.2 Complementary small-power regime
 
-If (9.6) fails, the exact arithmetic dichotomy in PR #37 gives
+If (9.6) fails, the exact arithmetic dichotomy gives
 
 \[
 m_0<2^{\lceil U/3\rceil}.
 \tag{9.9}
 \]
 
-The deterministic residual estimate gives
+The deterministic residual estimate then yields
 
 \[
 \mathcal A(\mathcal M,j)
@@ -341,10 +370,9 @@ The deterministic residual estimate gives
 \tag{9.10}
 \]
 
-Since \(U=(2+o(1))\log_2n\), the exponent in (9.10) is
-\(n^{2/3+o(1)}\), and hence is \(o(n/N^4)\).  Together with (9.8), there is a
-deterministic sequence \(\varepsilon_n\to0\) such that uniformly over all
-attained high skeletons,
+Since \(U=(2+o(1))\log_2n\), this exponent is \(n^{2/3+o(1)}\), and hence is
+\(o(n/N^4)\).  Together with (9.8), there is a deterministic sequence
+\(arepsilon_n\to0\) such that uniformly over all attained high skeletons,
 
 \[
 \boxed{
@@ -354,10 +382,10 @@ attained high skeletons,
 \tag{9.11}
 \]
 
-This regime split is intrinsic to the finite q estimate and avoids introducing
-the auxiliary threshold \(n/N^6\).
+This split is intrinsic to the finite \(q\)-estimate and avoids the auxiliary
+threshold \(n/N^6\).
 
-## 9.3 Completion of the normalized second moment
+### 9.3 Completion of the normalized second moment
 
 The exact canonical decomposition gives
 
@@ -374,34 +402,35 @@ The exact canonical decomposition gives
 Equations (8.14) and (9.11) imply
 
 \[
+\boxed{
 \frac{\mathbb E(Z_k^{\mathrm{sgn}})^2}
      {(\mathbb EZ_k^{\mathrm{sgn}})^2}
 \le
-\exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}.
+\exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}.}
 \tag{9.13}
 \]
 
 This is the normalized second-moment estimate required by the seed and
 amplification argument.
 
-## Formalization map
+## Formalization map and remaining boundary
 
-The concise route is supported by the following focused developments:
+The concise route is supported by:
 
-- PR #34: matching-restriction injectivity and subset-product bound;
-- PR #35: literal attachment, attained-profile transport, and
-  `exp(O((log n)^2))` specialization;
-- PR #36: square-free endpoint transportation core;
-- PR #37: q-only absorption and intrinsic finite residual dichotomy;
-- PR #38: one all-high-deficit parametrization, its injectivity, and the
-  two-thirds exponent budget.
+- PR #34: matching-restriction injectivity and the finite subset-product bound;
+- PR #35: literal attachment, attained-profile transport, and the
+  \(\exp(O(N^2))\) large-residual specialization;
+- PR #36: square-free endpoint transportation;
+- PR #37: q-only absorption and the intrinsic finite residual dichotomy;
+- PR #38: square-free AM--GM linearization, one all-high-deficit
+  parametrization, and the two-thirds exponent budget.
 
 The remaining formal work is concentrated in two bridges:
 
-1. derive the linear endpoint inequality (8.4) from the square-free theorem and
-   sum it through the exact physical/type-table quotient;
-2. transport the local geometric bound (8.11) through the physical endpoint
-   decoration map and prove its phase-uniform asymptotic form.
+1. transport (8.4) through the exact physical/type-table quotient and sum it
+   by the one-sided multinomial expansions;
+2. prove (8.11) in the repository's `ENNReal` language and transport the
+   resulting decoration product through the physical endpoint-skeleton map.
 
-Those two obligations are considerably narrower than the current separate
-endpoint, near, middle, residual-cycle, and cubic-moment proof branches.
+These are narrower obligations than the present separate endpoint, near,
+middle, residual-cycle, and cubic-moment branches.

From 07ecb82e83124f34b15ae44b9f82598b90156988 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:45:03 +0300
Subject: [PATCH 15/34] Cancel obsolete Section 8 simplification runs

---
 .../workflows/erdos625-sections8-9-simplification-check.yml   | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index a4320710..1a26a534 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -13,6 +13,10 @@ on:
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"
   workflow_dispatch:
 
+concurrency:
+  group: erdos625-sections8-9-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

From fe39a42ea39957770135851be485675959cd8f26 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:48:27 +0300
Subject: [PATCH 16/34] Remove a control character from the concise replacement

---
 625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
index 18861e6c..7239fdfd 100644
--- a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
+++ b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
@@ -187,8 +187,9 @@ hm-\frac{h(h+1)}2
 \tag{8.10}
 \]
 
-PR #38 isolates this arithmetic statement.  Since
-\(inom mh\le m^h\), while the denominator in (8.9) is at least one,
+PR #38 isolates this arithmetic statement.  The elementary bound on the
+binomial coefficient is \(inom mh\le m^h\), while the denominator in (8.9) is
+at least one.  Hence
 
 \[
 A_{m,d}(h)

From 761871f0457e8e6c297e361b4ab6dd3dd13acf26 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:49:57 +0300
Subject: [PATCH 17/34] Fix the remaining Markdown control character

---
 625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
index 7239fdfd..d09ad97e 100644
--- a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
+++ b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
@@ -187,9 +187,8 @@ hm-\frac{h(h+1)}2
 \tag{8.10}
 \]
 
-PR #38 isolates this arithmetic statement.  The elementary bound on the
-binomial coefficient is \(inom mh\le m^h\), while the denominator in (8.9) is
-at least one.  Hence
+PR #38 isolates this arithmetic statement.  The binomial coefficient in
+(8.9) is at most \(m^h\), while its denominator is at least one.  Hence
 
 \[
 A_{m,d}(h)

From 2ca244b1d5a8d83530f5d3602e9ada3d353cc5ac Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:55:09 +0300
Subject: [PATCH 18/34] Clarify the physical decoration count in the concise
 replacement

---
 625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md | 297 +++++++++---------
 1 file changed, 144 insertions(+), 153 deletions(-)

diff --git a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
index d09ad97e..c1d93aba 100644
--- a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
+++ b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
@@ -1,260 +1,250 @@
 # Concise replacement draft for Sections 8 and 9
 
 This draft records the shortest proof route currently supported by the focused
-review PRs.  It keeps the exact canonical exposure but removes four separate
-layers of machinery:
+review PRs. It keeps the exact canonical exposure but removes four layers of
+machinery:
 
 - the table-family Cauchy inequality;
 - the near/middle high-cell split;
 - the residual configuration-model argument inside Section 8;
-- the cycle decomposition and separate cubic lambda estimate in Section 9.
-
-The notation is chosen to avoid collisions.  We use \(U=\alpha-2\) for the
-largest block size, \(\mathcal M\) for the exposed matching, \(h\) for an endpoint
-deficit, \(m_0\) for residual mass, and \(\mathrm e\) for Euler's number.
+- the cycle decomposition and separate cubic-lambda estimate in Section 9.
 
+The notation is chosen to avoid collisions. We use $U=\alpha-2$ for the
+largest block size, $\mathcal M$ for the exposed matching, $h$ for a local
+endpoint deficit, $m_0$ for residual mass, and $\mathrm e$ for Euler's number.
 Throughout,
 
-\[
-N=\ln n,
-\qquad
-U=\alpha-2,
-\qquad
-R_0=\lfloor U/2\rfloor,
-\]
+$$
+N=\ln n,\qquad U=\alpha-2,\qquad R_0=\lfloor U/2\rfloor,
+$$
 
-and the four block sizes are \(u_i=U-i\), \(0\le i\le3\).
+and the four block sizes are $u_i=U-i$, $0\le i\le3$.
 
 ## 8. Canonical high cells
 
-For an overlap table \(r=(r_{ab})\), define
+For an overlap table $r=(r_{ab})$, define
 
-\[
+$$
 \mathcal M(r)=\{(a,b):r_{ab}>R_0\}.
-\]
+$$
 
-Every row and column sum is at most \(U\), so \(\mathcal M(r)\) is a bipartite
-matching.  Write its cell multiplicities as \(j_{ab}=r_{ab}\), and put
+Every row and column sum is at most $U$, so $\mathcal M(r)$ is a bipartite
+matching. Write its cell multiplicities as $j_{ab}=r_{ab}$, and put
+$J=\sum_{(a,b)\in\mathcal M}j_{ab}$. Exposing the corresponding stub pairs has
+incidence
 
-\[
-J=\sum_{(a,b)\in\mathcal M}j_{ab}.
-\]
-
-Exposing the corresponding stub pairs has incidence
-
-\[
+$$
 \pi(\mathcal M,j)
 =
 \frac{\prod_{(a,b)\in\mathcal M}
       (s_a)_{j_{ab}}(t_b)_{j_{ab}}}
      {(n)_J\prod_{(a,b)\in\mathcal M}j_{ab}!}.
 \tag{8.1}
-\]
+$$
 
 Conditional on those pairs, the remaining matching is uniform with the induced
-residual degrees, is zero on \(\mathcal M\), and is capped by \(R_0\).
-Multiplying (8.1) by the exact residual configuration-table law recovers the
-original overlap probability.  Thus the decomposition is exact and every
-overlap table occurs once.
+residual degrees, is zero on $\mathcal M$, and is capped by $R_0$. Multiplying
+(8.1) by the exact residual configuration-table law recovers the original
+overlap probability. Thus the decomposition is exact and every overlap table
+occurs once.
 
 ### 8.1 Endpoint transportation without a global Cauchy step
 
-First suppose that every high cell is a full-containment cell.  Aggregate the
-physical block pairs by endpoint type into a table
-\(L=(\ell_{ij})_{0\le i,j\le3}\).  Let
+First suppose every high cell is a full-containment cell. Aggregate the selected
+block pairs by endpoint type into $L=(\ell_{ij})_{0\le i,j\le3}$. Let
 
-\[
-r_i=\sum_j\ell_{ij},
-\qquad
-c_j=\sum_i\ell_{ij},
-\]
+$$
+r_i=\sum_j\ell_{ij},\qquad c_j=\sum_i\ell_{ij},
+$$
 
-and let \(W(L)\) denote its exact endpoint incidence and local signed reward.
-Let \(D(r)\) be the common-subprofile weight from Section 7, and define
+and let $W(L)$ be the exact endpoint incidence and local signed reward. Let
+$D(r)$ be the common-subprofile weight from Section 7, and define
 
-\[
+$$
 A_L=\frac{\prod_i r_i!}{\prod_{ij}\ell_{ij}!},
 \qquad
 C_L=\frac{\prod_j c_j!}{\prod_{ij}\ell_{ij}!}.
-\]
+$$
 
 The endpoint transport calculation gives
 
-\[
+$$
 W(L)
 \le
 \sqrt{D(r)A_L\,D(c)C_L}\,Q^L,
 \qquad
 Q^L=\prod_{ij}Q_{ij}^{\ell_{ij}},
 \tag{8.2}
-\]
+$$
 
-where \(Q_{ii}=1\), and for \(d=|i-j|\in\{1,2,3\}\),
+where $Q_{ii}=1$, and for $d=|i-j|\in\{1,2,3\}$,
 
-\[
+$$
 Q_{ij}\le\frac{\eta_n^d}{d!},
 \qquad
 \eta_n=O\!\left(\frac{N^{3/2}}{\sqrt n}\right).
 \tag{8.3}
-\]
+$$
 
-PR #36 proves the square-free finite algebra underlying (8.2).  For the table
-sum, apply \(2\sqrt{xy}\le x+y\) term by term:
+PR #36 proves the square-free finite algebra underlying (8.2). For the table
+sum, apply $2\sqrt{xy}\le x+y$ termwise:
 
-\[
+$$
 W(L)
 \le
 \frac12\bigl(D(r)A_L+D(c)C_L\bigr)Q^L.
 \tag{8.4}
-\]
+$$
 
-Fix \(r\).  Dropping only the column-margin constraint and using the
-multinomial theorem gives
+Fix $r$. Dropping only the column-margin constraint and using the multinomial
+theorem gives
 
-\[
+$$
 \sum_{L:\operatorname{row}(L)=r}A_LQ^L
 \le
 \prod_i\left(\sum_jQ_{ij}\right)^{r_i}.
 \tag{8.5}
-\]
+$$
 
-The symmetric estimate holds after fixing \(c\).  Every row and column sum of
-\(Q\) is at most \(1+C\eta_n\), while every margin uses at most
-\(k_{\mathrm{co}}\) blocks.  Therefore
+The symmetric estimate holds after fixing $c$. Every row and column sum of $Q$
+is at most $1+C\eta_n$, while every margin uses at most $k_{\mathrm{co}}$
+blocks. Therefore
 
-\[
+$$
 \sum_LW(L)
 \le
 (1+C\eta_n)^{k_{\mathrm{co}}}\sum_rD(r).
 \tag{8.6}
-\]
+$$
 
-Lemma 7.1 gives \(\sum_rD(r)=1+o(1)\), so
+Lemma 7.1 gives $\sum_rD(r)=1+o(1)$, so
 
-\[
+$$
 \sum_LW(L)
 \le
 \exp\{O(\eta_nk_{\mathrm{co}})\}
 =
 \exp\{O(\sqrt{nN})\}.
 \tag{8.7}
-\]
+$$
 
 Thus the endpoint sum needs neither a Cauchy inequality over the table family,
-nor \((\sum_r\sqrt{D(r)})^2\), nor a polynomial count of margin vectors.
+nor $(\sum_r\sqrt{D(r)})^2$, nor a polynomial count of margin vectors.
 
-### 8.2 One geometric expansion for all high multiplicities
+### 8.2 One decorated-cell expansion for all high multiplicities
 
-Let a high cell join endpoint sizes \(m\) and \(m+d\), where \(0\le d\le3\),
-and write its multiplicity as
+Fix one selected block pair whose endpoint sizes are $m$ and $m+d$, with
+$0\le d\le3$. A high multiplicity has the form
 
-\[
+$$
 j=m-h.
-\]
+$$
 
-Since \(j>R_0\ge\lfloor m/2\rfloor\),
+Since $j>R_0\ge\lfloor m/2\rfloor$, we have
 
-\[
+$$
 2h<m.
 \tag{8.8}
-\]
+$$
 
-Filling the cell from \(m-h\) to its endpoint multiplicity \(m\) changes the
-local factor by the exact ratio
+The relevant object is not merely the number $h$. A **cell decoration** consists
+of a literal single-cell stub matching of size $m-h$. We sum all such
+decorations by their exact cardinality and signed local reward. Comparing that
+weighted cardinality with the full endpoint cell gives the exact ratio
 
-\[
+$$
 R_{m,d}(h)
 =
 \frac{\binom mh}{(d+1)\cdots(d+h)}
 2^{-hm+h(h+1)/2}.
 \tag{8.9}
-\]
+$$
 
-For several cells, if \(H=\sum h\), the single global denominator ratio is at
-most \(n^H\).  Hence each cell may be charged
+Thus no unique physical completion is claimed or needed: the missing-stub and
+pairing multiplicities are already contained in the ratio (8.9). For several
+selected block pairs, the block-pair support is a matching, so the local stub
+decorations are independent. If $H=\sum h$, the single global denominator ratio
+is at most $n^H$. Hence each decorated cell may be charged
 
-\[
+$$
 A_{m,d}(h)=n^hR_{m,d}(h).
-\]
+$$
 
 The formalization-first integer estimate is
 
-\[
+$$
 h\left\lfloor\frac{2m}{3}\right\rfloor
 \le
 hm-\frac{h(h+1)}2
 \qquad(2h<m).
 \tag{8.10}
-\]
+$$
 
-PR #38 isolates this arithmetic statement.  The binomial coefficient in
-(8.9) is at most \(m^h\), while its denominator is at least one.  Hence
+PR #38 isolates this arithmetic statement. The binomial coefficient in (8.9)
+is at most $m^h$, while its denominator is at least one. Hence
 
-\[
+$$
 A_{m,d}(h)
 \le
-\left(
-\frac{nm}{2^{\lfloor2m/3\rfloor}}
-\right)^h.
+\left(\frac{nm}{2^{\lfloor2m/3\rfloor}}\right)^h.
 \tag{8.11}
-\]
+$$
 
-All endpoint sizes satisfy \(U-3\le m\le U\).  Set
+All endpoint sizes satisfy $U-3\le m\le U$. Set
 
-\[
+$$
 b_*:=\left\lfloor\frac{2(U-3)}3\right\rfloor,
 \qquad
 \rho_n:=\frac{nU}{2^{b_*}}.
-\]
+$$
 
-The phase relation \(2^U=\Theta(n^2/N^2)\) gives
+The phase relation $2^U=\Theta(n^2/N^2)$ gives
 
-\[
+$$
 \rho_n
 =O\!\left(\frac{N^{7/3}}{n^{1/3}}\right)
 =o(1).
 \tag{8.12}
-\]
+$$
 
-Thus the sum of all nonzero high deficits of one endpoint cell is at most
-\(2\rho_n\) eventually.  Because the high support is a matching, filling all
-its cells to their endpoints produces a feasible endpoint skeleton.
-Conversely, an endpoint skeleton together with one allowed deficit per cell
-reconstructs the original high skeleton uniquely.  Distinguishing identical
-typed cells and then forgetting the labels is exactly the multinomial
-expansion; no additional multiplicity appears.
+For every selected endpoint block pair, summing over all nonzero high deficits
+and all corresponding stub decorations contributes at most $2\rho_n$ times the
+full-cell weight, eventually. Distinguish the selected block pairs, apply the
+exact product expansion over their allowed decorations, and only then group
+identical endpoint types. The existing block-pairing factorials perform that
+grouping; there is no additional unlabelled multiplicity.
 
-There are at most \(k_{\mathrm{co}}\) endpoint cells.  Therefore all high
+There are at most $k_{\mathrm{co}}$ selected block pairs. Therefore all high
 multiplicities cost at most
 
-\[
+$$
 (1+2\rho_n)^{k_{\mathrm{co}}}
 \le
 \exp\{O(k_{\mathrm{co}}\rho_n)\}
 =
 \exp\{O(n^{2/3}N^{4/3})\}.
 \tag{8.13}
-\]
+$$
 
 Combining (8.7) and (8.13),
 
-\[
+$$
 \boxed{
 \sum_{(\mathcal M,j)}w_{\mathrm{hi}}(\mathcal M,j)
 \le
 \exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}.}
 \tag{8.14}
-\]
+$$
 
 No near/middle partition or residual configuration-model argument is needed in
 Section 8.
 
 ## 9. Residual attachment
 
-Fix an attained high skeleton \((\mathcal M,j)\), and let \(m_0=n-J\) be its
-residual stub mass.  Its exact residual attachment is
+Fix an attained high skeleton $(\mathcal M,j)$, and let $m_0=n-J$ be its
+residual stub mass. Its exact residual attachment is
 
-\[
+$$
 \mathcal A(\mathcal M,j)
 =
 \mathbb E_{\mathrm{res}}\!\left[
@@ -263,11 +253,11 @@ residual stub mass.  Its exact residual attachment is
 \mathbf1_{\mathcal E(\mathcal M,j)}
 \right].
 \tag{9.1}
-\]
+$$
 
-For cells outside \(\mathcal M\), set
+For cells outside $\mathcal M$, set
 
-\[
+$$
 \theta_{ab}=\frac{\mathrm e\,d_ad'_b}{m_0},
 \qquad
 q_{ab}
@@ -277,57 +267,57 @@ q_{ab}
 \sum_{x=3}^{R_0}\bigl(g(x)-g(x-1)\bigr)
 \frac{\theta_{ab}^x}{x!},
 \tag{9.2}
-\]
+$$
 
-and put \(q_{ab}=0\) on \(\mathcal M\).
+and put $q_{ab}=0$ on $\mathcal M$.
 
-The threshold expansion for a fixed even edge set \(F\) is bounded by selected
-\(q\)-weights and unselected local increments.  Every local increment is at
-most \(q_{ab}\).  Hence
+The threshold expansion for a fixed even edge set $F$ is bounded by selected
+$q$-weights and unselected local increments. Every local increment is at most
+$q_{ab}$. Hence
 
-\[
+$$
 \mathcal A(\mathcal M,j)
 \le
 \left(\prod_{(a,b)\notin\mathcal M}(1+q_{ab})\right)
 \sum_{F\text{ even}}
 \prod_{(a,b)\in F\setminus\mathcal M}q_{ab}.
 \tag{9.3}
-\]
+$$
 
-The restriction map \(F\mapsto F\setminus\mathcal M\) is injective on even edge
+The restriction map $F\mapsto F\setminus\mathcal M$ is injective on even edge
 sets: two completions with the same residual restriction differ by an even
-subset of a matching, and the only such subset is empty.  Therefore
+subset of a matching, and the only such subset is empty. Therefore
 
-\[
+$$
 \sum_{F\text{ even}}
 \prod_{(a,b)\in F\setminus\mathcal M}q_{ab}
 \le
 \prod_{(a,b)\notin\mathcal M}(1+q_{ab}).
 \tag{9.4}
-\]
+$$
 
 Combining (9.3) and (9.4),
 
-\[
+$$
 \boxed{
 \mathcal A(\mathcal M,j)
 \le
 \exp\left(2\sum_{a,b}q_{ab}\right).}
 \tag{9.5}
-\]
+$$
 
 ### 9.1 Intrinsic quadratic regime
 
 Assume
 
-\[
+$$
 2^U\le m_0^3.
 \tag{9.6}
-\]
+$$
 
-The finite endpoint estimate gives \(q_{ab}\le C\theta_{ab}^2\).  Moreover,
+The finite endpoint estimate gives $q_{ab}\le C\theta_{ab}^2$. Moreover,
 
-\[
+$$
 \sum_{a,b}\theta_{ab}^2
 =
 \frac{\mathrm e^2}{m_0^2}
@@ -336,17 +326,17 @@ The finite endpoint estimate gives \(q_{ab}\le C\theta_{ab}^2\).  Moreover,
 \le
 \mathrm e^2U^2.
 \tag{9.7}
-\]
+$$
 
 Thus
 
-\[
+$$
 \boxed{
 \mathcal A(\mathcal M,j)
 \le\exp(CU^2)
 =\exp(O(N^2)).}
 \tag{9.8}
-\]
+$$
 
 PR #37 formalizes the finite q-only bound and its attained-profile
 specialization.
@@ -355,41 +345,41 @@ specialization.
 
 If (9.6) fails, the exact arithmetic dichotomy gives
 
-\[
+$$
 m_0<2^{\lceil U/3\rceil}.
 \tag{9.9}
-\]
+$$
 
 The deterministic residual estimate then yields
 
-\[
+$$
 \mathcal A(\mathcal M,j)
 \le2^{Um_0/2}
 \le
 \exp\{O(U2^{U/3})\}.
 \tag{9.10}
-\]
+$$
 
-Since \(U=(2+o(1))\log_2n\), this exponent is \(n^{2/3+o(1)}\), and hence is
-\(o(n/N^4)\).  Together with (9.8), there is a deterministic sequence
-\(arepsilon_n\to0\) such that uniformly over all attained high skeletons,
+Since $U=(2+o(1))\log_2n$, this exponent is $n^{2/3+o(1)}$, and hence is
+$o(n/N^4)$. Together with (9.8), there is a deterministic sequence
+$\varepsilon_n\to0$ such that uniformly over all attained high skeletons,
 
-\[
+$$
 \boxed{
 \mathcal A(\mathcal M,j)
 \le
 \exp\!\left\{\varepsilon_n\frac n{N^4}\right\}.}
 \tag{9.11}
-\]
+$$
 
-This split is intrinsic to the finite \(q\)-estimate and avoids the auxiliary
-threshold \(n/N^6\).
+This split is intrinsic to the finite $q$-estimate and avoids the auxiliary
+threshold $n/N^6$.
 
 ### 9.3 Completion of the normalized second moment
 
 The exact canonical decomposition gives
 
-\[
+$$
 \frac{\mathbb E(Z_k^{\mathrm{sgn}})^2}
      {(\mathbb EZ_k^{\mathrm{sgn}})^2}
 =
@@ -397,18 +387,18 @@ The exact canonical decomposition gives
  w_{\mathrm{hi}}(\mathcal M,j)
  \mathcal A(\mathcal M,j).
 \tag{9.12}
-\]
+$$
 
 Equations (8.14) and (9.11) imply
 
-\[
+$$
 \boxed{
 \frac{\mathbb E(Z_k^{\mathrm{sgn}})^2}
      {(\mathbb EZ_k^{\mathrm{sgn}})^2}
 \le
 \exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}.}
 \tag{9.13}
-\]
+$$
 
 This is the normalized second-moment estimate required by the seed and
 amplification argument.
@@ -419,7 +409,7 @@ The concise route is supported by:
 
 - PR #34: matching-restriction injectivity and the finite subset-product bound;
 - PR #35: literal attachment, attained-profile transport, and the
-  \(\exp(O(N^2))\) large-residual specialization;
+  $\exp(O(N^2))$ large-residual specialization;
 - PR #36: square-free endpoint transportation;
 - PR #37: q-only absorption and the intrinsic finite residual dichotomy;
 - PR #38: square-free AM--GM linearization, one all-high-deficit
@@ -429,8 +419,9 @@ The remaining formal work is concentrated in two bridges:
 
 1. transport (8.4) through the exact physical/type-table quotient and sum it
    by the one-sided multinomial expansions;
-2. prove (8.11) in the repository's `ENNReal` language and transport the
-   resulting decoration product through the physical endpoint-skeleton map.
+2. prove the decorated-cell ratio bound (8.11) in the repository's `ENNReal`
+   language and transport the resulting product through the exact block-pair
+   and single-cell stub-matching cardinalities.
 
 These are narrower obligations than the present separate endpoint, near,
 middle, residual-cycle, and cubic-moment branches.

From 976436aea148a9d29a7da4be6b3f60e8738d1baa Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:18:35 +0300
Subject: [PATCH 19/34] Fix warning-fatal square-free AM-GM helper

---
 625/formalization/Erdos625/Section8SquareFreeAMGM.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/625/formalization/Erdos625/Section8SquareFreeAMGM.lean b/625/formalization/Erdos625/Section8SquareFreeAMGM.lean
index 6ea68a2e..83c2b6eb 100644
--- a/625/formalization/Erdos625/Section8SquareFreeAMGM.lean
+++ b/625/formalization/Erdos625/Section8SquareFreeAMGM.lean
@@ -13,12 +13,13 @@ namespace Erdos625
 
 set_option autoImplicit false
 
-/-- A nonnegative square-product bound linearizes by AM--GM without taking a
-square root.  This is the abstract bridge used after the endpoint factorial
-normalizations have been exposed. -/
+/-- A square-product bound linearizes by AM--GM without taking a square root.
+The explicit nonnegativity assumptions on `y` and `z` match the endpoint
+application; nonnegativity of `x` is not logically needed but is retained as an
+interface hypothesis. -/
 theorem two_mul_le_add_of_sq_le_mul
     (x y z : Real)
-    (hx : 0 <= x) (hy : 0 <= y) (hz : 0 <= z)
+    (_hx : 0 <= x) (hy : 0 <= y) (hz : 0 <= z)
     (h : x ^ 2 <= y * z) :
     2 * x <= y + z := by
   have hsq : (2 * x) ^ 2 <= (y + z) ^ 2 := by

From 40ecbcb9aa0580e519f12c8f977a751d51e98173 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:30:07 +0300
Subject: [PATCH 20/34] Connect all high deficits to the literal one-cell
 weight

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

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
new file mode 100644
index 00000000..29102556
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
@@ -0,0 +1,128 @@
+import Erdos625.Section8NearCellChoiceLink
+import Erdos625.Section8AllHighDeficitArithmetic
+import Mathlib.Tactic
+
+/-!
+# Section VIII: literal all-high one-cell weight bound
+
+This module connects the all-high deficit parametrization to the repository's
+literal one-cell stub-matching weight `nearCellTerm`.  Despite the historical
+name, the same exact local weight applies to every endpoint deficit above the
+high-cell cutoff.
+
+The main result charges one physical deficit `e` by a single geometric base.
+It does not yet multiply the bound over an endpoint block pairing or perform
+the phase asymptotics.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Geometric base used for one all-high endpoint deficit. -/
+def allHighCellBase (n m : Nat) : ENNReal :=
+  (n : ENNReal) * (m : ENNReal) /
+    (2 : ENNReal) ^ ((2 * m) / 3)
+
+/-- The literal finite choices for every nonzero endpoint deficit compatible
+with the strict global high-cell cutoff. -/
+def allHighCellAllowed (a m : Nat) : Fin 1 → Finset (Fin (m + 1)) :=
+  nearCellAllowed m (allHighDeficitCut a m)
+
+/-- Exact optional-deficit expansion for one distinguishable endpoint cell over
+the full high range. -/
+theorem allHighCellChoiceExpansion
+    (n a m d : Nat) :
+    (∑ choice : NearSkeletonChoice (Fin 1) (Fin (m + 1))
+        (allHighCellAllowed a m),
+      nearSkeletonChoiceWeight (allHighCellAllowed a m)
+        (nearCellWeight n m d (allHighDeficitCut a m)) choice) =
+      1 + ∑ q ∈ allHighCellAllowed a m 0,
+        nearCellTerm n m d q.1 := by
+  rw [sum_nearSkeletonChoiceWeight_eq_product]
+  simp [allHighCellAllowed, nearCellWeight]
+
+/-- The exact charged local stub-matching weight is bounded by one power of the
+all-high geometric base whenever the deficit is below half the endpoint size. -/
+theorem nearCellTerm_le_allHighCellBase_pow
+    (n m d e : Nat) (hhalf : 2 * e < m) :
+    nearCellTerm n m d e ≤ allHighCellBase n m ^ e := by
+  let den : Nat := ∏ t ∈ Finset.Icc 1 e, d + t
+  let exponent : Nat := e * m - e * (e + 1) / 2
+  let budget : Nat := (2 * m) / 3
+  have hdenPos : 0 < den := by
+    dsimp [den]
+    apply Finset.prod_pos
+    intro t ht
+    omega
+  have hdenOne : 1 ≤ den := Nat.one_le_iff_ne_zero.mpr hdenPos.ne'
+  have hdenZero : (den : ENNReal) ≠ 0 := by
+    exact_mod_cast hdenPos.ne'
+  have hdenTop : (den : ENNReal) ≠ ∞ := ENNReal.natCast_ne_top den
+  have hchooseNat : Nat.choose m e ≤ m ^ e := Nat.choose_le_pow m e
+  have hchoose : (Nat.choose m e : ENNReal) ≤ (m : ENNReal) ^ e := by
+    exact_mod_cast hchooseNat
+  have hdiv :
+      ((n : ENNReal) ^ e * (Nat.choose m e : ENNReal)) /
+          (den : ENNReal) ≤
+        (n : ENNReal) ^ e * (Nat.choose m e : ENNReal) := by
+    apply (ENNReal.div_le_iff_le_mul (Or.inl hdenZero) (Or.inl hdenTop)).2
+    exact le_mul_of_one_le_right bot_le (by exact_mod_cast hdenOne)
+  have hfirst :
+      ((n : ENNReal) ^ e * (Nat.choose m e : ENNReal)) /
+          (den : ENNReal) ≤
+        (n : ENNReal) ^ e * (m : ENNReal) ^ e :=
+    hdiv.trans (mul_le_mul_left' hchoose _)
+  have hbudgetNat : e * budget ≤ exponent := by
+    dsimp [budget, exponent]
+    exact highDeficit_twoThird_exponent_budget m e hhalf
+  have hpowNat : 2 ^ (e * budget) ≤ 2 ^ exponent :=
+    Nat.pow_le_pow_right (by decide) hbudgetNat
+  have hpow :
+      (2 : ENNReal) ^ (e * budget) ≤ (2 : ENNReal) ^ exponent := by
+    exact_mod_cast hpowNat
+  have hinv :
+      ((2 : ENNReal) ^ exponent)⁻¹ ≤
+        ((2 : ENNReal) ^ (e * budget))⁻¹ := by
+    rw [ENNReal.inv_le_inv]
+    exact hpow
+  calc
+    nearCellTerm n m d e =
+        (((n : ENNReal) ^ e * (Nat.choose m e : ENNReal)) /
+          (den : ENNReal)) * ((2 : ENNReal) ^ exponent)⁻¹ := by
+      rfl
+    _ ≤ ((n : ENNReal) ^ e * (m : ENNReal) ^ e) *
+          ((2 : ENNReal) ^ (e * budget))⁻¹ :=
+      mul_le_mul' hfirst hinv
+    _ = allHighCellBase n m ^ e := by
+      simp [allHighCellBase, budget, div_eq_mul_inv, mul_pow, pow_mul,
+        Nat.mul_comm, mul_assoc, mul_comm, mul_left_comm]
+
+/-- Every allowed nonzero all-high deficit satisfies the hypothesis of the
+literal one-cell geometric bound. -/
+theorem nearCellTerm_le_allHighCellBase_pow_of_mem
+    (n a m d : Nat) (hm : m ≤ a) (hmHigh : a / 2 < m)
+    (e : Fin (m + 1))
+    (he : e ∈ allHighCellAllowed a m 0) :
+    nearCellTerm n m d e.1 ≤ allHighCellBase n m ^ e.1 := by
+  have heCut : e.1 ≤ allHighDeficitCut a m := by
+    simpa [allHighCellAllowed, nearCellAllowed] using he
+  have hjHigh := allHighDeficit_reconstructs_highMultiplicity a m e.1 hmHigh heCut
+  have heLe : e.1 ≤ m := by omega
+  have hhalf := highMultiplicity_deficit_twice_lt a m (m - e.1)
+    hm hjHigh (Nat.sub_le _ _)
+  have hreconstruct : m - (m - e.1) = e.1 := by omega
+  rw [hreconstruct] at hhalf
+  exact nearCellTerm_le_allHighCellBase_pow n m d e.1 hhalf
+
+#print axioms allHighCellChoiceExpansion
+#print axioms nearCellTerm_le_allHighCellBase_pow
+#print axioms nearCellTerm_le_allHighCellBase_pow_of_mem
+
+end
+
+end Erdos625

From 6ce264e099588b1f059ebb92b1530f2b6f5436be Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:30:48 +0300
Subject: [PATCH 21/34] Extend the Section 8 simplification core to literal
 cell weights

---
 .../Erdos625/Section8SimplificationCore.lean              | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/625/formalization/Erdos625/Section8SimplificationCore.lean b/625/formalization/Erdos625/Section8SimplificationCore.lean
index 947a103f..d620a2ae 100644
--- a/625/formalization/Erdos625/Section8SimplificationCore.lean
+++ b/625/formalization/Erdos625/Section8SimplificationCore.lean
@@ -1,10 +1,12 @@
 import Erdos625.Section8SquareFreeAMGM
 import Erdos625.Section8AllHighDeficitArithmetic
+import Erdos625.Section8AllHighDeficitCellWeight
 
 /-!
 # Section VIII simplification core
 
-This aggregate module checks the two finite bridges used by the shortened
-Section VIII route: square-free AM--GM linearization and one all-high-deficit
-parametrization with a uniform binary exponent budget.
+This aggregate module checks the finite bridges used by the shortened Section
+VIII route: square-free AM--GM linearization, one all-high-deficit
+parametrization, its uniform binary exponent budget, and the literal one-cell
+stub-matching weight bound over the full high range.
 -/

From d1c38ebcaf83971091f626ad1f828a0ed612ce02 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:31:47 +0300
Subject: [PATCH 22/34] Validate the literal all-high cell-weight bridge

---
 .../workflows/erdos625-sections8-9-simplification-check.yml   | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index 1a26a534..0fafa788 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -9,6 +9,7 @@ on:
       - "625/experiments/sections8_9_simplification_check.py"
       - "625/formalization/Erdos625/Section8SquareFreeAMGM.lean"
       - "625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean"
+      - "625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean"
       - "625/formalization/Erdos625/Section8SimplificationCore.lean"
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"
   workflow_dispatch:
@@ -43,6 +44,7 @@ jobs:
             '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
             625/formalization/Erdos625/Section8SquareFreeAMGM.lean \
             625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean \
+            625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean \
             625/formalization/Erdos625/Section8SimplificationCore.lean; then
             exit 1
           fi
@@ -62,7 +64,7 @@ jobs:
           lake build Erdos625.Section8SimplificationCore --wfail \
             > /tmp/section8-simplification-lean.log 2>&1
           status=$?
-          tail -n 260 /tmp/section8-simplification-lean.log
+          tail -n 340 /tmp/section8-simplification-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From 6891c41bc80fbfd683fd62d52feb8eec19e82837 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:38:15 +0300
Subject: [PATCH 23/34] Repair the literal all-high cell-weight proof seams

---
 .../Erdos625/Section8AllHighDeficitCellWeight.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
index 29102556..60860f10 100644
--- a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
+++ b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
@@ -51,7 +51,7 @@ all-high geometric base whenever the deficit is below half the endpoint size. -/
 theorem nearCellTerm_le_allHighCellBase_pow
     (n m d e : Nat) (hhalf : 2 * e < m) :
     nearCellTerm n m d e ≤ allHighCellBase n m ^ e := by
-  let den : Nat := ∏ t ∈ Finset.Icc 1 e, d + t
+  let den : Nat := ∏ t ∈ Finset.Icc 1 e, (d + t : Nat)
   let exponent : Nat := e * m - e * (e + 1) / 2
   let budget : Nat := (2 * m) / 3
   have hdenPos : 0 < den := by
@@ -76,7 +76,7 @@ theorem nearCellTerm_le_allHighCellBase_pow
       ((n : ENNReal) ^ e * (Nat.choose m e : ENNReal)) /
           (den : ENNReal) ≤
         (n : ENNReal) ^ e * (m : ENNReal) ^ e :=
-    hdiv.trans (mul_le_mul_left' hchoose _)
+    hdiv.trans (mul_le_mul_left hchoose _)
   have hbudgetNat : e * budget ≤ exponent := by
     dsimp [budget, exponent]
     exact highDeficit_twoThird_exponent_budget m e hhalf
@@ -94,13 +94,15 @@ theorem nearCellTerm_le_allHighCellBase_pow
     nearCellTerm n m d e =
         (((n : ENNReal) ^ e * (Nat.choose m e : ENNReal)) /
           (den : ENNReal)) * ((2 : ENNReal) ^ exponent)⁻¹ := by
-      rfl
+      simp only [nearCellTerm, den, exponent]
     _ ≤ ((n : ENNReal) ^ e * (m : ENNReal) ^ e) *
           ((2 : ENNReal) ^ (e * budget))⁻¹ :=
       mul_le_mul' hfirst hinv
     _ = allHighCellBase n m ^ e := by
+      have heb : e * budget = budget * e := Nat.mul_comm _ _
+      rw [heb]
       simp [allHighCellBase, budget, div_eq_mul_inv, mul_pow, pow_mul,
-        Nat.mul_comm, mul_assoc, mul_comm, mul_left_comm]
+        mul_assoc]
 
 /-- Every allowed nonzero all-high deficit satisfies the hypothesis of the
 literal one-cell geometric bound. -/
@@ -109,10 +111,10 @@ theorem nearCellTerm_le_allHighCellBase_pow_of_mem
     (e : Fin (m + 1))
     (he : e ∈ allHighCellAllowed a m 0) :
     nearCellTerm n m d e.1 ≤ allHighCellBase n m ^ e.1 := by
-  have heCut : e.1 ≤ allHighDeficitCut a m := by
+  have hmem : e.1 ∈ Finset.Icc 1 (allHighDeficitCut a m) := by
     simpa [allHighCellAllowed, nearCellAllowed] using he
+  have heCut : e.1 ≤ allHighDeficitCut a m := hmem.2
   have hjHigh := allHighDeficit_reconstructs_highMultiplicity a m e.1 hmHigh heCut
-  have heLe : e.1 ≤ m := by omega
   have hhalf := highMultiplicity_deficit_twice_lt a m (m - e.1)
     hm hjHigh (Nat.sub_le _ _)
   have hreconstruct : m - (m - e.1) = e.1 := by omega

From 8cd51bd0eb2744a2ffc7030e7c690863d242d63a Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:43:35 +0300
Subject: [PATCH 24/34] Resolve remaining literal all-high cell-weight proof
 errors

---
 .../Erdos625/Section8AllHighDeficitCellWeight.lean       | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
index 60860f10..d9b673af 100644
--- a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
+++ b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
@@ -58,6 +58,7 @@ theorem nearCellTerm_le_allHighCellBase_pow
     dsimp [den]
     apply Finset.prod_pos
     intro t ht
+    simp only [Finset.mem_Icc] at ht
     omega
   have hdenOne : 1 ≤ den := Nat.one_le_iff_ne_zero.mpr hdenPos.ne'
   have hdenZero : (den : ENNReal) ≠ 0 := by
@@ -76,7 +77,7 @@ theorem nearCellTerm_le_allHighCellBase_pow
       ((n : ENNReal) ^ e * (Nat.choose m e : ENNReal)) /
           (den : ENNReal) ≤
         (n : ENNReal) ^ e * (m : ENNReal) ^ e :=
-    hdiv.trans (mul_le_mul_left hchoose _)
+    hdiv.trans (mul_le_mul_right hchoose _)
   have hbudgetNat : e * budget ≤ exponent := by
     dsimp [budget, exponent]
     exact highDeficit_twoThird_exponent_budget m e hhalf
@@ -112,8 +113,10 @@ theorem nearCellTerm_le_allHighCellBase_pow_of_mem
     (he : e ∈ allHighCellAllowed a m 0) :
     nearCellTerm n m d e.1 ≤ allHighCellBase n m ^ e.1 := by
   have hmem : e.1 ∈ Finset.Icc 1 (allHighDeficitCut a m) := by
-    simpa [allHighCellAllowed, nearCellAllowed] using he
-  have heCut : e.1 ≤ allHighDeficitCut a m := hmem.2
+    simpa only [allHighCellAllowed, nearCellAllowed, Finset.mem_filter,
+      Finset.mem_univ, true_and] using he
+  have heCut : e.1 ≤ allHighDeficitCut a m :=
+    (Finset.mem_Icc.mp hmem).2
   have hjHigh := allHighDeficit_reconstructs_highMultiplicity a m e.1 hmHigh heCut
   have hhalf := highMultiplicity_deficit_twice_lt a m (m - e.1)
     hm hjHigh (Nat.sub_le _ _)

From f4ca028c5a10432ade31af8612ff8a4e4c436bd3 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:51:09 +0300
Subject: [PATCH 25/34] Synchronize the Section 8 checker with the two-thirds
 Lean budget

---
 .../sections8_9_simplification_check.py       | 85 ++++++++++++-------
 1 file changed, 53 insertions(+), 32 deletions(-)

diff --git a/625/experiments/sections8_9_simplification_check.py b/625/experiments/sections8_9_simplification_check.py
index 33fd204d..269d389c 100644
--- a/625/experiments/sections8_9_simplification_check.py
+++ b/625/experiments/sections8_9_simplification_check.py
@@ -2,14 +2,19 @@
 """Finite regression checks for the simplified Sections 8--9 route.
 
 The exact gates use only the Python standard library and remain active under
-``python -O``.  Floating-point phase scans are diagnostics and are labelled as
+``python -O``. Floating-point phase scans are diagnostics and are labelled as
 such; they are not used to certify an asymptotic theorem.
+
+The primary high-deficit gate follows the formalization-first exponent budget
+``floor(2m/3)`` used in Lean.  The earlier sharper ``floor((3m-1)/4)`` bound is
+also checked separately as a diagnostic, but it is not needed by the proposed
+replacement proof.
 """
 
 from __future__ import annotations
 
 from fractions import Fraction
-from math import comb, e, exp, lgamma, log, log2
+from math import comb, e, lgamma, log, log2
 
 
 def require(condition: bool, message: str) -> None:
@@ -32,45 +37,54 @@ def local_ratio_with_global_charge(n: int, m: int, d: int, deficit: int) -> Frac
     )
 
 
-def exact_high_deficit_checks() -> tuple[int, int]:
-    """Check the exact geometric domination used in (S8.5)--(S8.6)."""
+def exact_high_deficit_checks() -> tuple[int, int, int]:
+    """Check the formal two-thirds domination and the optional sharper budget."""
 
-    exponent_cases = 0
+    formal_exponent_cases = 0
+    sharper_exponent_cases = 0
     ratio_cases = 0
 
     for m in range(2, 601):
-        b_m = (3 * m - 1) // 4
+        b_formal = (2 * m) // 3
+        b_sharp = (3 * m - 1) // 4
         for deficit in range(1, m):
             if 2 * deficit >= m:
                 continue
 
             exponent = deficit * m - deficit * (deficit + 1) // 2
             require(
-                exponent >= deficit * b_m,
-                f"exponent budget failed: m={m}, e={deficit}",
+                exponent >= deficit * b_formal,
+                f"formal exponent budget failed: m={m}, e={deficit}",
             )
             require(
                 comb(m, deficit) <= m**deficit,
                 f"choose bound failed: m={m}, e={deficit}",
             )
-            exponent_cases += 1
+            formal_exponent_cases += 1
+
+            # The stronger budget is retained as an independent diagnostic.
+            require(
+                exponent >= deficit * b_sharp,
+                f"sharper exponent budget failed: m={m}, e={deficit}",
+            )
+            sharper_exponent_cases += 1
 
             # Exact Fraction checks on a representative range.  The preceding
-            # componentwise inequalities prove the same comparison generally;
+            # componentwise inequalities prove the formal comparison generally;
             # these cases guard the implemented formula and integer floors.
             if m <= 120:
                 for d in range(4):
                     for n in (2, 3, 10, 97, 10_000):
                         lhs = local_ratio_with_global_charge(n, m, d, deficit)
-                        rho = Fraction(n * m, 2**b_m)
+                        rho_formal = Fraction(n * m, 2**b_formal)
                         require(
-                            lhs <= rho**deficit,
-                            f"local geometric bound failed: n={n}, m={m}, "
+                            lhs <= rho_formal**deficit,
+                            f"formal local geometric bound failed: n={n}, m={m}, "
                             f"d={d}, e={deficit}",
                         )
                         ratio_cases += 1
 
-    return exponent_cases, ratio_cases
+    return formal_exponent_cases, sharper_exponent_cases, ratio_cases
 
 
 def exact_amgm_checks() -> int:
@@ -127,16 +141,22 @@ def phase_diagnostics() -> list[str]:
     for power in (10, 20, 50, 100, 200):
         n = 10**power
         alpha = int(alpha_zero(n))
-        a = alpha - 2
-        cutoff = a // 2
-        b_star = (3 * a - 10) // 4
-        log2_rho = log2(n) + log2(a) - b_star
+        largest_size = alpha - 2
+        cutoff = largest_size // 2
+
+        # Uniform formal base over endpoint sizes m in [U-3,U].
+        b_formal_star = 2 * (largest_size - 3) // 3
+        log2_rho_formal = log2(n) + log2(largest_size) - b_formal_star
+
+        # Retain the sharper earlier diagnostic for comparison only.
+        b_sharp_star = (3 * largest_size - 10) // 4
+        log2_rho_sharp = log2(n) + log2(largest_size) - b_sharp_star
 
         worst_log_sum = float("-inf")
         worst_type: tuple[int, int] | None = None
         for i in range(4):
             for j in range(4):
-                m = min(a - i, a - j)
+                m = min(largest_size - i, largest_size - j)
                 d = abs(i - j)
                 max_deficit = m - (cutoff + 1)
                 if max_deficit < 1:
@@ -150,35 +170,36 @@ def phase_diagnostics() -> list[str]:
                     worst_log_sum = value
                     worst_type = (i, j)
 
-        # Once rho < 1, the exact geometric majorant is rho/(1-rho).
-        if log2_rho < 0:
-            rho = 2**log2_rho
-            log2_majorant = log2(rho / (1 - rho))
+        if log2_rho_formal < 0:
+            rho_formal = 2**log2_rho_formal
+            log2_formal_majorant = log2(rho_formal / (1 - rho_formal))
             require(
-                worst_log_sum <= log2_majorant + 1e-9,
-                f"phase diagnostic exceeds geometric majorant at 10^{power}",
+                worst_log_sum <= log2_formal_majorant + 1e-9,
+                f"phase diagnostic exceeds formal geometric majorant at 10^{power}",
             )
-            majorant_text = f"log2 geometric majorant={log2_majorant:.6f}"
+            formal_text = f"log2 formal majorant={log2_formal_majorant:.6f}"
         else:
-            majorant_text = "rho >= 1 (pre-asymptotic diagnostic only)"
+            formal_text = "formal rho >= 1 (pre-asymptotic only)"
 
         lines.append(
-            f"  n=10^{power}: a={a}, worst type={worst_type}, "
+            f"  n=10^{power}: U={largest_size}, worst type={worst_type}, "
             f"log2 full-deficit sum={worst_log_sum:.6f}, "
-            f"log2 rho={log2_rho:.6f}, {majorant_text}"
+            f"log2 formal rho={log2_rho_formal:.6f}, {formal_text}, "
+            f"log2 sharper rho={log2_rho_sharp:.6f}"
         )
     return lines
 
 
 def main() -> None:
-    exponent_cases, ratio_cases = exact_high_deficit_checks()
+    formal_cases, sharper_cases, ratio_cases = exact_high_deficit_checks()
     amgm_cases = exact_amgm_checks()
     q_cases = exact_q_absorption_checks()
     diagnostics = phase_diagnostics()
 
     print("ERDOS 625 SECTIONS 8--9 SIMPLIFICATION CHECK: PASS")
-    print(f"  high-deficit exponent cases: {exponent_cases}")
-    print(f"  exact local-ratio cases: {ratio_cases}")
+    print(f"  formal two-thirds exponent cases: {formal_cases}")
+    print(f"  sharper three-quarters diagnostic cases: {sharper_cases}")
+    print(f"  exact formal local-ratio cases: {ratio_cases}")
     print(f"  exact AM-GM cases: {amgm_cases}")
     print(f"  exact q-absorption cases: {q_cases}")
     print("  phase diagnostics:")

From f45482e9d7ed7029bdf825d8a5c05228753eb44e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:52:47 +0300
Subject: [PATCH 26/34] Add the uniform all-high deficit product theorem

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

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
new file mode 100644
index 00000000..3b0ea9a3
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
@@ -0,0 +1,97 @@
+import Erdos625.Section8NearSkeletonExpansion
+import Mathlib.Tactic
+
+/-!
+# Section VIII: uniform product bound for distinguishable high-cell deficits
+
+Once the literal weight of every allowed nonzero deficit is bounded by one
+common quantity `rho`, the optional-deficit expansion is controlled by a single
+finite product.  This module records that generic step independently of the
+endpoint profile and its phase asymptotics.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- A power of an `ENNReal` number at most one is at most the number itself once
+the exponent is positive. -/
+theorem ennreal_pow_le_self_of_le_one
+    (rho : ENNReal) (hrho : rho ≤ 1) (e : Nat) (he : 1 ≤ e) :
+    rho ^ e ≤ rho := by
+  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le he
+  have hk : rho ^ k ≤ 1 := by
+    induction k with
+    | zero => simp
+    | succ k ih =>
+        rw [pow_succ]
+        exact (mul_le_mul' ih hrho).trans_eq (one_mul 1)
+  rw [pow_add, pow_one]
+  exact (mul_le_mul_right hk rho).trans_eq (mul_one rho)
+
+/-- Uniform finite product estimate for optional distinguishable-cell choices.
+Each cell has at most `U` allowed deficits, and every allowed weight is at most
+`rho`. -/
+theorem sum_nearSkeletonChoiceWeight_le_uniform_card_mul
+    {Cell Deficit : Type*}
+    [Fintype Cell] [Fintype Deficit] [DecidableEq Deficit]
+    (allowed : Cell → Finset Deficit)
+    (weight : Cell → Deficit → ENNReal)
+    (U : Nat) (rho : ENNReal)
+    (hcard : ∀ c, (allowed c).card ≤ U)
+    (hweight : ∀ c e, e ∈ allowed c → weight c e ≤ rho) :
+    (∑ choice : NearSkeletonChoice Cell Deficit allowed,
+      nearSkeletonChoiceWeight allowed weight choice) ≤
+        (1 + (U : ENNReal) * rho) ^ Fintype.card Cell := by
+  rw [sum_nearSkeletonChoiceWeight_eq_product]
+  calc
+    (∏ c, (1 + ∑ e ∈ allowed c, weight c e)) ≤
+        ∏ _c : Cell, (1 + (U : ENNReal) * rho) := by
+      apply Finset.prod_le_prod'
+      intro c _
+      apply add_le_add_left
+      calc
+        (∑ e ∈ allowed c, weight c e) ≤
+            ∑ _e ∈ allowed c, rho := by
+          exact Finset.sum_le_sum fun e he => hweight c e he
+        _ = ((allowed c).card : ENNReal) * rho := by
+          simp
+        _ ≤ (U : ENNReal) * rho := by
+          exact mul_le_mul_right (by exact_mod_cast hcard c) rho
+    _ = (1 + (U : ENNReal) * rho) ^ Fintype.card Cell := by
+      simp
+
+/-- If each allowed deficit has a positive natural exponent and its literal
+weight is bounded by `rho^e`, the same uniform product bound follows whenever
+`rho ≤ 1`. -/
+theorem sum_nearSkeletonChoiceWeight_le_uniform_pow
+    {Cell Deficit : Type*}
+    [Fintype Cell] [Fintype Deficit] [DecidableEq Deficit]
+    (allowed : Cell → Finset Deficit)
+    (weight : Cell → Deficit → ENNReal)
+    (exponent : Deficit → Nat)
+    (U : Nat) (rho : ENNReal)
+    (hrho : rho ≤ 1)
+    (hcard : ∀ c, (allowed c).card ≤ U)
+    (hpositive : ∀ c e, e ∈ allowed c → 1 ≤ exponent e)
+    (hweight : ∀ c e, e ∈ allowed c → weight c e ≤ rho ^ exponent e) :
+    (∑ choice : NearSkeletonChoice Cell Deficit allowed,
+      nearSkeletonChoiceWeight allowed weight choice) ≤
+        (1 + (U : ENNReal) * rho) ^ Fintype.card Cell := by
+  apply sum_nearSkeletonChoiceWeight_le_uniform_card_mul
+    allowed weight U rho hcard
+  intro c e he
+  exact (hweight c e he).trans
+    (ennreal_pow_le_self_of_le_one rho hrho (exponent e) (hpositive c e he))
+
+#print axioms ennreal_pow_le_self_of_le_one
+#print axioms sum_nearSkeletonChoiceWeight_le_uniform_card_mul
+#print axioms sum_nearSkeletonChoiceWeight_le_uniform_pow
+
+end
+
+end Erdos625

From 609bfbd6fb365c387cf9b51d2139ad956a2f3628 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:53:09 +0300
Subject: [PATCH 27/34] Extend the Section 8 core to the uniform deficit
 product

---
 625/formalization/Erdos625/Section8SimplificationCore.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section8SimplificationCore.lean b/625/formalization/Erdos625/Section8SimplificationCore.lean
index d620a2ae..9039a3bb 100644
--- a/625/formalization/Erdos625/Section8SimplificationCore.lean
+++ b/625/formalization/Erdos625/Section8SimplificationCore.lean
@@ -1,12 +1,14 @@
 import Erdos625.Section8SquareFreeAMGM
 import Erdos625.Section8AllHighDeficitArithmetic
 import Erdos625.Section8AllHighDeficitCellWeight
+import Erdos625.Section8AllHighDeficitProductBound
 
 /-!
 # Section VIII simplification core
 
 This aggregate module checks the finite bridges used by the shortened Section
 VIII route: square-free AM--GM linearization, one all-high-deficit
-parametrization, its uniform binary exponent budget, and the literal one-cell
-stub-matching weight bound over the full high range.
+parametrization, its uniform binary exponent budget, the literal one-cell
+stub-matching weight bound over the full high range, and the generic product
+bound over distinguishable endpoint cells.
 -/

From 568ec93a65d6c05bf385f0acf88cc3dc98df90c8 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:53:50 +0300
Subject: [PATCH 28/34] Validate the uniform all-high deficit product theorem

---
 .../workflows/erdos625-sections8-9-simplification-check.yml   | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index 0fafa788..0d51cf48 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -10,6 +10,7 @@ on:
       - "625/formalization/Erdos625/Section8SquareFreeAMGM.lean"
       - "625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean"
       - "625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean"
+      - "625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean"
       - "625/formalization/Erdos625/Section8SimplificationCore.lean"
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"
   workflow_dispatch:
@@ -45,6 +46,7 @@ jobs:
             625/formalization/Erdos625/Section8SquareFreeAMGM.lean \
             625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean \
             625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean \
+            625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean \
             625/formalization/Erdos625/Section8SimplificationCore.lean; then
             exit 1
           fi
@@ -64,7 +66,7 @@ jobs:
           lake build Erdos625.Section8SimplificationCore --wfail \
             > /tmp/section8-simplification-lean.log 2>&1
           status=$?
-          tail -n 340 /tmp/section8-simplification-lean.log
+          tail -n 400 /tmp/section8-simplification-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From daa21bbd7991e2a478518a9a536bc35c1fff1c31 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 14:01:11 +0300
Subject: [PATCH 29/34] Repair the uniform all-high deficit product proof

---
 .../Erdos625/Section8AllHighDeficitProductBound.lean  | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
index 3b0ea9a3..80f4764e 100644
--- a/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
+++ b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic
 
 Once the literal weight of every allowed nonzero deficit is bounded by one
 common quantity `rho`, the optional-deficit expansion is controlled by a single
-finite product.  This module records that generic step independently of the
+finite product. This module records that generic step independently of the
 endpoint profile and its phase asymptotics.
 -/
 
@@ -24,12 +24,7 @@ theorem ennreal_pow_le_self_of_le_one
     (rho : ENNReal) (hrho : rho ≤ 1) (e : Nat) (he : 1 ≤ e) :
     rho ^ e ≤ rho := by
   obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le he
-  have hk : rho ^ k ≤ 1 := by
-    induction k with
-    | zero => simp
-    | succ k ih =>
-        rw [pow_succ]
-        exact (mul_le_mul' ih hrho).trans_eq (one_mul 1)
+  have hk : rho ^ k ≤ 1 := pow_le_one₀ bot_le hrho
   rw [pow_add, pow_one]
   exact (mul_le_mul_right hk rho).trans_eq (mul_one rho)
 
@@ -53,7 +48,7 @@ theorem sum_nearSkeletonChoiceWeight_le_uniform_card_mul
         ∏ _c : Cell, (1 + (U : ENNReal) * rho) := by
       apply Finset.prod_le_prod'
       intro c _
-      apply add_le_add_left
+      apply add_le_add_right
       calc
         (∑ e ∈ allowed c, weight c e) ≤
             ∑ _e ∈ allowed c, rho := by

From 7c2fa001a4bd10454b3c1ab8a977976f011128d7 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 14:02:30 +0300
Subject: [PATCH 30/34] Normalize the inverse-power algebra in the all-high
 cell bound

---
 .../Erdos625/Section8AllHighDeficitCellWeight.lean         | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
index d9b673af..b5d93151 100644
--- a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
+++ b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic
 # Section VIII: literal all-high one-cell weight bound
 
 This module connects the all-high deficit parametrization to the repository's
-literal one-cell stub-matching weight `nearCellTerm`.  Despite the historical
+literal one-cell stub-matching weight `nearCellTerm`. Despite the historical
 name, the same exact local weight applies to every endpoint deficit above the
 high-cell cutoff.
 
@@ -101,9 +101,8 @@ theorem nearCellTerm_le_allHighCellBase_pow
       mul_le_mul' hfirst hinv
     _ = allHighCellBase n m ^ e := by
       have heb : e * budget = budget * e := Nat.mul_comm _ _
-      rw [heb]
-      simp [allHighCellBase, budget, div_eq_mul_inv, mul_pow, pow_mul,
-        mul_assoc]
+      rw [heb, pow_mul, inv_pow]
+      simp [allHighCellBase, budget, div_eq_mul_inv, mul_pow, mul_assoc]
 
 /-- Every allowed nonzero all-high deficit satisfies the hypothesis of the
 literal one-cell geometric bound. -/

From 92594d09e6dd22676008260fe19719b4e845e0df Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 14:05:10 +0300
Subject: [PATCH 31/34] Apply the all-high product bound to physical endpoint
 block pairings

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

diff --git a/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
new file mode 100644
index 00000000..2abb3aa9
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
@@ -0,0 +1,163 @@
+import Erdos625.Section8EndpointBlockPairings
+import Erdos625.Section8AllHighDeficitCellWeight
+import Erdos625.Section8AllHighDeficitProductBound
+import Mathlib.Tactic
+
+/-!
+# Section VIII: all-high decorations of one physical endpoint block pairing
+
+For a fixed endpoint block pairing, every selected physical cell may retain its
+full endpoint multiplicity or choose one nonzero deficit still above the global
+high-cell cutoff.  This module expresses that literal family as one
+`NearSkeletonChoice` product and applies the generic uniform product theorem.
+
+The only analytic input retained as a hypothesis is a common upper bound `rho`
+on the one-cell bases.  Its phase asymptotics are deliberately postponed.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Largest of the four endpoint sizes. -/
+def fourEndpointLargestSize (alpha : Nat) (hAlpha : 5 < alpha) : Nat :=
+  fourEndpointOverlapSize alpha hAlpha 0 0
+
+/-- Every endpoint overlap size is at most the largest endpoint size. -/
+theorem fourEndpointOverlapSize_le_largest
+    (alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) :
+    fourEndpointOverlapSize alpha hAlpha i j ≤
+      fourEndpointLargestSize alpha hAlpha := by
+  fin_cases i <;> fin_cases j <;>
+    simp [fourEndpointLargestSize, fourEndpointOverlapSize,
+      fourEndpointSize, fourEndpointCoordinate, fourDeficitCoordinate,
+      fourDeficit] <;> omega
+
+/-- Once `alpha > 8`, all four endpoint sizes lie strictly above half the
+largest endpoint size. -/
+theorem fourEndpointOverlapSize_above_half_largest
+    (alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha)
+    (i j : Fin 4) :
+    fourEndpointLargestSize alpha hAlpha / 2 <
+      fourEndpointOverlapSize alpha hAlpha i j := by
+  fin_cases i <;> fin_cases j <;>
+    simp [fourEndpointLargestSize, fourEndpointOverlapSize,
+      fourEndpointSize, fourEndpointCoordinate, fourDeficitCoordinate,
+      fourDeficit] <;> omega
+
+/-- Global deficit type used for every selected endpoint cell. -/
+abbrev FourEndpointDeficit (alpha : Nat) := Fin (alpha + 1)
+
+/-- Allowed nonzero deficits for one selected physical endpoint cell. -/
+def fourEndpointAllHighAllowed
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (cell : ↥P.1.edges) : Finset (FourEndpointDeficit alpha) :=
+  let i := cell.1.1.1
+  let j := cell.1.2.1
+  let m := fourEndpointOverlapSize alpha hAlpha i j
+  Finset.univ.filter fun deficit =>
+    deficit.1 ∈ Finset.Icc 1
+      (allHighDeficitCut (fourEndpointLargestSize alpha hAlpha) m)
+
+/-- Literal charged local factor attached to one selected endpoint cell and one
+candidate deficit. -/
+def fourEndpointAllHighWeight
+    (n alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (cell : ↥P.1.edges) (deficit : FourEndpointDeficit alpha) : ENNReal :=
+  nearCellTerm n
+    (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1)
+    (Nat.dist cell.1.1.1.val cell.1.2.1.val) deficit.1
+
+/-- Exact optional-deficit expansion over all distinguishable selected cells of
+one physical endpoint block pairing. -/
+theorem sum_fourEndpointAllHighChoiceWeight_eq_product
+    (n alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L) :
+    (∑ choice : NearSkeletonChoice (↥P.1.edges)
+        (FourEndpointDeficit alpha)
+        (fourEndpointAllHighAllowed alpha hAlpha P),
+      nearSkeletonChoiceWeight
+        (fourEndpointAllHighAllowed alpha hAlpha P)
+        (fourEndpointAllHighWeight n alpha hAlpha P) choice) =
+      ∏ cell : ↥P.1.edges,
+        (1 + ∑ deficit ∈ fourEndpointAllHighAllowed alpha hAlpha P cell,
+          fourEndpointAllHighWeight n alpha hAlpha P cell deficit) := by
+  exact sum_nearSkeletonChoiceWeight_eq_product
+    (fourEndpointAllHighAllowed alpha hAlpha P)
+    (fourEndpointAllHighWeight n alpha hAlpha P)
+
+/-- Uniform finite product bound for all literal high deficits decorating one
+endpoint block pairing.  The phase-dependent task is reduced to proving that
+`rho ≤ 1` and that it dominates every local `allHighCellBase`. -/
+theorem sum_fourEndpointAllHighChoiceWeight_le_uniform
+    (n alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (rho : ENNReal) (hrho : rho ≤ 1)
+    (hbase : ∀ cell : ↥P.1.edges,
+      allHighCellBase n
+        (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1) ≤ rho) :
+    (∑ choice : NearSkeletonChoice (↥P.1.edges)
+        (FourEndpointDeficit alpha)
+        (fourEndpointAllHighAllowed alpha hAlpha P),
+      nearSkeletonChoiceWeight
+        (fourEndpointAllHighAllowed alpha hAlpha P)
+        (fourEndpointAllHighWeight n alpha hAlpha P) choice) ≤
+      (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.1.edges.card := by
+  classical
+  apply sum_nearSkeletonChoiceWeight_le_uniform_pow
+    (fourEndpointAllHighAllowed alpha hAlpha P)
+    (fourEndpointAllHighWeight n alpha hAlpha P)
+    (fun deficit => deficit.1) (alpha + 1) rho hrho
+  · intro cell
+    exact Finset.card_le_univ _
+  · intro cell deficit hdeficit
+    have hmem : deficit.1 ∈ Finset.Icc 1
+        (allHighDeficitCut (fourEndpointLargestSize alpha hAlpha)
+          (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1)) := by
+      simpa only [fourEndpointAllHighAllowed, Finset.mem_filter,
+        Finset.mem_univ, true_and] using hdeficit
+    exact (Finset.mem_Icc.mp hmem).1
+  · intro cell deficit hdeficit
+    let i : Fin 4 := cell.1.1.1
+    let j : Fin 4 := cell.1.2.1
+    let m := fourEndpointOverlapSize alpha hAlpha i j
+    have hmem : deficit.1 ∈ Finset.Icc 1
+        (allHighDeficitCut (fourEndpointLargestSize alpha hAlpha) m) := by
+      simpa only [fourEndpointAllHighAllowed, i, j, m,
+        Finset.mem_filter, Finset.mem_univ, true_and] using hdeficit
+    have hcut : deficit.1 ≤
+        allHighDeficitCut (fourEndpointLargestSize alpha hAlpha) m :=
+      (Finset.mem_Icc.mp hmem).2
+    have hm : m ≤ fourEndpointLargestSize alpha hAlpha :=
+      fourEndpointOverlapSize_le_largest alpha hAlpha i j
+    have hmHigh : fourEndpointLargestSize alpha hAlpha / 2 < m :=
+      fourEndpointOverlapSize_above_half_largest alpha hAlpha hHigh i j
+    have hjHigh := allHighDeficit_reconstructs_highMultiplicity
+      (fourEndpointLargestSize alpha hAlpha) m deficit.1 hmHigh hcut
+    have hhalf := highMultiplicity_deficit_twice_lt
+      (fourEndpointLargestSize alpha hAlpha) m (m - deficit.1)
+      hm hjHigh (Nat.sub_le _ _)
+    have hreconstruct : m - (m - deficit.1) = deficit.1 := by omega
+    rw [hreconstruct] at hhalf
+    have hlocal := nearCellTerm_le_allHighCellBase_pow n m
+      (Nat.dist i.val j.val) deficit.1 hhalf
+    exact hlocal.trans (ENNReal.pow_le_pow_left (hbase cell))
+
+#print axioms fourEndpointOverlapSize_le_largest
+#print axioms fourEndpointOverlapSize_above_half_largest
+#print axioms sum_fourEndpointAllHighChoiceWeight_eq_product
+#print axioms sum_fourEndpointAllHighChoiceWeight_le_uniform
+
+end
+
+end Erdos625

From d9762ba0fa15ec719bacf6ef962f4729c550a9e4 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 14:05:55 +0300
Subject: [PATCH 32/34] Extend the Section 8 core to physical endpoint
 decorations

---
 625/formalization/Erdos625/Section8SimplificationCore.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section8SimplificationCore.lean b/625/formalization/Erdos625/Section8SimplificationCore.lean
index 9039a3bb..f12c406f 100644
--- a/625/formalization/Erdos625/Section8SimplificationCore.lean
+++ b/625/formalization/Erdos625/Section8SimplificationCore.lean
@@ -2,6 +2,7 @@ import Erdos625.Section8SquareFreeAMGM
 import Erdos625.Section8AllHighDeficitArithmetic
 import Erdos625.Section8AllHighDeficitCellWeight
 import Erdos625.Section8AllHighDeficitProductBound
+import Erdos625.Section8EndpointAllHighDecoration
 
 /-!
 # Section VIII simplification core
@@ -9,6 +10,6 @@ import Erdos625.Section8AllHighDeficitProductBound
 This aggregate module checks the finite bridges used by the shortened Section
 VIII route: square-free AM--GM linearization, one all-high-deficit
 parametrization, its uniform binary exponent budget, the literal one-cell
-stub-matching weight bound over the full high range, and the generic product
-bound over distinguishable endpoint cells.
+stub-matching weight bound, the generic product bound, and its application to
+all selected physical cells of one endpoint block pairing.
 -/

From 4dc441eed6bcb4ab3a30ddf0780cfca638dc3b94 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 14:06:46 +0300
Subject: [PATCH 33/34] Validate the physical endpoint all-high decoration
 theorem

---
 .../workflows/erdos625-sections8-9-simplification-check.yml   | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/erdos625-sections8-9-simplification-check.yml b/.github/workflows/erdos625-sections8-9-simplification-check.yml
index 0d51cf48..aa3957ee 100644
--- a/.github/workflows/erdos625-sections8-9-simplification-check.yml
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -11,6 +11,7 @@ on:
       - "625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean"
       - "625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean"
       - "625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean"
+      - "625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean"
       - "625/formalization/Erdos625/Section8SimplificationCore.lean"
       - ".github/workflows/erdos625-sections8-9-simplification-check.yml"
   workflow_dispatch:
@@ -47,6 +48,7 @@ jobs:
             625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean \
             625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean \
             625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean \
+            625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean \
             625/formalization/Erdos625/Section8SimplificationCore.lean; then
             exit 1
           fi
@@ -66,7 +68,7 @@ jobs:
           lake build Erdos625.Section8SimplificationCore --wfail \
             > /tmp/section8-simplification-lean.log 2>&1
           status=$?
-          tail -n 400 /tmp/section8-simplification-lean.log
+          tail -n 460 /tmp/section8-simplification-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From a28d43c56897daa44ec2e07acc85855bd58db288 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 14:13:17 +0300
Subject: [PATCH 34/34] Eliminate the pairing-dependent base from all-high
 decorations

---
 .../Section8EndpointAllHighDecoration.lean    | 63 +++++++++++++++++--
 1 file changed, 59 insertions(+), 4 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
index 2abb3aa9..d37067be 100644
--- a/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
+++ b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
@@ -8,11 +8,11 @@ import Mathlib.Tactic
 
 For a fixed endpoint block pairing, every selected physical cell may retain its
 full endpoint multiplicity or choose one nonzero deficit still above the global
-high-cell cutoff.  This module expresses that literal family as one
+high-cell cutoff. This module expresses that literal family as one
 `NearSkeletonChoice` product and applies the generic uniform product theorem.
 
-The only analytic input retained as a hypothesis is a common upper bound `rho`
-on the one-cell bases.  Its phase asymptotics are deliberately postponed.
+The only analytic input retained at the endpoint is the eventual smallness of
+one explicit sum over the sixteen endpoint types.
 -/
 
 namespace Erdos625
@@ -96,7 +96,7 @@ theorem sum_fourEndpointAllHighChoiceWeight_eq_product
     (fourEndpointAllHighWeight n alpha hAlpha P)
 
 /-- Uniform finite product bound for all literal high deficits decorating one
-endpoint block pairing.  The phase-dependent task is reduced to proving that
+endpoint block pairing. The phase-dependent task is reduced to proving that
 `rho ≤ 1` and that it dominates every local `allHighCellBase`. -/
 theorem sum_fourEndpointAllHighChoiceWeight_le_uniform
     (n alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha)
@@ -153,10 +153,65 @@ theorem sum_fourEndpointAllHighChoiceWeight_le_uniform
       (Nat.dist i.val j.val) deficit.1 hhalf
     exact hlocal.trans (ENNReal.pow_le_pow_left (hbase cell))
 
+/-- Explicit common base: the sum of the sixteen endpoint-type bases. -/
+def fourEndpointAllHighRho
+    (n alpha : Nat) (hAlpha : 5 < alpha) : ENNReal :=
+  ∑ i : Fin 4, ∑ j : Fin 4,
+    allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i j)
+
+/-- Every endpoint-type base is bounded by the explicit sixteen-type sum. -/
+theorem allHighCellBase_le_fourEndpointAllHighRho
+    (n alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) :
+    allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i j) ≤
+      fourEndpointAllHighRho n alpha hAlpha := by
+  have hrow :
+      allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i j) ≤
+        ∑ j' : Fin 4,
+          allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i j') :=
+    Finset.single_le_sum
+      (s := Finset.univ)
+      (f := fun j' : Fin 4 =>
+        allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i j'))
+      (fun _ _ => bot_le) (Finset.mem_univ j)
+  have houter :
+      (∑ j' : Fin 4,
+          allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i j')) ≤
+        ∑ i' : Fin 4, ∑ j' : Fin 4,
+          allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i' j') :=
+    Finset.single_le_sum
+      (s := Finset.univ)
+      (f := fun i' : Fin 4 => ∑ j' : Fin 4,
+        allHighCellBase n (fourEndpointOverlapSize alpha hAlpha i' j'))
+      (fun _ _ => bot_le) (Finset.mem_univ i)
+  exact hrow.trans houter
+
+/-- The physical decoration sum is controlled by the explicit sixteen-type
+base; no pairing-dependent analytic hypothesis remains. -/
+theorem sum_fourEndpointAllHighChoiceWeight_le_rho
+    (n alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (hrho : fourEndpointAllHighRho n alpha hAlpha ≤ 1) :
+    (∑ choice : NearSkeletonChoice (↥P.1.edges)
+        (FourEndpointDeficit alpha)
+        (fourEndpointAllHighAllowed alpha hAlpha P),
+      nearSkeletonChoiceWeight
+        (fourEndpointAllHighAllowed alpha hAlpha P)
+        (fourEndpointAllHighWeight n alpha hAlpha P) choice) ≤
+      (1 + ((alpha + 1 : Nat) : ENNReal) *
+        fourEndpointAllHighRho n alpha hAlpha) ^ P.1.edges.card := by
+  apply sum_fourEndpointAllHighChoiceWeight_le_uniform
+    n alpha hAlpha hHigh P (fourEndpointAllHighRho n alpha hAlpha) hrho
+  intro cell
+  exact allHighCellBase_le_fourEndpointAllHighRho
+    n alpha hAlpha cell.1.1.1 cell.1.2.1
+
 #print axioms fourEndpointOverlapSize_le_largest
 #print axioms fourEndpointOverlapSize_above_half_largest
 #print axioms sum_fourEndpointAllHighChoiceWeight_eq_product
 #print axioms sum_fourEndpointAllHighChoiceWeight_le_uniform
+#print axioms allHighCellBase_le_fourEndpointAllHighRho
+#print axioms sum_fourEndpointAllHighChoiceWeight_le_rho
 
 end