Sharpen and simplify the Section 8 all-deficit partition function

.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

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.