From 0b693a9d81ed65d3d8dc51a6ec32112d819103e8 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 08:58:43 +0300
Subject: [PATCH 01/16] Add the sharp cellwise all-deficit product interface

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

diff --git a/625/formalization/Erdos625/Section8SharpDeficitProduct.lean b/625/formalization/Erdos625/Section8SharpDeficitProduct.lean
new file mode 100644
index 00000000..abafd7a1
--- /dev/null
+++ b/625/formalization/Erdos625/Section8SharpDeficitProduct.lean
@@ -0,0 +1,122 @@
+import Erdos625.Section8AllHighDeficitProductBound
+import Mathlib.Tactic
+
+/-!
+# Section VIII: sharp cellwise product interface for all high deficits
+
+The generic all-high product theorem previously replaced every nonzero deficit
+weight by one common bound and then multiplied by the number of admissible
+deficits.  That route is sufficient for the normalized second moment, but it
+introduces an unnecessary factor of the phase size.
+
+This module isolates the sharper interface actually used by the concise
+manuscript proof.  First sum the complete positive-deficit fibre in each
+selected physical cell; then multiply the resulting local partition functions.
+The local bounds may vary from cell to cell.
+
+No geometric-series estimate, phase asymptotic, endpoint transportation bound,
+or identification with attained canonical demands is asserted here.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Exact optional-deficit expansion followed by arbitrary cellwise upper
+bounds on the positive-deficit sums. -/
+theorem sum_nearSkeletonChoiceWeight_le_product_of_local_sums
+    {Cell Deficit : Type*}
+    [Fintype Cell] [Fintype Deficit] [DecidableEq Deficit]
+    (allowed : Cell → Finset Deficit)
+    (weight : Cell → Deficit → ENNReal)
+    (bound : Cell → ENNReal)
+    (hlocal : ∀ c, (∑ e ∈ allowed c, weight c e) ≤ bound c) :
+    (∑ choice : NearSkeletonChoice Cell Deficit allowed,
+      nearSkeletonChoiceWeight allowed weight choice) ≤
+        ∏ c, (1 + bound c) := by
+  rw [sum_nearSkeletonChoiceWeight_eq_product]
+  apply Finset.prod_le_prod'
+  intro c _
+  exact add_le_add_left (hlocal c) 1
+
+/-- Uniform specialization of the cellwise local-sum interface. -/
+theorem sum_nearSkeletonChoiceWeight_le_uniform_local_sum
+    {Cell Deficit : Type*}
+    [Fintype Cell] [Fintype Deficit] [DecidableEq Deficit]
+    (allowed : Cell → Finset Deficit)
+    (weight : Cell → Deficit → ENNReal)
+    (sigma : ENNReal)
+    (hlocal : ∀ c, (∑ e ∈ allowed c, weight c e) ≤ sigma) :
+    (∑ choice : NearSkeletonChoice Cell Deficit allowed,
+      nearSkeletonChoiceWeight allowed weight choice) ≤
+        (1 + sigma) ^ Fintype.card Cell := by
+  calc
+    (∑ choice : NearSkeletonChoice Cell Deficit allowed,
+        nearSkeletonChoiceWeight allowed weight choice) ≤
+        ∏ _c : Cell, (1 + sigma) := by
+      apply sum_nearSkeletonChoiceWeight_le_product_of_local_sums
+        allowed weight (fun _ => sigma)
+      exact hlocal
+    _ = (1 + sigma) ^ Fintype.card Cell := by simp
+
+/-- If the complete positive-deficit fibre in cell `c` is at most `2*rho c`,
+the global optional-deficit partition function retains the cellwise charges. -/
+theorem sum_nearSkeletonChoiceWeight_le_cellwise_two_rho
+    {Cell Deficit : Type*}
+    [Fintype Cell] [Fintype Deficit] [DecidableEq Deficit]
+    (allowed : Cell → Finset Deficit)
+    (weight : Cell → Deficit → ENNReal)
+    (rho : Cell → ENNReal)
+    (hlocal : ∀ c, (∑ e ∈ allowed c, weight c e) ≤ 2 * rho c) :
+    (∑ choice : NearSkeletonChoice Cell Deficit allowed,
+      nearSkeletonChoiceWeight allowed weight choice) ≤
+        ∏ c, (1 + 2 * rho c) := by
+  apply sum_nearSkeletonChoiceWeight_le_product_of_local_sums
+    allowed weight (fun c => 2 * rho c)
+  exact hlocal
+
+/-- Uniform `2*rho` specialization.  This is the formal endpoint needed after
+a finite geometric-series estimate in every selected cell. -/
+theorem sum_nearSkeletonChoiceWeight_le_uniform_two_rho
+    {Cell Deficit : Type*}
+    [Fintype Cell] [Fintype Deficit] [DecidableEq Deficit]
+    (allowed : Cell → Finset Deficit)
+    (weight : Cell → Deficit → ENNReal)
+    (rho : ENNReal)
+    (hlocal : ∀ c, (∑ e ∈ allowed c, weight c e) ≤ 2 * rho) :
+    (∑ choice : NearSkeletonChoice Cell Deficit allowed,
+      nearSkeletonChoiceWeight allowed weight choice) ≤
+        (1 + 2 * rho) ^ Fintype.card Cell := by
+  apply sum_nearSkeletonChoiceWeight_le_uniform_local_sum
+    allowed weight (2 * rho)
+  exact hlocal
+
+/-- The sharp `2*rho` local charge is never worse than the old cardinality
+charge `U*rho` once every cell was allowed at least two candidate deficits. -/
+theorem two_mul_ennreal_le_natCast_mul
+    (U : Nat) (rho : ENNReal) (hU : 2 ≤ U) :
+    2 * rho ≤ (U : ENNReal) * rho := by
+  have hU' : (2 : ENNReal) ≤ (U : ENNReal) := by
+    exact_mod_cast hU
+  exact mul_le_mul_right hU' rho
+
+/-- Additive form of the comparison with the earlier uniform-cardinality
+interface. -/
+theorem one_add_two_mul_ennreal_le_one_add_natCast_mul
+    (U : Nat) (rho : ENNReal) (hU : 2 ≤ U) :
+    1 + 2 * rho ≤ 1 + (U : ENNReal) * rho := by
+  exact add_le_add_left (two_mul_ennreal_le_natCast_mul U rho hU) 1
+
+#print axioms sum_nearSkeletonChoiceWeight_le_product_of_local_sums
+#print axioms sum_nearSkeletonChoiceWeight_le_uniform_local_sum
+#print axioms sum_nearSkeletonChoiceWeight_le_cellwise_two_rho
+#print axioms sum_nearSkeletonChoiceWeight_le_uniform_two_rho
+#print axioms two_mul_ennreal_le_natCast_mul
+
+end
+
+end Erdos625

From 80b9ff4469a62c11699e1fac9a25c4d65dd901c8 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 08:59:59 +0300
Subject: [PATCH 02/16] Add exact checks for the sharp all-deficit partition
 function

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

