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..aa3957ee
--- /dev/null
+++ b/.github/workflows/erdos625-sections8-9-simplification-check.yml
@@ -0,0 +1,79 @@
+name: Erdős 625 Sections 8--9 simplification check
+
+on:
+  pull_request:
+    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/Section8SquareFreeAMGM.lean"
+      - "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:
+
+concurrency:
+  group: erdos625-sections8-9-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+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
+
+  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/Section8SquareFreeAMGM.lean \
+            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
+      - 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 Section 8 simplification core warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section8SimplificationCore --wfail \
+            > /tmp/section8-simplification-lean.log 2>&1
+          status=$?
+          tail -n 460 /tmp/section8-simplification-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section8-simplification-lean-log
+          path: /tmp/section8-simplification-lean.log
+          if-no-files-found: ignore
diff --git a/625/experiments/sections8_9_simplification_check.py b/625/experiments/sections8_9_simplification_check.py
new file mode 100644
index 00000000..269d389c
--- /dev/null
+++ b/625/experiments/sections8_9_simplification_check.py
@@ -0,0 +1,211 @@
+#!/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.
+
+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, 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, int]:
+    """Check the formal two-thirds domination and the optional sharper budget."""
+
+    formal_exponent_cases = 0
+    sharper_exponent_cases = 0
+    ratio_cases = 0
+
+    for m in range(2, 601):
+        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_formal,
+                f"formal exponent budget failed: m={m}, e={deficit}",
+            )
+            require(
+                comb(m, deficit) <= m**deficit,
+                f"choose bound failed: m={m}, e={deficit}",
+            )
+            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 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_formal = Fraction(n * m, 2**b_formal)
+                        require(
+                            lhs <= rho_formal**deficit,
+                            f"formal local geometric bound failed: n={n}, m={m}, "
+                            f"d={d}, e={deficit}",
+                        )
+                        ratio_cases += 1
+
+    return formal_exponent_cases, sharper_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))
+        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(largest_size - i, largest_size - 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)
+
+        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_formal_majorant + 1e-9,
+                f"phase diagnostic exceeds formal geometric majorant at 10^{power}",
+            )
+            formal_text = f"log2 formal majorant={log2_formal_majorant:.6f}"
+        else:
+            formal_text = "formal rho >= 1 (pre-asymptotic only)"
+
+        lines.append(
+            f"  n=10^{power}: U={largest_size}, worst type={worst_type}, "
+            f"log2 full-deficit sum={worst_log_sum:.6f}, "
+            f"log2 formal rho={log2_rho_formal:.6f}, {formal_text}, "
+            f"log2 sharper rho={log2_rho_sharp:.6f}"
+        )
+    return lines
+
+
+def main() -> None:
+    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"  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:")
+    for line in diagnostics:
+        print(line)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean b/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
new file mode 100644
index 00000000..42f1fb81
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AllHighDeficitArithmetic.lean
@@ -0,0 +1,115 @@
+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.
+
+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
+
+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
+
+/-- 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
diff --git a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
new file mode 100644
index 00000000..b5d93151
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
@@ -0,0 +1,132 @@
+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 : Nat)
+  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
+    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
+    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_right 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
+      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, 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. -/
+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 hmem : e.1 ∈ Finset.Icc 1 (allHighDeficitCut a m) := by
+    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 _ _)
+  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
diff --git a/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
new file mode 100644
index 00000000..80f4764e
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
@@ -0,0 +1,92 @@
+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 := pow_le_one₀ bot_le hrho
+  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_right
+      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
diff --git a/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
new file mode 100644
index 00000000..d37067be
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
@@ -0,0 +1,218 @@
+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 at the endpoint is the eventual smallness of
+one explicit sum over the sixteen endpoint types.
+-/
+
+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))
+
+/-- 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
+
+end Erdos625
diff --git a/625/formalization/Erdos625/Section8SimplificationCore.lean b/625/formalization/Erdos625/Section8SimplificationCore.lean
new file mode 100644
index 00000000..f12c406f
--- /dev/null
+++ b/625/formalization/Erdos625/Section8SimplificationCore.lean
@@ -0,0 +1,15 @@
+import Erdos625.Section8SquareFreeAMGM
+import Erdos625.Section8AllHighDeficitArithmetic
+import Erdos625.Section8AllHighDeficitCellWeight
+import Erdos625.Section8AllHighDeficitProductBound
+import Erdos625.Section8EndpointAllHighDecoration
+
+/-!
+# 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, the literal one-cell
+stub-matching weight bound, the generic product bound, and its application to
+all selected physical cells of one endpoint block pairing.
+-/
diff --git a/625/formalization/Erdos625/Section8SquareFreeAMGM.lean b/625/formalization/Erdos625/Section8SquareFreeAMGM.lean
new file mode 100644
index 00000000..83c2b6eb
--- /dev/null
+++ b/625/formalization/Erdos625/Section8SquareFreeAMGM.lean
@@ -0,0 +1,42 @@
+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 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)
+    (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
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.
diff --git a/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
new file mode 100644
index 00000000..c1d93aba
--- /dev/null
+++ b/625/proofs/SECTIONS8_9_CONCISE_REPLACEMENT.md
@@ -0,0 +1,427 @@
+# 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 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 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,
+$$
+
+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
+
+$$
+\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
+$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 without a global Cauchy step
+
+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},
+$$
+
+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\}$,
+
+$$
+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$ 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
+
+$$
+\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
+
+$$
+\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
+
+$$
+\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.
+
+### 8.2 One decorated-cell expansion for all high multiplicities
+
+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$, we have
+
+$$
+2h<m.
+\tag{8.8}
+$$
+
+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}
+$$
+
+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
+
+$$
+A_{m,d}(h)
+\le
+\left(\frac{nm}{2^{\lfloor2m/3\rfloor}}\right)^h.
+\tag{8.11}
+$$
+
+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
+
+$$
+\rho_n
+=O\!\left(\frac{N^{7/3}}{n^{1/3}}\right)
+=o(1).
+\tag{8.12}
+$$
+
+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}}$ 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
+
+$$
+\mathcal A(\mathcal M,j)
+=
+\mathbb E_{\mathrm{res}}\!\left[
+\prod_{a,b} g(r'_{ab})
+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{\mathrm 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 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
+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_{(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,
+
+$$
+\sum_{a,b}\theta_{ab}^2
+=
+\frac{\mathrm e^2}{m_0^2}
+\left(\sum_ad_a^2\right)
+\left(\sum_b(d'_b)^2\right)
+\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.
+
+### 9.2 Complementary small-power regime
+
+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
+$\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$.
+
+### 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
+
+$$
+\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.
+
+## Formalization map and remaining boundary
+
+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;
+- 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. transport (8.4) through the exact physical/type-table quotient and sum it
+   by the one-sided multinomial expansions;
+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.
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).