diff --git a/.github/workflows/erdos625-sharp-deficit-product.yml b/.github/workflows/erdos625-sharp-deficit-product.yml
new file mode 100644
index 00000000..d04aead0
--- /dev/null
+++ b/.github/workflows/erdos625-sharp-deficit-product.yml
@@ -0,0 +1,104 @@
+name: Erdős 625 sharp all-deficit product
+
+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"
+      - ".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 \
+            625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.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 interfaces warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          : > /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
+        with:
+          name: erdos625-sharp-deficit-product-log
+          path: /tmp/erdos625-sharp-deficit-product.log
+          if-no-files-found: ignore
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..d4290bdd
--- /dev/null
+++ b/625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex
@@ -0,0 +1,201 @@
+% 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{3m-1}{4}\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^{\lfloor(3m-1)/4\rfloor}}
+  \right)^h.
+  \label{eq:three-quarter-local-charge-v2}
+\end{equation}
+Define the cell-dependent charge
+\[
+  \rho_e
+  :=
+  \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
+\[
+  \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)^{5/2}}{\sqrt n}
+  \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(\sqrt n(\log n)^{3/2}\right)
+  \right\}.
+\]
+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
+\begin{equation}
+  \operatorname{BareSkeletonSum}_n
+  \le
+  \exp\!\left\{
+    O\!\left(\sqrt n(\log n)^{3/2}\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}
+
+\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.
diff --git a/625/experiments/section8_sharp_deficit_product.py b/625/experiments/section8_sharp_deficit_product.py
new file mode 100644
index 00000000..ce57ae5a
--- /dev/null
+++ b/625/experiments/section8_sharp_deficit_product.py
@@ -0,0 +1,305 @@
+#!/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)."""
+
+    rising = factorial(d + h) // factorial(d)
+    binary_exponent = h * m - h * (h + 1) // 2
+    return Fraction(comb(m, h), rising * 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 = 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):
+                require(2 * h < m, "loop admitted a non-high deficit")
+                exponent_budget = h * m - h * (h + 1) // 2
+                require(
+                    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 * 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}",
+                    )
+                    checked += 1
+    return checked
+
+
+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)
+    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):
+                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 * ratio
+                    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
+
+
+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")
+            power = Fraction(1, 1)
+            finite_sum = Fraction(0, 1)
+            for cutoff in range(0, 81):
+                if cutoff > 0:
+                    power *= rho
+                    finite_sum += power
+                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_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
+        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 * ratios[h] for h in range(1, largest + 1)),
+                    Fraction(0, 1),
+                )
+                first = n * ratios[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."""
+
+    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 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 ** ((3 * min(s, t) - 1) // 4),
+                )
+                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, Decimal]
+]:
+    """Logarithms of error-scale ratios after division by n/N^4.
+
+    With N=log n:
+
+      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, Decimal]] = []
+    previous: tuple[Decimal, Decimal, Decimal, Decimal] | None = None
+    for nlog in (120, 240, 480, 960, 1920):
+        N = Decimal(nlog)
+        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:
+            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()
+    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()
+    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: {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, three-quarter, two-thirds, old-cardinality, endpoint):"
+    )
+    for row in diagnostics:
+        print("   ", row)
+    print("  scope: exact finite arithmetic and scale diagnostics only")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/625/formalization/Erdos625/Section8SharpDeficitProduct.lean b/625/formalization/Erdos625/Section8SharpDeficitProduct.lean
new file mode 100644
index 00000000..869a34c5
--- /dev/null
+++ b/625/formalization/Erdos625/Section8SharpDeficitProduct.lean
@@ -0,0 +1,123 @@
+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 _
+  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
+    {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
+  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
+  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
+#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
diff --git a/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
new file mode 100644
index 00000000..dc3842c0
--- /dev/null
+++ b/625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
@@ -0,0 +1,75 @@
+import Erdos625.Section8AllHighDeficitArithmetic
+import Mathlib.Tactic
+
+/-!
+# 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 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
+
+`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]
+  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
+    omega
+  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
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..40aa0ab8
--- /dev/null
+++ b/625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
@@ -0,0 +1,484 @@
+# Section VIII: sharp all-deficit partition function
+
+## Purpose
+
+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 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.
+
+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)
+\]
+
+by summing geometrically, and then to
+
+\[
+  O\!\left(\sqrt n(\log n)^{3/2}\right)
+\]
+
+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 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
+\(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 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
+
+\[
+  \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}
+\]
+
+This is already kernel-checked as
+
+```text
+sum_nearSkeletonChoiceWeight_eq_product.
+```
+
+The new module
+
+```text
+Erdos625/Section8SharpDeficitProduct.lean
+```
+
+adds the cellwise inequality: 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 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
+
+```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 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
+
+\[
+  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
+
+\[
+  \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).}
+  \tag{2.3}
+\]
+
+Equation (2.3) uses one global denominator estimate.  It does not introduce a
+separate configuration-model normalization in every selected cell.
+
+## 3. Three-quarter geometric charge
+
+The high condition gives
+
+\[
+  2h<m.
+\]
+
+The kernel-checked theorem
+
+```text
+highDeficit_threeQuarter_exponent_budget
+```
+
+states (0.1).  Combining it with
+
+\[
+  \binom mh\le m^h,
+  \qquad
+  (d+1)\cdots(d+h)\ge1,
+\]
+
+gives
+
+\[
+  n^hR_{m,d}(h)
+  \le
+  \left(
+    \frac{nm}{2^{\lfloor(3m-1)/4\rfloor}}
+  \right)^h.
+  \tag{3.1}
+\]
+
+Define the cell-dependent charge
+
+\[
+  \rho_e
+  :=
+  \frac{n m_e}{2^{\lfloor(3m_e-1)/4\rfloor}}.
+  \tag{3.2}
+\]
+
+If \(\rho_e\le1/2\), then the complete 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.3}
+\]
+
+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
+
+\[
+  \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.4}
+\]
+
+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.5}
+\]
+
+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\).
+
+## 4. Phase scale
+
+For the four endpoint sizes, the phase relation
+
+\[
+  2^{m}=\Theta\!\left(\frac{n^2}{(\log n)^2}\right)
+\]
+
+holds uniformly up to constant factors.  Therefore
+
+\[
+  \rho_n
+  =
+  O\!\left(
+    \frac{(\log n)^{5/2}}{\sqrt n}
+  \right)
+  =o(1).
+  \tag{4.1}
+\]
+
+The support is a matching, so
+\(|P|\le k_{\mathrm{co}}=\Theta(n/\log n)\).  Using
+\(\log(1+x)\le x\),
+
+\[
+  (1+2\rho_n)^{k_{\mathrm{co}}}
+  \le
+  \exp\{2k_{\mathrm{co}}\rho_n\}
+  =
+  \exp\!\left\{
+    O\!\left(\sqrt n(\log n)^{3/2}\right)
+  \right\}.
+  \tag{4.2}
+\]
+
+The endpoint transportation term remains
+
+\[
+  \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 resulting bare-skeleton estimate is
+
+\[
+  \operatorname{BareSkeletonSum}_n
+  \le
+  \exp\!\left\{
+    O\!\left(\sqrt n(\log n)^{3/2}\right)
+    +O(\sqrt{n\log n})
+  \right\}.
+  \tag{4.4}
+\]
+
+### 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 reduces to four steps.
+
+### 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 deficits before supports
+
+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: transport 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 the four steps gives (4.4).
+
+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 contain 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 ambient denominator is bounded once:
+
+\[
+  (n-12)_3\le n^3=n^{h_1}n^{h_2}.
+\]
+
+Hence
+
+\[
+  \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 the two local partition functions.  There is no additional ordering factor
+and no second ambient denominator.
+
+## 7. Formal and computational status
+
+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.
+```
+
+The standard-library regression
+
+```text
+625/experiments/section8_sharp_deficit_product.py
+```
+
+checks exactly:
+
+- 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;
+- 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 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
+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 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)\}\).