diff --git a/625/experiments/section8_sharp_deficit_product.py b/625/experiments/section8_sharp_deficit_product.py
new file mode 100644
index 00000000..d7166bf1
--- /dev/null
+++ b/625/experiments/section8_sharp_deficit_product.py
@@ -0,0 +1,226 @@
+#!/usr/bin/env python3
+"""Exact regression checks for the sharp Section VIII deficit product.
+
+The script is standard-library only.  It verifies finite arithmetic and product
+identities used by the concise all-deficit route.  It does not prove the phase
+asymptotics, the attained-demand reindexing, or the random-graph theorem.
+"""
+
+from __future__ import annotations
+
+from decimal import Decimal, getcontext
+from fractions import Fraction
+from itertools import product
+from math import comb, factorial
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise RuntimeError(message)
+
+
+def falling(n: int, k: int) -> int:
+    require(0 <= k <= n, f"invalid falling factorial ({n})_{{{k}}}")
+    value = 1
+    for offset in range(k):
+        value *= n - offset
+    return value
+
+
+def local_ratio(m: int, d: int, h: int) -> Fraction:
+    """The aggregate local ratio R_{m,d}(h)."""
+
+    denominator = 1
+    for t in range(1, h + 1):
+        denominator *= d + t
+    binary_exponent = h * m - h * (h + 1) // 2
+    return Fraction(comb(m, h), denominator * 2**binary_exponent)
+
+
+def check_exact_local_ratio(max_m: int = 100) -> int:
+    checked = 0
+    for m in range(3, max_m + 1):
+        for d in range(4):
+            for h in range((m - 1) // 2 + 1):
+                j = m - h
+                decorated = Fraction(
+                    falling(m, j) * falling(m + d, j), factorial(j)
+                ) * Fraction(2 ** comb(j, 2), 2)
+                full = Fraction(
+                    falling(m, m) * falling(m + d, m), factorial(m)
+                ) * Fraction(2 ** comb(m, 2), 2)
+                require(
+                    decorated / full == local_ratio(m, d, h),
+                    f"local ratio failed at m={m}, d={d}, h={h}",
+                )
+                checked += 1
+    return checked
+
+
+def check_two_thirds_charge(max_m: int = 240) -> int:
+    """Verify n^h R <= (n m / 2^floor(2m/3))^h exactly."""
+
+    checked = 0
+    sample_n = (1, 2, 3, 5, 10, 20, 50, 100)
+    for m in range(3, max_m + 1):
+        for d in range(4):
+            for h in range(1, (m - 1) // 2 + 1):
+                if 2 * h >= m:
+                    continue
+                exponent_budget = h * m - h * (h + 1) // 2
+                require(
+                    h * ((2 * m) // 3) <= exponent_budget,
+                    f"two-thirds exponent budget failed at m={m}, h={h}",
+                )
+                for n in sample_n:
+                    lhs = n**h * local_ratio(m, d, h)
+                    rho = Fraction(n * m, 2 ** ((2 * m) // 3))
+                    require(
+                        lhs <= rho**h,
+                        f"charged local ratio failed at n={n}, m={m}, d={d}, h={h}",
+                    )
+                    checked += 1
+    return checked
+
+
+def check_finite_geometric_bound() -> int:
+    """Check sum_{h=1}^H rho^h <= rho/(1-rho) <= 2 rho."""
+
+    checked = 0
+    for denominator in range(2, 81):
+        for numerator in range(1, denominator // 2 + 1):
+            rho = Fraction(numerator, denominator)
+            require(rho <= Fraction(1, 2), "test construction exceeded one half")
+            for cutoff in range(0, 81):
+                finite_sum = sum(
+                    (rho**h for h in range(1, cutoff + 1)), Fraction(0, 1)
+                )
+                require(
+                    finite_sum <= rho / (1 - rho),
+                    f"geometric majorant failed at rho={rho}, H={cutoff}",
+                )
+                require(
+                    finite_sum <= 2 * rho,
+                    f"two-rho majorant failed at rho={rho}, H={cutoff}",
+                )
+                checked += 1
+    return checked
+
+
+def check_partition_function_factorization() -> int:
+    """Exhaust exact sums over small distinguishable deficit fibres."""
+
+    local_fibres = (
+        (Fraction(1), Fraction(1, 7), Fraction(1, 49)),
+        (Fraction(1), Fraction(2, 9)),
+        (Fraction(1), Fraction(1, 11), Fraction(1, 121), Fraction(1, 1331)),
+        (Fraction(1),),
+    )
+    checked = 0
+    for number_of_cells in range(0, len(local_fibres) + 1):
+        fibres = local_fibres[:number_of_cells]
+        direct = Fraction(0, 1)
+        for choice in product(*fibres):
+            term = Fraction(1, 1)
+            for value in choice:
+                term *= value
+            direct += term
+        factorized = Fraction(1, 1)
+        for fibre in fibres:
+            factorized *= sum(fibre, Fraction(0, 1))
+        require(
+            direct == factorized,
+            f"partition-function factorization failed for {number_of_cells} cells",
+        )
+        checked += 1
+    return checked
+
+
+def check_cellwise_and_uniform_bounds() -> int:
+    """Compare cellwise 2 rho charges with the older U rho interface."""
+
+    checked = 0
+    for U in range(2, 81):
+        for denominator in range(2, 61):
+            for numerator in range(1, denominator // 2 + 1):
+                rho = Fraction(numerator, denominator)
+                require(2 * rho <= U * rho, "sharp charge exceeded old charge")
+                require(1 + 2 * rho <= 1 + U * rho, "additive charge comparison failed")
+                checked += 1
+    return checked
+
+
+def check_endpoint_type_retention() -> int:
+    """Retaining cellwise charges is at least as sharp as replacing them by max rho."""
+
+    checked = 0
+    for alpha in range(12, 61):
+        endpoint_sizes = tuple(alpha - d for d in (2, 3, 4, 5))
+        for n in (1, 2, 5, 10, 20):
+            charges = [
+                Fraction(n * min(s, t), 2 ** ((2 * min(s, t)) // 3))
+                for s in endpoint_sizes
+                for t in endpoint_sizes
+            ]
+            require(
+                sum(charges, Fraction(0, 1)) <= len(charges) * max(charges),
+                "cellwise-to-uniform maximum comparison failed",
+            )
+            checked += 1
+    return checked
+
+
+def asymptotic_diagnostics() -> list[tuple[int, Decimal, Decimal, Decimal]]:
+    """Logarithms of sharp, old, and endpoint-transport scale ratios.
+
+    With N=log n, divide each error scale by n/N^4:
+
+      sharp all-deficit: n^(2/3) N^(4/3) -> exp(-N/3) N^(16/3),
+      old U*rho bound:   n^(2/3) N^(7/3) -> exp(-N/3) N^(19/3),
+      endpoint transport: sqrt(nN)        -> exp(-N/2) N^(9/2).
+    """
+
+    getcontext().prec = 80
+    rows: list[tuple[int, Decimal, Decimal, Decimal]] = []
+    previous: tuple[Decimal, Decimal, Decimal] | None = None
+    for nlog in (120, 240, 480, 960, 1920):
+        N = Decimal(nlog)
+        sharp = -N / 3 + (Decimal(16) / 3) * N.ln()
+        old = -N / 3 + (Decimal(19) / 3) * N.ln()
+        endpoint = -N / 2 + (Decimal(9) / 2) * N.ln()
+        if previous is not None:
+            require(sharp < previous[0], "sharp scale diagnostic is not decreasing")
+            require(old < previous[1], "old scale diagnostic is not decreasing")
+            require(endpoint < previous[2], "endpoint scale diagnostic is not decreasing")
+        previous = (sharp, old, endpoint)
+        rows.append((nlog, sharp, old, endpoint))
+    require(rows[-1][1] < -100, "sharp scale is not strongly subcritical")
+    require(rows[-1][2] < -100, "old scale is not strongly subcritical")
+    require(rows[-1][3] < -100, "endpoint scale is not strongly subcritical")
+    return rows
+
+
+def main() -> None:
+    local_cases = check_exact_local_ratio()
+    charge_cases = check_two_thirds_charge()
+    geometric_cases = check_finite_geometric_bound()
+    factorization_cases = check_partition_function_factorization()
+    comparison_cases = check_cellwise_and_uniform_bounds()
+    endpoint_cases = check_endpoint_type_retention()
+    diagnostics = asymptotic_diagnostics()
+
+    print("ERDOS 625 SHARP DEFICIT PRODUCT: PASS")
+    print(f"  exact aggregate local ratios: {local_cases}")
+    print(f"  exact two-thirds charged ratios: {charge_cases}")
+    print(f"  finite geometric sums: {geometric_cases}")
+    print(f"  exact partition-function factorizations: {factorization_cases}")
+    print(f"  sharp-vs-cardinality comparisons: {comparison_cases}")
+    print(f"  cellwise endpoint-type comparisons: {endpoint_cases}")
+    print("  asymptotic log-ratios (N, sharp, old-cardinality, endpoint):")
+    for row in diagnostics:
+        print("   ", row)
+    print("  scope: exact finite arithmetic and scale diagnostics only")
+
+
+if __name__ == "__main__":
+    main()

From e55b199e3e3f7df766282a217d0f22cb4484ceed Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:01:02 +0300
Subject: [PATCH 03/16] Add the sharp all-deficit lemma and reader-first
 Section 8 proof

---
 ...TION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md | 413 ++++++++++++++++++
 1 file changed, 413 insertions(+)
 create mode 100644 625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md

diff --git a/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md b/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
new file mode 100644
index 00000000..87454d85
--- /dev/null
+++ b/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
@@ -0,0 +1,413 @@
+# Section VIII: sharp all-deficit partition function
+
+## Purpose
+
+This note replaces the last avoidable loss in the concise Section VIII route.
+The earlier generic Lean bound treated every admissible nonzero deficit as if
+it had the same weight `rho` and then paid for the number of possible deficits.
+For a cell of endpoint size of order `log n`, this produces a local factor
+
+\[
+  1+O((\log n)\rho_n).
+\]
+
+The actual deficit weights decrease geometrically. Summing them before taking
+the product gives
+
+\[
+  1+O(\rho_n),
+\]
+
+with no extra phase-size factor. This yields the cleaner exponent
+
+\[
+  O\!\left(n^{2/3}(\log n)^{4/3}\right)
+\]
+
+instead of the still-sufficient but weaker
+
+\[
+  O\!\left(n^{2/3}(\log n)^{7/3}\right).
+\]
+
+The improvement is not a change of probabilistic model. It is the exact order
+in which a finite partition function should be summed:
+
+1. sum all deficits inside each distinguishable selected cell;
+2. multiply the resulting cell partition functions;
+3. only then sum over block supports and endpoint tables.
+
+## 1. Exact finite product lemma
+
+Let `C` be a finite set of distinguishable selected cells. For each cell
+\(c\in C\), let \(A_c\) be its finite set of positive deficits and let
+\(w_c(h)\ge0\) be the corresponding charged local weight. A global optional
+deficit choice either chooses no deficit in a cell, with weight one, or chooses
+one element of \(A_c\). Its weight is the product of the selected local
+weights.
+
+The exact finite identity is
+
+\[
+  \sum_{\text{global choices }\omega}
+    \prod_{c\in C}w_c(\omega_c)
+  =
+  \prod_{c\in C}
+    \left(1+\sum_{h\in A_c}w_c(h)\right).
+  \tag{1.1}
+\]
+
+Here the convention is that the local factor is one when no deficit is chosen.
+This is already kernel-checked as
+
+```text
+sum_nearSkeletonChoiceWeight_eq_product.
+```
+
+The new module
+
+```text
+Erdos625/Section8SharpDeficitProduct.lean
+```
+
+adds the following sharper interface. If
+
+\[
+  \sum_{h\in A_c}w_c(h)\le \sigma_c
+  \qquad(c\in C),
+\]
+
+then
+
+\[
+  \boxed{
+  \sum_{\omega}w(\omega)
+  \le
+  \prod_{c\in C}(1+\sigma_c).}
+  \tag{1.2}
+\]
+
+The theorem retains the cell-dependent values \(\sigma_c\); replacing them by
+one maximum is optional rather than built into the argument.
+
+## 2. Local ratio for one high cell
+
+Fix one selected block pair with endpoint sizes \(m\) and \(m+d\), where
+\(0\le d\le3\). Its full multiplicity is \(m\). If the actual high
+multiplicity is \(j=m-h\), then after summing the literal partial-stub-matching
+fibre, the exact local ratio relative to full containment is
+
+\[
+  R_{m,d}(h)
+  =
+  \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)}
+  2^{-hm+h(h+1)/2}.
+  \tag{2.1}
+\]
+
+For \(h=0\), the empty product is one and \(R_{m,d}(0)=1\).
+
+For a fixed block support \(P\), put
+
+\[
+  J=\sum_{e\in P}(m_e-h_e),
+  \qquad
+  H=\sum_{e\in P}h_e.
+\]
+
+The only nonlocal change is the ambient falling-factorial denominator:
+
+\[
+  \frac{(n)_{J+H}}{(n)_J}
+  =(n-J)_H
+  \le n^H.
+  \tag{2.2}
+\]
+
+Consequently the aggregate charged weight satisfies
+
+\[
+  \frac{w(P,m-h)}{w_{\mathrm{full}}(P)}
+  \le
+  \prod_{e\in P} n^{h_e}R_{m_e,d_e}(h_e).
+  \tag{2.3}
+\]
+
+Equation (2.3) uses one global denominator estimate, not one configuration-model
+normalization per cell.
+
+## 3. Sharp geometric charge
+
+The canonical high condition gives
+
+\[
+  2h<m.
+\]
+
+The exact integer inequality
+
+\[
+  h\left\lfloor\frac{2m}{3}\right\rfloor
+  \le
+  hm-\frac{h(h+1)}2
+  \tag{3.1}
+\]
+
+implies
+
+\[
+  n^hR_{m,d}(h)
+  \le
+  \left(
+    \frac{nm}{2^{\lfloor2m/3\rfloor}}
+  \right)^h.
+  \tag{3.2}
+\]
+
+Define the cell-dependent charge
+
+\[
+  \rho_e
+  :=
+  \frac{n m_e}{2^{\lfloor2m_e/3\rfloor}}.
+  \tag{3.3}
+\]
+
+If \(\rho_e\le1/2\), then the entire positive-deficit fibre in cell \(e\)
+satisfies
+
+\[
+  \sum_{h\ge1}n^hR_{m_e,d_e}(h)
+  \le
+  \sum_{h\ge1}\rho_e^h
+  =
+  \frac{\rho_e}{1-\rho_e}
+  \le2\rho_e.
+  \tag{3.4}
+\]
+
+The finite admissible deficit range is a subset of the infinite series, so no
+factor counting the number of deficits is present.
+
+Applying (1.2) gives the fixed-support estimate
+
+\[
+  \boxed{
+  \sum_{h:\,m-h\text{ high}}w(P,m-h)
+  \le
+  w_{\mathrm{full}}(P)
+  \prod_{e\in P}(1+2\rho_e).}
+  \tag{3.5}
+\]
+
+This cellwise form is slightly sharper than replacing every \(\rho_e\) by
+\(\rho_n=\max_e\rho_e\). The uniform corollary is
+
+\[
+  \sum_h w(P,m-h)
+  \le
+  w_{\mathrm{full}}(P)(1+2\rho_n)^{|P|}.
+  \tag{3.6}
+\]
+
+The previous generic cardinality interface gave
+
+\[
+  (1+U\rho_n)^{|P|},
+\]
+
+where \(U=\Theta(\log n)\). Since \(2\rho_n\le U\rho_n\) for \(U\ge2\),
+(3.6) is never worse and is asymptotically sharper by one factor of \(\log n\)
+in the exponent.
+
+## 4. Phase scale
+
+For the four endpoint sizes, the phase relation gives
+
+\[
+  \rho_n
+  =
+  O\!\left(
+    \frac{(\log n)^{7/3}}{n^{1/3}}
+  \right)
+  =o(1).
+  \tag{4.1}
+\]
+
+The block support is a matching and therefore has at most
+\(k_{\mathrm{co}}=\Theta(n/\log n)\) selected cells. From
+\(\log(1+x)\le x\),
+
+\[
+  (1+2\rho_n)^{k_{\mathrm{co}}}
+  \le
+  \exp\{2k_{\mathrm{co}}\rho_n\}
+  =
+  \exp\!\left\{
+    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+  \right\}.
+  \tag{4.2}
+\]
+
+The endpoint transportation term is
+
+\[
+  \exp\{O(\sqrt{n\log n})\}.
+  \tag{4.3}
+\]
+
+Both exponents are
+
+\[
+  o\!\left(\frac{n}{(\log n)^4}\right).
+\]
+
+Once the attained-demand reindexing and pointwise aggregate weight identity are
+connected to this product, the bare-skeleton estimate becomes
+
+\[
+  \operatorname{BareSkeletonSum}_n
+  \le
+  \exp\!\left\{
+    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+    +O(\sqrt{n\log n})
+  \right\}.
+  \tag{4.4}
+\]
+
+## 5. Reader-first proof of the Section VIII step
+
+The eventual manuscript proof can be reduced to the following sequence.
+
+### Step A: exact reindexing
+
+Every attained canonical high demand determines uniquely:
+
+- a block-level matching support \(P\);
+- one admissible deficit \(h_e\) in each selected cell;
+- the local partial-stub-matching fibre already summed into the aggregate
+  weight.
+
+This is the finite seam targeted by PR #48 and its successors.
+
+### Step B: compare with the full endpoint reference
+
+For fixed \((P,h)\), use (2.1) cell by cell and use (2.2) once globally to
+obtain (2.3).
+
+### Step C: sum all deficits before summing supports
+
+Use (3.4) in each cell and the exact product identity (1.1) to obtain (3.5).
+This is where the new sharp product interface is used.
+
+### Step D: sum full references
+
+Group full block supports by their endpoint table \(L\). The exact decorated
+endpoint normalization gives \(W(L)\), and square-free AM--GM transportation
+gives
+
+\[
+  \sum_LW(L)
+  \le
+  \exp\{O(\sqrt{n\log n})\}\sum_rD(r).
+\]
+
+The partial-diagonal sum is \(1+o(1)\). Combining these statements gives
+(4.4).
+
+This order makes the proof auditable: exact finite identities are completed
+before asymptotic estimates are introduced.
+
+## 6. Worked two-cell example
+
+Let the selected support have two cells with
+
+\[
+  (m_1,d_1,h_1)=(8,1,1),
+  \qquad
+  (m_2,d_2,h_2)=(7,2,2).
+\]
+
+Then
+
+\[
+  (j_1,j_2)=(7,5),
+  \qquad J=12,
+  \qquad H=3.
+\]
+
+The exact aggregate ratio is
+
+\[
+  \frac{(n)_{15}}{(n)_{12}}
+  R_{8,1}(1)R_{7,2}(2)
+  =(n-12)_3R_{8,1}(1)R_{7,2}(2).
+\]
+
+The global denominator is bounded once:
+
+\[
+  (n-12)_3\le n^3=n^{h_1}n^{h_2}.
+\]
+
+Thus
+
+\[
+  \frac{w(P,(7,5))}{w_{\mathrm{full}}(P)}
+  \le
+  \bigl(nR_{8,1}(1)\bigr)
+  \bigl(n^2R_{7,2}(2)\bigr).
+\]
+
+Summing every possible deficit independently in the two cells gives the product
+of their two local partition functions. There is no additional ordering
+factor and no second ambient denominator.
+
+## 7. Formal and computational status
+
+The new Lean module proves only the finite product interfaces:
+
+```text
+sum_nearSkeletonChoiceWeight_le_product_of_local_sums
+sum_nearSkeletonChoiceWeight_le_uniform_local_sum
+sum_nearSkeletonChoiceWeight_le_cellwise_two_rho
+sum_nearSkeletonChoiceWeight_le_uniform_two_rho
+```
+
+It deliberately assumes the local estimates (3.4). The standard-library
+regression script
+
+```text
+625/experiments/section8_sharp_deficit_product.py
+```
+
+checks exactly:
+
+- the formula (2.1);
+- the two-thirds charge (3.2);
+- finite geometric sums and the `2 rho` bound;
+- exact finite product factorization over distinguishable cells;
+- the comparison between the sharp `2 rho` and old `U rho` interfaces;
+- the sharp and old asymptotic error scales.
+
+The script is evidence for arithmetic and bookkeeping. It is not a substitute
+for the remaining Lean reindexing theorem or the phase asymptotics.
+
+## 8. Remaining boundary
+
+This note does not claim that the Erdős 625 proof is closed. The following
+interfaces remain load-bearing:
+
+1. a green attained-demand support/deficit injection on the actual midpoint
+   profile;
+2. the pointwise equality between `profileHighSkeletonWeight` and the aggregate
+   partial-cell weight indexed by that support and deficit vector;
+3. the specialization of the local geometric estimate to the attained
+   endpoint cells;
+4. the final composition with endpoint transportation and the q-only Section
+   IX theorem.
+
+The mathematical improvement here is narrower but exact: once those interfaces
+are connected, the all-deficit cost has the sharp exponent
+\(O(n^{2/3}(\log n)^{4/3})\), and the corresponding manuscript argument can be
+written in four short steps instead of a near/middle case split.

From d1f041ad373682d7eaa2a1a261e82dc9de950937 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:01:40 +0300
Subject: [PATCH 04/16] Add a copy-ready sharp all-deficit Section 8 insert

---
 .../SECTION8_SHARP_DEFICIT_INSERT_V2.tex      | 186 ++++++++++++++++++
 1 file changed, 186 insertions(+)
 create mode 100644 625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex

diff --git a/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex b/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex
new file mode 100644
index 00000000..d2919b28
--- /dev/null
+++ b/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex
@@ -0,0 +1,186 @@
+% Copy-ready Section VIII insert for the post-closure Version 2 manuscript.
+% Do not include this file from main.tex until the attained-demand reindexing
+% and pointwise aggregate weight identity have been checked.
+
+\subsection{The all-deficit partition function}
+\label{subsec:all-deficit-partition-function}
+
+Fix a block-level matching support $P$.  For every selected cell $e\in P$, let
+$s_e,t_e$ be its endpoint block sizes and put
+\[
+  m_e:=\min\{s_e,t_e\},
+  \qquad
+  d_e:=|s_e-t_e|.
+\]
+If the actual high multiplicity is $j_e$, write
+\[
+  j_e=m_e-h_e.
+\]
+The canonical high condition implies $2h_e<m_e$.
+
+After summing the literal partial-stub-matching fibre in every selected cell,
+the aggregate bare weight is
+\begin{equation}
+  w(P,j)
+  =
+  \frac{\displaystyle\prod_{e\in P}
+    (s_e)_{j_e}(t_e)_{j_e}}
+  {\displaystyle (n)_J\prod_{e\in P}j_e!}
+  \prod_{e\in P}g(j_e),
+  \qquad
+  J:=\sum_{e\in P}j_e.
+  \label{eq:aggregate-bare-weight-v2}
+\end{equation}
+No objectwise full completion is selected in
+\eqref{eq:aggregate-bare-weight-v2}; the formula is the sum of the complete
+finite physical fibre.
+
+For endpoint sizes $m,m+d$, define
+\begin{equation}
+  R_{m,d}(h)
+  :=
+  \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)}
+  2^{-hm+h(h+1)/2},
+  \label{eq:local-deficit-ratio-v2}
+\end{equation}
+with $R_{m,d}(0)=1$.
+
+\begin{lemma}[Aggregate deficit comparison]
+\label{lem:aggregate-deficit-comparison-v2}
+For a fixed block support $P$ and an admissible deficit vector
+$h=(h_e)_{e\in P}$,
+\[
+  \frac{w(P,m-h)}{w_{\mathrm{full}}(P)}
+  \le
+  \prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e).
+\]
+\end{lemma}
+
+\begin{proof}
+The ratio of the local factors in one selected cell is exactly
+\eqref{eq:local-deficit-ratio-v2}.  Put
+\[
+  H:=\sum_{e\in P}h_e.
+\]
+The only nonlocal change is the ambient falling-factorial denominator:
+\[
+  \frac{(n)_{J+H}}{(n)_J}
+  =(n-J)_H
+  \le n^H.
+\]
+Distributing $n^H=\prod_e n^{h_e}$ over the selected cells gives the result.
+\end{proof}
+
+\begin{lemma}[Cellwise optional-deficit product]
+\label{lem:cellwise-deficit-product-v2}
+Let $A_e$ be the finite positive-deficit set in cell $e$, and let
+$u_e(h)\ge0$ be its charged local weight.  Then
+\[
+  \sum_{\text{optional deficit choices }\omega}
+    \prod_{e\in P}u_e(\omega_e)
+  =
+  \prod_{e\in P}
+    \left(1+\sum_{h\in A_e}u_e(h)\right),
+\]
+where the local factor is one if no positive deficit is selected.
+Consequently, if
+\[
+  \sum_{h\in A_e}u_e(h)\le \sigma_e
+  \qquad(e\in P),
+\]
+then the total optional-deficit weight is at most
+\[
+  \prod_{e\in P}(1+\sigma_e).
+\]
+\end{lemma}
+
+\begin{proof}
+Expand the finite product.  Each monomial selects either the constant term one
+or exactly one positive-deficit weight in every distinguishable selected cell.
+\end{proof}
+
+For $2h<m$, the integer estimate
+\[
+  h\left\lfloor\frac{2m}{3}\right\rfloor
+  \le
+  hm-\frac{h(h+1)}2
+\]
+and \eqref{eq:local-deficit-ratio-v2} give
+\begin{equation}
+  n^hR_{m,d}(h)
+  \le
+  \left(
+    \frac{nm}{2^{\lfloor2m/3\rfloor}}
+  \right)^h.
+  \label{eq:two-thirds-local-charge-v2}
+\end{equation}
+Define the cell-dependent charge
+\[
+  \rho_e
+  :=
+  \frac{n m_e}{2^{\lfloor2m_e/3\rfloor}}.
+\]
+For all sufficiently large $n$, every endpoint charge is at most $1/2$.
+Therefore
+\[
+  \sum_{h\in A_e}n^hR_{m_e,d_e}(h)
+  \le
+  \sum_{h\ge1}\rho_e^h
+  =
+  \frac{\rho_e}{1-\rho_e}
+  \le2\rho_e.
+\]
+By Lemma~\ref{lem:cellwise-deficit-product-v2},
+\begin{equation}
+  \sum_{h:\,m-h\text{ high}}w(P,m-h)
+  \le
+  w_{\mathrm{full}}(P)
+  \prod_{e\in P}(1+2\rho_e).
+  \label{eq:fixed-support-all-deficit-v2}
+\end{equation}
+
+Let
+\[
+  \rho_n:=\max_e\rho_e.
+\]
+The four-size phase relation gives
+\[
+  \rho_n
+  =
+  O\!\left(
+    \frac{(\log n)^{7/3}}{n^{1/3}}
+  \right)
+  =o(1).
+\]
+Since $|P|\le k_{\mathrm{co}}=\Theta(n/\log n)$,
+\[
+  \prod_{e\in P}(1+2\rho_e)
+  \le
+  (1+2\rho_n)^{k_{\mathrm{co}}}
+  \le
+  \exp\!\left\{
+    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+  \right\}.
+\]
+This estimate has no extra factor of order $\log n$ from counting the
+admissible deficits.
+
+Combining \eqref{eq:fixed-support-all-deficit-v2} with the exact full-endpoint
+normalisation, endpoint transportation, and the partial-diagonal estimate gives
+\begin{equation}
+  \operatorname{BareSkeletonSum}_n
+  \le
+  \exp\!\left\{
+    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+    +O(\sqrt{n\log n})
+  \right\}
+  =
+  \exp\!\left\{
+    o\!\left(\frac{n}{(\log n)^4}\right)
+  \right\}.
+  \label{eq:bare-skeleton-sharp-v2}
+\end{equation}
+
+% Audit boundary: equation \eqref{eq:bare-skeleton-sharp-v2} may be promoted
+% into the canonical manuscript only after the attained-demand reindexing and
+% the pointwise aggregate weight identity are proved on the integrated branch.

From d59126dfffb17e0bb6f9352957236fdc9fa8cb1b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:02:03 +0300
Subject: [PATCH 05/16] Add focused CI for the sharp all-deficit product

---
 .../erdos625-sharp-deficit-product.yml        | 92 +++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100644 .github/workflows/erdos625-sharp-deficit-product.yml

diff --git a/.github/workflows/erdos625-sharp-deficit-product.yml b/.github/workflows/erdos625-sharp-deficit-product.yml
new file mode 100644
index 00000000..5df27a35
--- /dev/null
+++ b/.github/workflows/erdos625-sharp-deficit-product.yml
@@ -0,0 +1,92 @@
+name: Erdős 625 sharp all-deficit product
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section8SharpDeficitProduct.lean"
+      - "625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md"
+      - "625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex"
+      - "625/experiments/section8_sharp_deficit_product.py"
+      - ".github/workflows/erdos625-sharp-deficit-product.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-sharp-deficit-product-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  exact-regression:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Compile exact checker
+        run: python -m py_compile 625/experiments/section8_sharp_deficit_product.py
+      - name: Run exact checker
+        run: python 625/experiments/section8_sharp_deficit_product.py
+      - name: Run exact checker with optimization
+        run: python -O 625/experiments/section8_sharp_deficit_product.py
+      - name: Validate reader-facing TeX fragment
+        run: |
+          python - <<'PY'
+          from pathlib import Path
+
+          path = Path("625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex")
+          text = path.read_text(encoding="utf-8")
+          required = (
+              "Aggregate deficit comparison",
+              "Cellwise optional-deficit product",
+              "eq:aggregate-bare-weight-v2",
+              "eq:fixed-support-all-deficit-v2",
+              "eq:bare-skeleton-sharp-v2",
+              "Audit boundary",
+          )
+          missing = [token for token in required if token not in text]
+          if missing:
+              raise SystemExit(f"missing TeX markers: {missing}")
+          if text.count("{") != text.count("}"):
+              raise SystemExit("unbalanced TeX braces")
+          if "\\tag{" in text:
+              raise SystemExit("manual equation tags are forbidden in the insert")
+          print("TeX marker and brace checks passed")
+          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/Section8SharpDeficitProduct.lean; then
+              exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the sharp all-deficit interface warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section8SharpDeficitProduct --wfail \
+            > /tmp/erdos625-sharp-deficit-product.log 2>&1
+          status=$?
+          tail -n 500 /tmp/erdos625-sharp-deficit-product.log
+          exit $status
+      - name: Upload focused Lean log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-sharp-deficit-product-log
+          path: /tmp/erdos625-sharp-deficit-product.log
+          if-no-files-found: ignore

From 5f62135d3207e35534bca9fffe5a658d0b3d0449 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:06:07 +0300
Subject: [PATCH 06/16] Fix commutative order in the sharp deficit inequalities

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

diff --git a/625/formalization/Erdos625/Section8SharpDeficitProduct.lean b/625/formalization/Erdos625/Section8SharpDeficitProduct.lean
index abafd7a1..869a34c5 100644
--- a/625/formalization/Erdos625/Section8SharpDeficitProduct.lean
+++ b/625/formalization/Erdos625/Section8SharpDeficitProduct.lean
@@ -41,7 +41,7 @@ theorem sum_nearSkeletonChoiceWeight_le_product_of_local_sums
   rw [sum_nearSkeletonChoiceWeight_eq_product]
   apply Finset.prod_le_prod'
   intro c _
-  exact add_le_add_left (hlocal c) 1
+  simpa [add_comm] using add_le_add_left (hlocal c) 1
 
 /-- Uniform specialization of the cellwise local-sum interface. -/
 theorem sum_nearSkeletonChoiceWeight_le_uniform_local_sum
@@ -102,14 +102,15 @@ theorem two_mul_ennreal_le_natCast_mul
     2 * rho ≤ (U : ENNReal) * rho := by
   have hU' : (2 : ENNReal) ≤ (U : ENNReal) := by
     exact_mod_cast hU
-  exact mul_le_mul_right hU' rho
+  simpa [mul_comm] using mul_le_mul_right hU' rho
 
 /-- Additive form of the comparison with the earlier uniform-cardinality
 interface. -/
 theorem one_add_two_mul_ennreal_le_one_add_natCast_mul
     (U : Nat) (rho : ENNReal) (hU : 2 ≤ U) :
     1 + 2 * rho ≤ 1 + (U : ENNReal) * rho := by
-  exact add_le_add_left (two_mul_ennreal_le_natCast_mul U rho hU) 1
+  simpa [add_comm] using
+    add_le_add_left (two_mul_ennreal_le_natCast_mul U rho hU) 1
 
 #print axioms sum_nearSkeletonChoiceWeight_le_product_of_local_sums
 #print axioms sum_nearSkeletonChoiceWeight_le_uniform_local_sum

From 00f5ea6240a59763bb683b6cc3d23900999e5d8d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:09:11 +0300
Subject: [PATCH 07/16] Add the sharper three-quarter deficit exponent budget

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

diff --git a/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
new file mode 100644
index 00000000..7e1840ee
--- /dev/null
+++ b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
@@ -0,0 +1,75 @@
+import Erdos625.Section8AllHighDeficitArithmetic
+import Mathlib.Tactic
+
+/-!
+# Section VIII: the sharp three-quarter exponent budget
+
+For a high multiplicity `j=m-h`, the condition `2h<m` gives a stronger binary
+exponent budget than the earlier two-thirds estimate.  The exact coefficient
+`floor((3m-1)/4)` is the worst-case value at the largest admissible deficit.
+
+This improves the common local charge from
+
+`n*m / 2^floor(2m/3)`
+
+to
+
+`n*m / 2^floor((3m-1)/4)`.
+
+No phase asymptotic or weighted-cell ratio is asserted in this module.
+-/
+
+namespace Erdos625
+
+set_option autoImplicit false
+
+/-- If `2h<m`, then the local binary exponent pays at least
+`h * floor((3m-1)/4)`:
+
+`h * floor((3m-1)/4) <= h*m - h*(h+1)/2`.
+-/
+theorem highDeficit_threeQuarter_exponent_budget
+    (m h : Nat) (hhalf : 2 * h < m) :
+    h * ((3 * m - 1) / 4) ≤ h * m - h * (h + 1) / 2 := by
+  by_cases hh : h = 0
+  · simp [hh]
+  have hhpos : 0 < h := Nat.pos_of_ne_zero hh
+  have hmpos : 0 < m := by omega
+  let penalty := h * (h + 1) / 2
+  have hh_m : h + 1 ≤ m := by omega
+  have hpenalty_le_product : penalty ≤ h * (h + 1) := by
+    dsimp only [penalty]
+    exact Nat.div_le_self _ _
+  have hpenalty_le : penalty ≤ h * m :=
+    hpenalty_le_product.trans (Nat.mul_le_mul_left h hh_m)
+  have hsub : (h * m - penalty) + penalty = h * m :=
+    Nat.sub_add_cancel hpenalty_le
+  have hstep : 2 * (h + 1) ≤ m + 1 := by omega
+  have hstep_mul : 2 * (h * (h + 1)) ≤ h * (m + 1) := by
+    simpa [mul_assoc, mul_comm, mul_left_comm] using
+      Nat.mul_le_mul_left h hstep
+  have hpenalty_div : penalty * 2 ≤ h * (h + 1) := by
+    dsimp only [penalty]
+    exact Nat.div_mul_le_self _ _
+  have hpenalty_four : 4 * penalty ≤ 2 * (h * (h + 1)) := by
+    have hmul := Nat.mul_le_mul_left 2 hpenalty_div
+    simpa [mul_assoc, mul_comm, mul_left_comm] using hmul
+  have hpenalty_bound : 4 * penalty ≤ h * (m + 1) :=
+    hpenalty_four.trans hstep_mul
+  have h3m : 1 ≤ 3 * m := by omega
+  have h3m_sub : (3 * m - 1) + 1 = 3 * m :=
+    Nat.sub_add_cancel h3m
+  have hmain : h * (3 * m - 1) ≤ 4 * (h * m - penalty) := by
+    nlinarith [hsub, hpenalty_bound, h3m_sub]
+  have hquarter := Nat.div_mul_le_self (3 * m - 1) 4
+  have hquarter_mul :
+      4 * (h * ((3 * m - 1) / 4)) ≤ h * (3 * m - 1) := by
+    have hmul := Nat.mul_le_mul_left h hquarter
+    simpa [mul_assoc, mul_comm, mul_left_comm] using hmul
+  have hfour := hquarter_mul.trans hmain
+  dsimp only [penalty] at hfour ⊢
+  omega
+
+#print axioms highDeficit_threeQuarter_exponent_budget
+
+end Erdos625

From 75554aaeb65329a57822c0fefa105ee81a0a1fce Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:09:49 +0300
Subject: [PATCH 08/16] Check the three-quarter exponent budget in focused CI

---
 .../erdos625-sharp-deficit-product.yml        | 28 +++++++++++++------
 1 file changed, 20 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/erdos625-sharp-deficit-product.yml b/.github/workflows/erdos625-sharp-deficit-product.yml
index 5df27a35..d04aead0 100644
--- a/.github/workflows/erdos625-sharp-deficit-product.yml
+++ b/.github/workflows/erdos625-sharp-deficit-product.yml
@@ -4,6 +4,7 @@ on:
   pull_request:
     paths:
       - "625/formalization/Erdos625/Section8SharpDeficitProduct.lean"
+      - "625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean"
       - "625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md"
       - "625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex"
       - "625/experiments/section8_sharp_deficit_product.py"
@@ -62,7 +63,8 @@ jobs:
         run: |
           if grep -nE \
             '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
-            625/formalization/Erdos625/Section8SharpDeficitProduct.lean; then
+            625/formalization/Erdos625/Section8SharpDeficitProduct.lean \
+            625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean; then
               exit 1
           fi
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
@@ -73,16 +75,26 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build the sharp all-deficit interface warning-fatally
+      - name: Build the sharp all-deficit interfaces warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
-          set +e
-          lake build Erdos625.Section8SharpDeficitProduct --wfail \
-            > /tmp/erdos625-sharp-deficit-product.log 2>&1
-          status=$?
-          tail -n 500 /tmp/erdos625-sharp-deficit-product.log
-          exit $status
+          : > /tmp/erdos625-sharp-deficit-product.log
+          for target in \
+            Erdos625.Section8SharpDeficitProduct \
+            Erdos625.Section8ThreeQuarterDeficitArithmetic; do
+              echo "=== $target ===" | tee -a /tmp/erdos625-sharp-deficit-product.log
+              set +e
+              lake build "$target" --wfail \
+                >> /tmp/erdos625-sharp-deficit-product.log 2>&1
+              status=$?
+              set -e
+              if [[ $status -ne 0 ]]; then
+                tail -n 700 /tmp/erdos625-sharp-deficit-product.log
+                exit $status
+              fi
+          done
+          tail -n 700 /tmp/erdos625-sharp-deficit-product.log
       - name: Upload focused Lean log
         if: always()
         uses: actions/upload-artifact@v4

From 2aab9d47ba23665f3cfdcf600f32e8112b6062c3 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:14:18 +0300
Subject: [PATCH 09/16] Repair the constant-factor step in the three-quarter
 budget

---
 .../Erdos625/Section8ThreeQuarterDeficitArithmetic.lean       | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
index 7e1840ee..c108f0db 100644
--- a/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
+++ b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
@@ -33,8 +33,6 @@ theorem highDeficit_threeQuarter_exponent_budget
     h * ((3 * m - 1) / 4) ≤ h * m - h * (h + 1) / 2 := by
   by_cases hh : h = 0
   · simp [hh]
-  have hhpos : 0 < h := Nat.pos_of_ne_zero hh
-  have hmpos : 0 < m := by omega
   let penalty := h * (h + 1) / 2
   have hh_m : h + 1 ≤ m := by omega
   have hpenalty_le_product : penalty ≤ h * (h + 1) := by
@@ -53,7 +51,7 @@ theorem highDeficit_threeQuarter_exponent_budget
     exact Nat.div_mul_le_self _ _
   have hpenalty_four : 4 * penalty ≤ 2 * (h * (h + 1)) := by
     have hmul := Nat.mul_le_mul_left 2 hpenalty_div
-    simpa [mul_assoc, mul_comm, mul_left_comm] using hmul
+    omega
   have hpenalty_bound : 4 * penalty ≤ h * (m + 1) :=
     hpenalty_four.trans hstep_mul
   have h3m : 1 ≤ 3 * m := by omega

From cd9d824c0377469a355ac4d01d8d9fb71fbde0c2 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:18:27 +0300
Subject: [PATCH 10/16] Extend exact checks to the three-quarter deficit budget

---
 .../section8_sharp_deficit_product.py         | 137 ++++++++++++++----
 1 file changed, 111 insertions(+), 26 deletions(-)

diff --git a/625/experiments/section8_sharp_deficit_product.py b/625/experiments/section8_sharp_deficit_product.py
index d7166bf1..f447aec8 100644
--- a/625/experiments/section8_sharp_deficit_product.py
+++ b/625/experiments/section8_sharp_deficit_product.py
@@ -1,8 +1,8 @@
 #!/usr/bin/env python3
 """Exact regression checks for the sharp Section VIII deficit product.
 
-The script is standard-library only.  It verifies finite arithmetic and product
-identities used by the concise all-deficit route.  It does not prove the phase
+The script is standard-library only. It verifies finite arithmetic and product
+identities used by the concise all-deficit route. It does not prove the phase
 asymptotics, the attained-demand reindexing, or the random-graph theorem.
 """
 
@@ -77,7 +77,39 @@ def check_two_thirds_charge(max_m: int = 240) -> int:
                     rho = Fraction(n * m, 2 ** ((2 * m) // 3))
                     require(
                         lhs <= rho**h,
-                        f"charged local ratio failed at n={n}, m={m}, d={d}, h={h}",
+                        f"two-thirds charge failed at n={n}, m={m}, d={d}, h={h}",
+                    )
+                    checked += 1
+    return checked
+
+
+def check_three_quarter_charge(max_m: int = 360) -> int:
+    """Verify the sharper floor((3m-1)/4) charged ratio exactly."""
+
+    checked = 0
+    sample_n = (1, 2, 3, 5, 10, 20, 50, 100)
+    for m in range(3, max_m + 1):
+        two_thirds = (2 * m) // 3
+        three_quarters = (3 * m - 1) // 4
+        require(
+            two_thirds <= three_quarters,
+            f"three-quarter exponent is weaker at m={m}",
+        )
+        for d in range(4):
+            for h in range(1, (m - 1) // 2 + 1):
+                if 2 * h >= m:
+                    continue
+                exponent_budget = h * m - h * (h + 1) // 2
+                require(
+                    h * three_quarters <= exponent_budget,
+                    f"three-quarter exponent budget failed at m={m}, h={h}",
+                )
+                for n in sample_n:
+                    lhs = n**h * local_ratio(m, d, h)
+                    rho = Fraction(n * m, 2**three_quarters)
+                    require(
+                        lhs <= rho**h,
+                        f"three-quarter charge failed at n={n}, m={m}, d={d}, h={h}",
                     )
                     checked += 1
     return checked
@@ -107,6 +139,40 @@ def check_finite_geometric_bound() -> int:
     return checked
 
 
+def check_head_tail_bound(max_m: int = 120) -> int:
+    """Check an optional first-term plus geometric-tail refinement.
+
+    Whenever the three-quarter charge rho is at most one half,
+
+      sum_{h>=1} n^h R(h) <= n R(1) + rho^2/(1-rho).
+
+    This refinement is not needed by the main PR theorem, but records that the
+    first deficit can be separated without changing the exact local ratio.
+    """
+
+    checked = 0
+    for m in range(3, max_m + 1):
+        exponent = (3 * m - 1) // 4
+        for n in range(1, 21):
+            rho = Fraction(n * m, 2**exponent)
+            if rho > Fraction(1, 2):
+                continue
+            for d in range(4):
+                largest = (m - 1) // 2
+                actual = sum(
+                    (n**h * local_ratio(m, d, h) for h in range(1, largest + 1)),
+                    Fraction(0, 1),
+                )
+                first = n * local_ratio(m, d, 1)
+                tail = rho**2 / (1 - rho)
+                require(
+                    actual <= first + tail,
+                    f"head-tail bound failed at n={n}, m={m}, d={d}",
+                )
+                checked += 1
+    return checked
+
+
 def check_partition_function_factorization() -> int:
     """Exhaust exact sums over small distinguishable deficit fibres."""
 
@@ -145,20 +211,26 @@ def check_cellwise_and_uniform_bounds() -> int:
             for numerator in range(1, denominator // 2 + 1):
                 rho = Fraction(numerator, denominator)
                 require(2 * rho <= U * rho, "sharp charge exceeded old charge")
-                require(1 + 2 * rho <= 1 + U * rho, "additive charge comparison failed")
+                require(
+                    1 + 2 * rho <= 1 + U * rho,
+                    "additive charge comparison failed",
+                )
                 checked += 1
     return checked
 
 
 def check_endpoint_type_retention() -> int:
-    """Retaining cellwise charges is at least as sharp as replacing them by max rho."""
+    """Retaining cellwise charges is sharper than replacing them by max rho."""
 
     checked = 0
     for alpha in range(12, 61):
         endpoint_sizes = tuple(alpha - d for d in (2, 3, 4, 5))
         for n in (1, 2, 5, 10, 20):
             charges = [
-                Fraction(n * min(s, t), 2 ** ((2 * min(s, t)) // 3))
+                Fraction(
+                    n * min(s, t),
+                    2 ** ((3 * min(s, t) - 1) // 4),
+                )
                 for s in endpoint_sizes
                 for t in endpoint_sizes
             ]
@@ -170,40 +242,48 @@ def check_endpoint_type_retention() -> int:
     return checked
 
 
-def asymptotic_diagnostics() -> list[tuple[int, Decimal, Decimal, Decimal]]:
-    """Logarithms of sharp, old, and endpoint-transport scale ratios.
+def asymptotic_diagnostics() -> list[
+    tuple[int, Decimal, Decimal, Decimal, Decimal]
+]:
+    """Logarithms of error-scale ratios after division by n/N^4.
 
-    With N=log n, divide each error scale by n/N^4:
+    With N=log n:
 
-      sharp all-deficit: n^(2/3) N^(4/3) -> exp(-N/3) N^(16/3),
-      old U*rho bound:   n^(2/3) N^(7/3) -> exp(-N/3) N^(19/3),
-      endpoint transport: sqrt(nN)        -> exp(-N/2) N^(9/2).
+      three-quarter: sqrt(n) N^(3/2) -> exp(-N/2) N^(11/2),
+      two-thirds:    n^(2/3) N^(4/3) -> exp(-N/3) N^(16/3),
+      old U*rho:     n^(2/3) N^(7/3) -> exp(-N/3) N^(19/3),
+      endpoint:      sqrt(nN)         -> exp(-N/2) N^(9/2).
     """
 
     getcontext().prec = 80
-    rows: list[tuple[int, Decimal, Decimal, Decimal]] = []
-    previous: tuple[Decimal, Decimal, Decimal] | None = None
+    rows: list[tuple[int, Decimal, Decimal, Decimal, Decimal]] = []
+    previous: tuple[Decimal, Decimal, Decimal, Decimal] | None = None
     for nlog in (120, 240, 480, 960, 1920):
         N = Decimal(nlog)
-        sharp = -N / 3 + (Decimal(16) / 3) * N.ln()
+        three_quarter = -N / 2 + (Decimal(11) / 2) * N.ln()
+        two_thirds = -N / 3 + (Decimal(16) / 3) * N.ln()
         old = -N / 3 + (Decimal(19) / 3) * N.ln()
         endpoint = -N / 2 + (Decimal(9) / 2) * N.ln()
+        current = (three_quarter, two_thirds, old, endpoint)
         if previous is not None:
-            require(sharp < previous[0], "sharp scale diagnostic is not decreasing")
-            require(old < previous[1], "old scale diagnostic is not decreasing")
-            require(endpoint < previous[2], "endpoint scale diagnostic is not decreasing")
-        previous = (sharp, old, endpoint)
-        rows.append((nlog, sharp, old, endpoint))
-    require(rows[-1][1] < -100, "sharp scale is not strongly subcritical")
-    require(rows[-1][2] < -100, "old scale is not strongly subcritical")
-    require(rows[-1][3] < -100, "endpoint scale is not strongly subcritical")
+            labels = ("three-quarter", "two-thirds", "old", "endpoint")
+            for label, value, old_value in zip(labels, current, previous):
+                require(value < old_value, f"{label} scale diagnostic is not decreasing")
+        previous = current
+        rows.append((nlog, *current))
+    for index, label in enumerate(
+        ("three-quarter", "two-thirds", "old", "endpoint"), start=1
+    ):
+        require(rows[-1][index] < -100, f"{label} scale is not strongly subcritical")
     return rows
 
 
 def main() -> None:
     local_cases = check_exact_local_ratio()
-    charge_cases = check_two_thirds_charge()
+    two_thirds_cases = check_two_thirds_charge()
+    three_quarter_cases = check_three_quarter_charge()
     geometric_cases = check_finite_geometric_bound()
+    head_tail_cases = check_head_tail_bound()
     factorization_cases = check_partition_function_factorization()
     comparison_cases = check_cellwise_and_uniform_bounds()
     endpoint_cases = check_endpoint_type_retention()
@@ -211,12 +291,17 @@ def main() -> None:
 
     print("ERDOS 625 SHARP DEFICIT PRODUCT: PASS")
     print(f"  exact aggregate local ratios: {local_cases}")
-    print(f"  exact two-thirds charged ratios: {charge_cases}")
+    print(f"  exact two-thirds charged ratios: {two_thirds_cases}")
+    print(f"  exact three-quarter charged ratios: {three_quarter_cases}")
     print(f"  finite geometric sums: {geometric_cases}")
+    print(f"  first-term plus tail checks: {head_tail_cases}")
     print(f"  exact partition-function factorizations: {factorization_cases}")
     print(f"  sharp-vs-cardinality comparisons: {comparison_cases}")
     print(f"  cellwise endpoint-type comparisons: {endpoint_cases}")
-    print("  asymptotic log-ratios (N, sharp, old-cardinality, endpoint):")
+    print(
+        "  asymptotic log-ratios "
+        "(N, three-quarter, two-thirds, old-cardinality, endpoint):"
+    )
     for row in diagnostics:
         print("   ", row)
     print("  scope: exact finite arithmetic and scale diagnostics only")

From 3388d1b246066a5f00e58683495b5bf15258a86d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:21:55 +0300
Subject: [PATCH 11/16] Clarify the near-sharp three-quarter exponent budget

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

diff --git a/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
index c108f0db..dc3842c0 100644
--- a/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
+++ b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
@@ -2,11 +2,13 @@ import Erdos625.Section8AllHighDeficitArithmetic
 import Mathlib.Tactic
 
 /-!
-# Section VIII: the sharp three-quarter exponent budget
+# Section VIII: a three-quarter exponent budget
 
 For a high multiplicity `j=m-h`, the condition `2h<m` gives a stronger binary
-exponent budget than the earlier two-thirds estimate.  The exact coefficient
-`floor((3m-1)/4)` is the worst-case value at the largest admissible deficit.
+exponent budget than the earlier two-thirds estimate.  The coefficient
+`floor((3m-1)/4)` is within one of the optimal integer coefficient
+`floor(3m/4)` and has a short parity-free proof.  The two coefficients have the
+same phase asymptotics.
 
 This improves the common local charge from
 

From 2958f0937fdfb19b8809e9b05183cefb1dca7d8e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:23:37 +0300
Subject: [PATCH 12/16] Upgrade the Section 8 note to the three-quarter charge

---
 ...TION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md | 269 +++++++++++-------
 1 file changed, 170 insertions(+), 99 deletions(-)

diff --git a/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md b/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
index 87454d85..40aa0ab8 100644
--- a/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
+++ b/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
@@ -2,49 +2,76 @@
 
 ## Purpose
 
-This note replaces the last avoidable loss in the concise Section VIII route.
-The earlier generic Lean bound treated every admissible nonzero deficit as if
-it had the same weight `rho` and then paid for the number of possible deficits.
-For a cell of endpoint size of order `log n`, this produces a local factor
+This note makes two independent improvements to the concise Section VIII
+route.
+
+First, the earlier generic Lean bound treated every admissible nonzero deficit
+as if it had the same weight `rho` and then multiplied by the number of
+possible deficits.  For endpoint size of order `log n`, that produces a local
+factor
 
 \[
   1+O((\log n)\rho_n).
 \]
 
-The actual deficit weights decrease geometrically. Summing them before taking
-the product gives
+The actual deficit weights form a geometric sequence.  Summing the complete
+positive-deficit fibre in each distinguishable selected cell before taking the
+product gives
 
 \[
   1+O(\rho_n),
 \]
 
-with no extra phase-size factor. This yields the cleaner exponent
+with no extra phase-size factor.
+
+Second, the high condition `2h<m` gives the near-sharp integer budget
+
+\[
+  h\left\lfloor\frac{3m-1}{4}\right\rfloor
+  \le
+  hm-\frac{h(h+1)}2,
+  \tag{0.1}
+\]
+
+which is stronger than the previously used two-thirds budget.  The coefficient
+in (0.1) differs from the optimal integer coefficient
+\(\lfloor3m/4\rfloor\) by at most one and has the same phase asymptotics.
+
+Together these changes improve the direct all-deficit exponent from
+
+\[
+  O\!\left(n^{2/3}(\log n)^{7/3}\right)
+\]
+
+in the old cardinality interface, first to
 
 \[
   O\!\left(n^{2/3}(\log n)^{4/3}\right)
 \]
 
-instead of the still-sufficient but weaker
+by summing geometrically, and then to
 
 \[
-  O\!\left(n^{2/3}(\log n)^{7/3}\right).
+  O\!\left(\sqrt n(\log n)^{3/2}\right)
 \]
 
-The improvement is not a change of probabilistic model. It is the exact order
-in which a finite partition function should be summed:
+by using (0.1).  Every one of these exponents is sufficient for the normalized
+second moment.  The last is the strongest one-step geometric estimate and is
+the recommended manuscript version.
+
+The proof order is:
 
 1. sum all deficits inside each distinguishable selected cell;
-2. multiply the resulting cell partition functions;
-3. only then sum over block supports and endpoint tables.
+2. multiply the resulting local partition functions;
+3. sum over block supports and endpoint tables only afterward.
 
 ## 1. Exact finite product lemma
 
-Let `C` be a finite set of distinguishable selected cells. For each cell
+Let `C` be a finite set of distinguishable selected cells.  For each
 \(c\in C\), let \(A_c\) be its finite set of positive deficits and let
-\(w_c(h)\ge0\) be the corresponding charged local weight. A global optional
-deficit choice either chooses no deficit in a cell, with weight one, or chooses
-one element of \(A_c\). Its weight is the product of the selected local
-weights.
+\(w_c(h)\ge0\) be the corresponding charged local weight.  A global optional
+deficit choice selects either no deficit in a cell, with weight one, or one
+element of \(A_c\).  Its weight is the product of the selected local weights.
 
 The exact finite identity is
 
@@ -57,7 +84,6 @@ The exact finite identity is
   \tag{1.1}
 \]
 
-Here the convention is that the local factor is one when no deficit is chosen.
 This is already kernel-checked as
 
 ```text
@@ -70,10 +96,10 @@ The new module
 Erdos625/Section8SharpDeficitProduct.lean
 ```
 
-adds the following sharper interface. If
+adds the cellwise inequality: if
 
 \[
-  \sum_{h\in A_c}w_c(h)\le \sigma_c
+  \sum_{h\in A_c}w_c(h)\le\sigma_c
   \qquad(c\in C),
 \]
 
@@ -81,19 +107,28 @@ then
 
 \[
   \boxed{
-  \sum_{\omega}w(\omega)
+  \sum_\omega w(\omega)
   \le
   \prod_{c\in C}(1+\sigma_c).}
   \tag{1.2}
 \]
 
-The theorem retains the cell-dependent values \(\sigma_c\); replacing them by
-one maximum is optional rather than built into the argument.
+The local bounds \(\sigma_c\) may vary with the endpoint type.  Replacing them
+by one maximum is optional, not built into the argument.
+
+The corresponding Lean declarations are
 
-## 2. Local ratio for one high cell
+```text
+sum_nearSkeletonChoiceWeight_le_product_of_local_sums
+sum_nearSkeletonChoiceWeight_le_uniform_local_sum
+sum_nearSkeletonChoiceWeight_le_cellwise_two_rho
+sum_nearSkeletonChoiceWeight_le_uniform_two_rho.
+```
+
+## 2. Aggregate ratio for one high cell
 
-Fix one selected block pair with endpoint sizes \(m\) and \(m+d\), where
-\(0\le d\le3\). Its full multiplicity is \(m\). If the actual high
+Fix a selected block pair with endpoint sizes \(m\) and \(m+d\), where
+\(0\le d\le3\).  Its full multiplicity is \(m\).  If its actual high
 multiplicity is \(j=m-h\), then after summing the literal partial-stub-matching
 fibre, the exact local ratio relative to full containment is
 
@@ -124,44 +159,50 @@ The only nonlocal change is the ambient falling-factorial denominator:
   \tag{2.2}
 \]
 
-Consequently the aggregate charged weight satisfies
+Consequently
 
 \[
+  \boxed{
   \frac{w(P,m-h)}{w_{\mathrm{full}}(P)}
   \le
-  \prod_{e\in P} n^{h_e}R_{m_e,d_e}(h_e).
+  \prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e).}
   \tag{2.3}
 \]
 
-Equation (2.3) uses one global denominator estimate, not one configuration-model
-normalization per cell.
+Equation (2.3) uses one global denominator estimate.  It does not introduce a
+separate configuration-model normalization in every selected cell.
 
-## 3. Sharp geometric charge
+## 3. Three-quarter geometric charge
 
-The canonical high condition gives
+The high condition gives
 
 \[
   2h<m.
 \]
 
-The exact integer inequality
+The kernel-checked theorem
+
+```text
+highDeficit_threeQuarter_exponent_budget
+```
+
+states (0.1).  Combining it with
 
 \[
-  h\left\lfloor\frac{2m}{3}\right\rfloor
-  \le
-  hm-\frac{h(h+1)}2
-  \tag{3.1}
+  \binom mh\le m^h,
+  \qquad
+  (d+1)\cdots(d+h)\ge1,
 \]
 
-implies
+gives
 
 \[
   n^hR_{m,d}(h)
   \le
   \left(
-    \frac{nm}{2^{\lfloor2m/3\rfloor}}
+    \frac{nm}{2^{\lfloor(3m-1)/4\rfloor}}
   \right)^h.
-  \tag{3.2}
+  \tag{3.1}
 \]
 
 Define the cell-dependent charge
@@ -169,11 +210,11 @@ Define the cell-dependent charge
 \[
   \rho_e
   :=
-  \frac{n m_e}{2^{\lfloor2m_e/3\rfloor}}.
-  \tag{3.3}
+  \frac{n m_e}{2^{\lfloor(3m_e-1)/4\rfloor}}.
+  \tag{3.2}
 \]
 
-If \(\rho_e\le1/2\), then the entire positive-deficit fibre in cell \(e\)
+If \(\rho_e\le1/2\), then the complete positive-deficit fibre in cell \(e\)
 satisfies
 
 \[
@@ -183,13 +224,13 @@ satisfies
   =
   \frac{\rho_e}{1-\rho_e}
   \le2\rho_e.
-  \tag{3.4}
+  \tag{3.3}
 \]
 
-The finite admissible deficit range is a subset of the infinite series, so no
-factor counting the number of deficits is present.
+The actual admissible range is finite, so extending it to the infinite series
+only enlarges the sum.  No factor counting the admissible deficits occurs.
 
-Applying (1.2) gives the fixed-support estimate
+Applying (1.2) gives
 
 \[
   \boxed{
@@ -197,45 +238,44 @@ Applying (1.2) gives the fixed-support estimate
   \le
   w_{\mathrm{full}}(P)
   \prod_{e\in P}(1+2\rho_e).}
-  \tag{3.5}
+  \tag{3.4}
 \]
 
-This cellwise form is slightly sharper than replacing every \(\rho_e\) by
-\(\rho_n=\max_e\rho_e\). The uniform corollary is
+Writing \(\rho_n=\max_e\rho_e\), one obtains the uniform corollary
 
 \[
   \sum_h w(P,m-h)
   \le
   w_{\mathrm{full}}(P)(1+2\rho_n)^{|P|}.
-  \tag{3.6}
+  \tag{3.5}
 \]
 
-The previous generic cardinality interface gave
+The previous generic interface gave \((1+U\rho_n)^{|P|}\), where
+\(U=\Theta(\log n)\).  Since \(2\rho_n\le U\rho_n\) for \(U\ge2\), (3.5) is
+never worse and avoids the artificial factor \(U\).
 
-\[
-  (1+U\rho_n)^{|P|},
-\]
+## 4. Phase scale
 
-where \(U=\Theta(\log n)\). Since \(2\rho_n\le U\rho_n\) for \(U\ge2\),
-(3.6) is never worse and is asymptotically sharper by one factor of \(\log n\)
-in the exponent.
+For the four endpoint sizes, the phase relation
 
-## 4. Phase scale
+\[
+  2^{m}=\Theta\!\left(\frac{n^2}{(\log n)^2}\right)
+\]
 
-For the four endpoint sizes, the phase relation gives
+holds uniformly up to constant factors.  Therefore
 
 \[
   \rho_n
   =
   O\!\left(
-    \frac{(\log n)^{7/3}}{n^{1/3}}
+    \frac{(\log n)^{5/2}}{\sqrt n}
   \right)
   =o(1).
   \tag{4.1}
 \]
 
-The block support is a matching and therefore has at most
-\(k_{\mathrm{co}}=\Theta(n/\log n)\) selected cells. From
+The support is a matching, so
+\(|P|\le k_{\mathrm{co}}=\Theta(n/\log n)\).  Using
 \(\log(1+x)\le x\),
 
 \[
@@ -244,12 +284,12 @@ The block support is a matching and therefore has at most
   \exp\{2k_{\mathrm{co}}\rho_n\}
   =
   \exp\!\left\{
-    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+    O\!\left(\sqrt n(\log n)^{3/2}\right)
   \right\}.
   \tag{4.2}
 \]
 
-The endpoint transportation term is
+The endpoint transportation term remains
 
 \[
   \exp\{O(\sqrt{n\log n})\}.
@@ -263,21 +303,50 @@ Both exponents are
 \]
 
 Once the attained-demand reindexing and pointwise aggregate weight identity are
-connected to this product, the bare-skeleton estimate becomes
+connected to this product, the resulting bare-skeleton estimate is
 
 \[
   \operatorname{BareSkeletonSum}_n
   \le
   \exp\!\left\{
-    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+    O\!\left(\sqrt n(\log n)^{3/2}\right)
     +O(\sqrt{n\log n})
   \right\}.
   \tag{4.4}
 \]
 
-## 5. Reader-first proof of the Section VIII step
+### Optional head--tail refinement
+
+The one-step estimate (4.2) is the recommended proof because it is short.  A
+further refinement is available by separating the first deficit:
+
+\[
+  nR_{m,d}(1)
+  =
+  \frac{nm}{d+1}2^{-m+1}
+  =O\!\left(\frac{(\log n)^3}{n}\right).
+  \tag{4.5}
+\]
+
+For the tail \(h\ge2\), (3.1) gives
+
+\[
+  \sum_{h\ge2}n^hR_{m,d}(h)
+  \le
+  \frac{\rho_n^2}{1-\rho_n}
+  =O\!\left(\frac{(\log n)^5}{n}\right).
+  \tag{4.6}
+\]
+
+Thus the local positive-deficit mass is
+\(O((\log n)^5/n)\), and multiplying over at most \(O(n/\log n)\) cells gives
+an all-deficit exponent \(O((\log n)^4)\).  This refinement is exact at the
+finite head--tail level and is checked by the Python regression, but is not
+needed for the main theorem or the Lean product interface.
+
+## 5. Reader-first Section VIII proof
 
-The eventual manuscript proof can be reduced to the following sequence.
+The eventual manuscript proof reduces to four steps.
 
 ### Step A: exact reindexing
 
@@ -295,14 +364,14 @@ This is the finite seam targeted by PR #48 and its successors.
 For fixed \((P,h)\), use (2.1) cell by cell and use (2.2) once globally to
 obtain (2.3).
 
-### Step C: sum all deficits before summing supports
+### Step C: sum deficits before supports
 
-Use (3.4) in each cell and the exact product identity (1.1) to obtain (3.5).
-This is where the new sharp product interface is used.
+Use (3.3) in each selected cell and the exact product identity (1.1) to obtain
+(3.4).  This is the only place the new sharp product interface is needed.
 
-### Step D: sum full references
+### Step D: transport full references
 
-Group full block supports by their endpoint table \(L\). The exact decorated
+Group full block supports by their endpoint table \(L\).  The exact decorated
 endpoint normalization gives \(W(L)\), and square-free AM--GM transportation
 gives
 
@@ -312,15 +381,14 @@ gives
   \exp\{O(\sqrt{n\log n})\}\sum_rD(r).
 \]
 
-The partial-diagonal sum is \(1+o(1)\). Combining these statements gives
-(4.4).
+The partial-diagonal sum is \(1+o(1)\).  Combining the four steps gives (4.4).
 
-This order makes the proof auditable: exact finite identities are completed
-before asymptotic estimates are introduced.
+This order separates exact finite identities from asymptotic estimates and
+removes the old near/middle case split.
 
 ## 6. Worked two-cell example
 
-Let the selected support have two cells with
+Let the selected support contain two cells with
 
 \[
   (m_1,d_1,h_1)=(8,1,1),
@@ -344,13 +412,13 @@ The exact aggregate ratio is
   =(n-12)_3R_{8,1}(1)R_{7,2}(2).
 \]
 
-The global denominator is bounded once:
+The ambient denominator is bounded once:
 
 \[
   (n-12)_3\le n^3=n^{h_1}n^{h_2}.
 \]
 
-Thus
+Hence
 
 \[
   \frac{w(P,(7,5))}{w_{\mathrm{full}}(P)}
@@ -360,22 +428,22 @@ Thus
 \]
 
 Summing every possible deficit independently in the two cells gives the product
-of their two local partition functions. There is no additional ordering
-factor and no second ambient denominator.
+of the two local partition functions.  There is no additional ordering factor
+and no second ambient denominator.
 
 ## 7. Formal and computational status
 
-The new Lean module proves only the finite product interfaces:
+The new Lean modules prove:
 
 ```text
 sum_nearSkeletonChoiceWeight_le_product_of_local_sums
 sum_nearSkeletonChoiceWeight_le_uniform_local_sum
 sum_nearSkeletonChoiceWeight_le_cellwise_two_rho
 sum_nearSkeletonChoiceWeight_le_uniform_two_rho
+highDeficit_threeQuarter_exponent_budget.
 ```
 
-It deliberately assumes the local estimates (3.4). The standard-library
-regression script
+The standard-library regression
 
 ```text
 625/experiments/section8_sharp_deficit_product.py
@@ -383,19 +451,22 @@ regression script
 
 checks exactly:
 
-- the formula (2.1);
-- the two-thirds charge (3.2);
+- the local ratio (2.1);
+- both the two-thirds and three-quarter exponent budgets;
+- the charged local ratio for many finite values;
 - finite geometric sums and the `2 rho` bound;
-- exact finite product factorization over distinguishable cells;
-- the comparison between the sharp `2 rho` and old `U rho` interfaces;
-- the sharp and old asymptotic error scales.
+- the optional first-term plus geometric-tail refinement;
+- exact partition-function factorization over distinguishable cells;
+- the sharp `2 rho` versus old `U rho` comparison;
+- cellwise endpoint-type retention;
+- all relevant error scales compared with \(n/(\log n)^4\).
 
-The script is evidence for arithmetic and bookkeeping. It is not a substitute
-for the remaining Lean reindexing theorem or the phase asymptotics.
+The script verifies arithmetic and bookkeeping.  It is not a substitute for
+the remaining Lean reindexing theorem or the phase asymptotics.
 
 ## 8. Remaining boundary
 
-This note does not claim that the Erdős 625 proof is closed. The following
+This note does not claim that the Erdős 625 proof is closed.  The following
 interfaces remain load-bearing:
 
 1. a green attained-demand support/deficit injection on the actual midpoint
@@ -407,7 +478,7 @@ interfaces remain load-bearing:
 4. the final composition with endpoint transportation and the q-only Section
    IX theorem.
 
-The mathematical improvement here is narrower but exact: once those interfaces
-are connected, the all-deficit cost has the sharp exponent
-\(O(n^{2/3}(\log n)^{4/3})\), and the corresponding manuscript argument can be
-written in four short steps instead of a near/middle case split.
+The mathematical improvement here is exact: once those interfaces are
+connected, the all-deficit contribution admits the short bound
+\(\exp\{O(\sqrt n(\log n)^{3/2})\}\), with an optional head--tail refinement to
+\(\exp\{O((\log n)^4)\}\).

From 835939aec6b2ba3fae128d678944ab31513733ab Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:24:56 +0300
Subject: [PATCH 13/16] Use the three-quarter charge in the Section 8 TeX
 insert

---
 .../SECTION8_SHARP_DEFICIT_INSERT_V2.tex      | 33 ++++++++++++++-----
 1 file changed, 24 insertions(+), 9 deletions(-)

diff --git a/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex b/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex
index d2919b28..d4290bdd 100644
--- a/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex
+++ b/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex
@@ -101,7 +101,7 @@ \subsection{The all-deficit partition function}
 
 For $2h<m$, the integer estimate
 \[
-  h\left\lfloor\frac{2m}{3}\right\rfloor
+  h\left\lfloor\frac{3m-1}{4}\right\rfloor
   \le
   hm-\frac{h(h+1)}2
 \]
@@ -110,15 +110,15 @@ \subsection{The all-deficit partition function}
   n^hR_{m,d}(h)
   \le
   \left(
-    \frac{nm}{2^{\lfloor2m/3\rfloor}}
+    \frac{nm}{2^{\lfloor(3m-1)/4\rfloor}}
   \right)^h.
-  \label{eq:two-thirds-local-charge-v2}
+  \label{eq:three-quarter-local-charge-v2}
 \end{equation}
 Define the cell-dependent charge
 \[
   \rho_e
   :=
-  \frac{n m_e}{2^{\lfloor2m_e/3\rfloor}}.
+  \frac{n m_e}{2^{\lfloor(3m_e-1)/4\rfloor}}.
 \]
 For all sufficiently large $n$, every endpoint charge is at most $1/2$.
 Therefore
@@ -148,7 +148,7 @@ \subsection{The all-deficit partition function}
   \rho_n
   =
   O\!\left(
-    \frac{(\log n)^{7/3}}{n^{1/3}}
+    \frac{(\log n)^{5/2}}{\sqrt n}
   \right)
   =o(1).
 \]
@@ -159,11 +159,11 @@ \subsection{The all-deficit partition function}
   (1+2\rho_n)^{k_{\mathrm{co}}}
   \le
   \exp\!\left\{
-    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+    O\!\left(\sqrt n(\log n)^{3/2}\right)
   \right\}.
 \]
-This estimate has no extra factor of order $\log n$ from counting the
-admissible deficits.
+This estimate has neither the old factor counting admissible deficits nor the
+weaker two-thirds exponent loss.
 
 Combining \eqref{eq:fixed-support-all-deficit-v2} with the exact full-endpoint
 normalisation, endpoint transportation, and the partial-diagonal estimate gives
@@ -171,7 +171,7 @@ \subsection{The all-deficit partition function}
   \operatorname{BareSkeletonSum}_n
   \le
   \exp\!\left\{
-    O\!\left(n^{2/3}(\log n)^{4/3}\right)
+    O\!\left(\sqrt n(\log n)^{3/2}\right)
     +O(\sqrt{n\log n})
   \right\}
   =
@@ -181,6 +181,21 @@ \subsection{The all-deficit partition function}
   \label{eq:bare-skeleton-sharp-v2}
 \end{equation}
 
+\begin{remark}[Optional head--tail refinement]
+The first positive deficit is explicit:
+\[
+  nR_{m,d}(1)
+  =
+  \frac{nm}{d+1}2^{-m+1}
+  =O\!\left(\frac{(\log n)^3}{n}\right).
+\]
+The remaining terms are at most
+$\rho_n^2/(1-\rho_n)=O((\log n)^5/n)$.  Thus one may replace the direct
+all-deficit exponent above by $O((\log n)^4)$.  This refinement is not needed
+for the second moment, so we retain the one-line geometric estimate in the main
+argument.
+\end{remark}
+
 % Audit boundary: equation \eqref{eq:bare-skeleton-sharp-v2} may be promoted
 % into the canonical manuscript only after the attained-demand reindexing and
 % the pointwise aggregate weight identity are proved on the integrated branch.

From 8f3f5028111d6a68f3373344cb0bf3dae77fbafc Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:29:10 +0300
Subject: [PATCH 14/16] Optimize the exact sharp-deficit regression

---
 .../section8_sharp_deficit_product.py         | 66 +++++++++----------
 1 file changed, 30 insertions(+), 36 deletions(-)

diff --git a/625/experiments/section8_sharp_deficit_product.py b/625/experiments/section8_sharp_deficit_product.py
index f447aec8..ce57ae5a 100644
--- a/625/experiments/section8_sharp_deficit_product.py
+++ b/625/experiments/section8_sharp_deficit_product.py
@@ -30,11 +30,9 @@ def falling(n: int, k: int) -> int:
 def local_ratio(m: int, d: int, h: int) -> Fraction:
     """The aggregate local ratio R_{m,d}(h)."""
 
-    denominator = 1
-    for t in range(1, h + 1):
-        denominator *= d + t
+    rising = factorial(d + h) // factorial(d)
     binary_exponent = h * m - h * (h + 1) // 2
-    return Fraction(comb(m, h), denominator * 2**binary_exponent)
+    return Fraction(comb(m, h), rising * 2**binary_exponent)
 
 
 def check_exact_local_ratio(max_m: int = 100) -> int:
@@ -57,24 +55,25 @@ def check_exact_local_ratio(max_m: int = 100) -> int:
     return checked
 
 
-def check_two_thirds_charge(max_m: int = 240) -> int:
+def check_two_thirds_charge(max_m: int = 220) -> int:
     """Verify n^h R <= (n m / 2^floor(2m/3))^h exactly."""
 
     checked = 0
     sample_n = (1, 2, 3, 5, 10, 20, 50, 100)
     for m in range(3, max_m + 1):
+        exponent = (2 * m) // 3
         for d in range(4):
             for h in range(1, (m - 1) // 2 + 1):
-                if 2 * h >= m:
-                    continue
+                require(2 * h < m, "loop admitted a non-high deficit")
                 exponent_budget = h * m - h * (h + 1) // 2
                 require(
-                    h * ((2 * m) // 3) <= exponent_budget,
+                    h * exponent <= exponent_budget,
                     f"two-thirds exponent budget failed at m={m}, h={h}",
                 )
+                ratio = local_ratio(m, d, h)
                 for n in sample_n:
-                    lhs = n**h * local_ratio(m, d, h)
-                    rho = Fraction(n * m, 2 ** ((2 * m) // 3))
+                    lhs = n**h * ratio
+                    rho = Fraction(n * m, 2**exponent)
                     require(
                         lhs <= rho**h,
                         f"two-thirds charge failed at n={n}, m={m}, d={d}, h={h}",
@@ -83,8 +82,8 @@ def check_two_thirds_charge(max_m: int = 240) -> int:
     return checked
 
 
-def check_three_quarter_charge(max_m: int = 360) -> int:
-    """Verify the sharper floor((3m-1)/4) charged ratio exactly."""
+def check_three_quarter_charge(max_m: int = 280) -> int:
+    """Verify the stronger floor((3m-1)/4) charged ratio exactly."""
 
     checked = 0
     sample_n = (1, 2, 3, 5, 10, 20, 50, 100)
@@ -97,15 +96,15 @@ def check_three_quarter_charge(max_m: int = 360) -> int:
         )
         for d in range(4):
             for h in range(1, (m - 1) // 2 + 1):
-                if 2 * h >= m:
-                    continue
+                require(2 * h < m, "loop admitted a non-high deficit")
                 exponent_budget = h * m - h * (h + 1) // 2
                 require(
                     h * three_quarters <= exponent_budget,
                     f"three-quarter exponent budget failed at m={m}, h={h}",
                 )
+                ratio = local_ratio(m, d, h)
                 for n in sample_n:
-                    lhs = n**h * local_ratio(m, d, h)
+                    lhs = n**h * ratio
                     rho = Fraction(n * m, 2**three_quarters)
                     require(
                         lhs <= rho**h,
@@ -123,10 +122,12 @@ def check_finite_geometric_bound() -> int:
         for numerator in range(1, denominator // 2 + 1):
             rho = Fraction(numerator, denominator)
             require(rho <= Fraction(1, 2), "test construction exceeded one half")
+            power = Fraction(1, 1)
+            finite_sum = Fraction(0, 1)
             for cutoff in range(0, 81):
-                finite_sum = sum(
-                    (rho**h for h in range(1, cutoff + 1)), Fraction(0, 1)
-                )
+                if cutoff > 0:
+                    power *= rho
+                    finite_sum += power
                 require(
                     finite_sum <= rho / (1 - rho),
                     f"geometric majorant failed at rho={rho}, H={cutoff}",
@@ -139,31 +140,24 @@ def check_finite_geometric_bound() -> int:
     return checked
 
 
-def check_head_tail_bound(max_m: int = 120) -> int:
-    """Check an optional first-term plus geometric-tail refinement.
-
-    Whenever the three-quarter charge rho is at most one half,
-
-      sum_{h>=1} n^h R(h) <= n R(1) + rho^2/(1-rho).
-
-    This refinement is not needed by the main PR theorem, but records that the
-    first deficit can be separated without changing the exact local ratio.
-    """
+def check_head_tail_bound(max_m: int = 100) -> int:
+    """Check the optional first-term plus geometric-tail refinement."""
 
     checked = 0
     for m in range(3, max_m + 1):
         exponent = (3 * m - 1) // 4
-        for n in range(1, 21):
-            rho = Fraction(n * m, 2**exponent)
-            if rho > Fraction(1, 2):
-                continue
-            for d in range(4):
-                largest = (m - 1) // 2
+        largest = (m - 1) // 2
+        for d in range(4):
+            ratios = tuple(local_ratio(m, d, h) for h in range(largest + 1))
+            for n in range(1, 21):
+                rho = Fraction(n * m, 2**exponent)
+                if rho > Fraction(1, 2):
+                    continue
                 actual = sum(
-                    (n**h * local_ratio(m, d, h) for h in range(1, largest + 1)),
+                    (n**h * ratios[h] for h in range(1, largest + 1)),
                     Fraction(0, 1),
                 )
-                first = n * local_ratio(m, d, 1)
+                first = n * ratios[1]
                 tail = rho**2 / (1 - rho)
                 require(
                     actual <= first + tail,

From 6e6436bf5bf9c5fd5dc8d3f81a785f345d3657cf Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 10:21:12 +0300
Subject: [PATCH 15/16] TEMP

---
 625/experiments/extract_line_by_line_audit_map.py | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 625/experiments/extract_line_by_line_audit_map.py

diff --git a/625/experiments/extract_line_by_line_audit_map.py b/625/experiments/extract_line_by_line_audit_map.py
new file mode 100644
index 00000000..c1b0730e
--- /dev/null
+++ b/625/experiments/extract_line_by_line_audit_map.py
@@ -0,0 +1 @@
+x
\ No newline at end of file

From ea04ab9bc61b8104d325486759cca31d32829244 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 10:22:03 +0300
Subject: [PATCH 16/16] Remove accidental audit-map placeholder

---
 625/experiments/extract_line_by_line_audit_map.py | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 625/experiments/extract_line_by_line_audit_map.py

diff --git a/625/experiments/extract_line_by_line_audit_map.py b/625/experiments/extract_line_by_line_audit_map.py
deleted file mode 100644
index c1b0730e..00000000
--- a/625/experiments/extract_line_by_line_audit_map.py
+++ /dev/null
@@ -1 +0,0 @@
-x
\ No newline at end of file