diff --git a/.github/workflows/erdos625-self-contained-manuscript.yml b/.github/workflows/erdos625-self-contained-manuscript.yml
new file mode 100644
index 0000000..4d50797
--- /dev/null
+++ b/.github/workflows/erdos625-self-contained-manuscript.yml
@@ -0,0 +1,128 @@
+name: Erdős 625 self-contained manuscript
+
+on:
+  pull_request:
+    paths:
+      - "625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex"
+      - "625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex"
+      - "625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex"
+      - "625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex"
+      - "625/arxiv/SECTION8_SELF_CONTAINED_V3.tex"
+      - "625/arxiv/SECTION9_SELF_CONTAINED_V3.tex"
+      - "625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex"
+      - "625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex"
+      - "625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex"
+      - "625/arxiv/main.tex"
+      - "625/arxiv/references.bib"
+      - "625/scripts/build_self_contained_ams_v3.py"
+      - "625/experiments/check_self_contained_manuscript_v3.py"
+      - "625/audits/SELF_CONTAINED_BULLETPROOF_MANUSCRIPT_PASS_2026-08-04.md"
+      - ".github/workflows/erdos625-self-contained-manuscript.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-self-contained-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  structural-checks:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Compile manuscript tools
+        run: |
+          python -m py_compile 625/scripts/build_self_contained_ams_v3.py
+          python -m py_compile 625/experiments/check_self_contained_manuscript_v3.py
+      - name: Run fail-closed manuscript checker
+        run: python 625/experiments/check_self_contained_manuscript_v3.py
+      - name: Replay checker with optimized Python
+        run: python -O 625/experiments/check_self_contained_manuscript_v3.py
+      - name: Upload generated TeX body
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-self-contained-generated-body
+          path: 625/arxiv/AMS_SELF_CONTAINED_BODY_V3.generated.tex
+          if-no-files-found: error
+
+  build-complete-pdf:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Install TeX and PDF inspection dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends \
+            latexmk texlive-latex-extra texlive-bibtex-extra \
+            texlive-fonts-recommended texlive-fonts-extra \
+            texlive-plain-generic poppler-utils
+      - name: Generate the complete manuscript body
+        run: python 625/scripts/build_self_contained_ams_v3.py
+      - name: Build the complete AMS manuscript
+        working-directory: 625/arxiv
+        run: |
+          latexmk -pdf -interaction=nonstopmode -halt-on-error \
+            AMS_SELF_CONTAINED_DRAFT_V3.tex
+      - name: Reject unresolved references and citations
+        working-directory: 625/arxiv
+        shell: bash
+        run: |
+          if grep -E \
+              "LaTeX Warning: (Reference|Citation).*undefined|There were undefined references|There were undefined citations" \
+              AMS_SELF_CONTAINED_DRAFT_V3.log; then
+            exit 1
+          fi
+      - name: Reject material overfull boxes
+        working-directory: 625/arxiv
+        shell: bash
+        run: |
+          python - <<'PY'
+          import re
+          from pathlib import Path
+          log = Path("AMS_SELF_CONTAINED_DRAFT_V3.log").read_text(errors="replace")
+          widths = [float(x) for x in re.findall(r"Overfull \\hbox \(([0-9.]+)pt too wide\)", log)]
+          bad = [x for x in widths if x > 5.0]
+          if bad:
+              raise SystemExit(f"material overfull boxes: {bad}")
+          print(f"overfull boxes above 5pt: {len(bad)}")
+          PY
+      - name: Verify full-paper size and extractability
+        working-directory: 625/arxiv
+        shell: bash
+        run: |
+          pages=$(pdfinfo AMS_SELF_CONTAINED_DRAFT_V3.pdf | awk '/^Pages:/ {print $2}')
+          test -n "$pages"
+          if [ "$pages" -lt 30 ]; then
+            echo "expected a full paper, found only $pages pages"
+            exit 1
+          fi
+          pdftotext AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-v3.txt
+          words=$(wc -w < /tmp/erdos625-v3.txt)
+          if [ "$words" -lt 15000 ]; then
+            echo "expected at least 15000 extracted words, found $words"
+            exit 1
+          fi
+          echo "pages: $pages"
+          echo "extracted words: $words"
+      - name: Render representative pages
+        working-directory: 625/arxiv
+        run: |
+          mkdir -p /tmp/erdos625-renders
+          pages=$(pdfinfo AMS_SELF_CONTAINED_DRAFT_V3.pdf | awk '/^Pages:/ {print $2}')
+          pdftoppm -f 1 -singlefile -png -r 144 \
+            AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-001
+          pdftoppm -f "$pages" -singlefile -png -r 144 \
+            AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-last
+      - name: Upload complete manuscript artifacts
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-self-contained-manuscript-v3
+          path: |
+            625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.pdf
+            625/arxiv/AMS_SELF_CONTAINED_BODY_V3.generated.tex
+            625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.log
+            /tmp/erdos625-renders/page-001.png
+            /tmp/erdos625-renders/page-last.png
+          if-no-files-found: error
diff --git a/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex b/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex
new file mode 100644
index 0000000..5f63ea3
--- /dev/null
+++ b/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex
@@ -0,0 +1,73 @@
+\documentclass[11pt,reqno]{amsart}
+
+\usepackage[letterpaper,margin=1in]{geometry}
+\usepackage[T1]{fontenc}
+\usepackage{newtxtext,newtxmath}
+\usepackage{microtype}
+\usepackage{amsmath,mathtools}
+\usepackage[authoryear,round]{natbib}
+\usepackage{enumitem}
+\usepackage{needspace}
+\usepackage{booktabs}
+\usepackage{longtable}
+\usepackage{array}
+\usepackage{xurl}
+\usepackage{xcolor}
+\usepackage[hidelinks]{hyperref}
+\usepackage{bookmark}
+
+\setcounter{secnumdepth}{2}
+\setcounter{tocdepth}{2}
+\setlength{\parindent}{1.45em}
+\setlength{\parskip}{0pt}
+\setlist[itemize]{leftmargin=2.05em,itemsep=0.12em,topsep=0.32em}
+\setlist[enumerate]{leftmargin=2.15em,itemsep=0.12em,topsep=0.32em}
+\setlength{\emergencystretch}{3em}
+\allowdisplaybreaks
+\providecommand{\tightlist}{%
+  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
+
+\newcommand{\Prob}[1]{\mathbb{P}\!\left(#1\right)}
+\newcommand{\Exp}[1]{\mathbb{E}\!\left[#1\right]}
+\newcommand{\Expres}[1]{\mathbb{E}_{\mathrm{res}}\!\left[#1\right]}
+\newcommand{\whp}{with high probability}
+\newcommand{\gnp}{G(n,1/2)}
+\newcommand{\gap}{\chi(G_n)-\zeta(G_n)}
+\newcommand{\displayheading}[1]{%
+  \par\addvspace{0.68\baselineskip}%
+  \noindent{\scshape #1.}\par\nobreak\smallskip\noindent}
+
+\input{AMS_THEOREM_ENVIRONMENTS_V3}
+
+% Verification status switch. This must remain false until the four remaining
+% DAG gates in Appendix A are green on one integrated private commit and have
+% been independently replayed.
+\newif\ifErdosProofClosed
+\ErdosProofClosedfalse
+
+\hypersetup{
+  pdftitle={A Full-Sequence Gap Between the Chromatic and Cochromatic Numbers of a Random Graph},
+  pdfauthor={Samuil Petkov},
+  pdfcreator={LaTeX}}
+
+\title[Chromatic and cochromatic numbers]{A Full-Sequence Polynomial Gap
+Between the Chromatic and Cochromatic Numbers of a Random Graph}
+\author[Samuil Petkov]{Samuil Petkov}
+\address{\'Ecole normale sup\'erieure, Universit\'e PSL, Paris, France}
+\email{samuil.petkov@ens.psl.eu}
+\subjclass[2020]{Primary 05C80; Secondary 05C15, 60C05}
+\keywords{random graph, chromatic number, cochromatic number, second moment method, configuration model}
+
+\begin{document}
+
+\input{FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3}
+\input{CONVENTIONS_AND_PROOF_OBJECTS_V3}
+\input{PROOF_ARCHITECTURE_SELF_CONTAINED_V3}
+\input{AMS_SELF_CONTAINED_BODY_V3.generated}
+\input{FORMALIZATION_STATUS_APPENDIX_V3}
+
+\renewcommand{\bibsection}{\section*{References}}
+\bibliographystyle{plainnat}
+\bibliography{references}
+
+\end{document}
diff --git a/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex b/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex
new file mode 100644
index 0000000..56b808a
--- /dev/null
+++ b/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex
@@ -0,0 +1,30 @@
+% Standard theorem environments for the self-contained Version 3 manuscript.
+% The legacy wrappers are compatibility shims for canonical sections imported by
+% the deterministic manuscript generator. New text must use the ordinary
+% amsthm environments directly.
+
+\theoremstyle{plain}
+\newtheorem{theorem}{Theorem}[section]
+\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{claim}[theorem]{Claim}
+
+\theoremstyle{definition}
+\newtheorem{definition}[theorem]{Definition}
+\newtheorem{convention}[theorem]{Convention}
+
+\theoremstyle{remark}
+\newtheorem{remark}[theorem]{Remark}
+
+% Compatibility only. The generator normally converts legacy statement boxes
+% to theorem, lemma, and proposition environments before compilation.
+\newenvironment{resultbox}[1]
+  {\par\medskip\noindent\textbf{#1.}\enspace\itshape\ignorespaces}
+  {\par\medskip}
+\newenvironment{lemmabox}[1]
+  {\par\medskip\noindent\textbf{#1.}\enspace\itshape\ignorespaces}
+  {\par\medskip}
+\newenvironment{propositionbox}[1]
+  {\par\medskip\noindent\textbf{#1.}\enspace\itshape\ignorespaces}
+  {\par\medskip}
diff --git a/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex b/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex
new file mode 100644
index 0000000..13cb60b
--- /dev/null
+++ b/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex
@@ -0,0 +1,155 @@
+\section*{Conventions and proof objects}
+\addcontentsline{toc}{section}{Conventions and proof objects}
+\label{sec:conventions-v3}
+
+This section fixes the standard graph-theoretic conventions and the
+manuscript-specific proof objects. Its purpose is to prevent the combinatorial,
+configuration-model, and type-level uses of the word \emph{matching} from
+being conflated later.
+
+\begin{convention}[Graphs and partitions]
+All graphs are finite, simple, and undirected. A partition always consists of
+nonempty, pairwise disjoint classes whose union is the whole vertex set. An
+independent set induces an edgeless graph, and a clique induces a complete
+graph. The chromatic number $\chi(G)$ is the least number of independent
+classes in a partition of $V(G)$. The cochromatic number $\zeta(G)$ is the
+least number of classes in a partition of $V(G)$ in which every class is either
+independent or a clique.
+\end{convention}
+
+\begin{definition}[Signed cocoloring witness]
+A \emph{signed cocoloring witness} consists of a vertex partition together
+with an $I$- or $K$-mark on each class. An $I$-marked class must be independent,
+and a $K$-marked class must be a clique. The marks are auxiliary counting data;
+they do not define a new graph invariant. In the four-size construction all
+classes have size at least two for sufficiently large $n$, so a realized class
+cannot be both independent and complete. Forgetting the marks therefore
+recovers the underlying cocoloring without multiplicity.
+\end{definition}
+
+\begin{convention}[Random graph and uniformity]
+The notation $G_n\sim G(n,1/2)$ refers to the labeled random graph on $[n]$ in
+which all $\binom n2$ edge indicators are independent Bernoulli variables of
+parameter $1/2$. All logarithms are natural. A statement holds with high
+probability if its probability tends to one as $n\to\infty$. An error term
+$o(1)$ is uniform in the phase whenever the phase variable is present. The
+phrase \emph{uniformly in the phase} means that one deterministic error
+sequence works for every phase value and every integer sequence approaching a
+phase endpoint.
+\end{convention}
+
+\begin{convention}[Falling factorials]
+For integers $x,r\ge0$, put
+\[
+  (x)_r=x(x-1)\cdots(x-r+1),\qquad (x)_0=1.
+\]
+We set $(x)_r=0$ for $r>x$. Quotient identities involving falling factorials
+are used only after feasibility and nonvanishing of the relevant denominator
+have been established.
+\end{convention}
+
+\begin{definition}[Profiles]
+A profile is a finite sequence $(k_s)$ in which $k_s$ is the number of classes
+of size $s$. It is feasible for $n$ vertices if
+\[
+  \sum_s k_s=k,
+  \qquad
+  \sum_s s k_s=n.
+\]
+The ordinary profile first moment counts partitions into independent classes.
+The signed profile first moment counts the same partitions together with an
+$I/K$ mark on every class.
+\end{definition}
+
+\begin{definition}[Overlap table]
+Let $(A_a)_a$ and $(B_b)_b$ be two ordered profile partitions. Their overlap
+table is
+\[
+  r_{ab}=|A_a\cap B_b|.
+\]
+Its row sums are the sizes of the $A_a$, and its column sums are the sizes of
+the $B_b$. The table is also the cell-count table of a bipartite configuration
+model: the vertices of $A_a$ are the row stubs of type $a$, the vertices of
+$B_b$ are the column stubs of type $b$, and the identity of the underlying
+vertex gives a perfect matching between the two stub families.
+\end{definition}
+
+\begin{definition}[Support graph and cycle rank]
+Given an overlap table $r$, let $H(r)$ be the simple bipartite graph whose edge
+set is
+\[
+  E(H(r))=\{(a,b):r_{ab}\ge2\}.
+\]
+A subset $F\subseteq E(H(r))$ is \emph{even} if every vertex has even degree
+in $(V(H(r)),F)$. Let $c(H)$ denote the number of connected components,
+including isolated vertices, and put
+\[
+  \beta(H)=|E(H)|-|V(H)|+c(H).
+\]
+Then $\beta(H)$ is the dimension of the binary cycle space and
+\[
+  |\{F\subseteq E(H):F\text{ is even}\}|=2^{\beta(H)}.
+\]
+The threshold $r_{ab}\ge2$ is exact: a cell of size zero or one contains no
+internal edge shared by the two partition classes, whereas a cell of size at
+least two contains a common internal edge and forces the two signs to agree.
+\end{definition}
+
+\begin{definition}[Three matching levels]
+Three distinct matching objects occur.
+\begin{enumerate}
+\item The \emph{configuration matching} is the perfect matching of all labeled
+row and column stubs induced by the common vertex set.
+\item A \emph{physical partial matching} is a set of selected individual stub
+pairs inside one or several prescribed overlap cells.
+\item A \emph{block support} is a matching between row-class slots and
+column-class slots. Its edges record which block pairs contain canonical high
+cells.
+\end{enumerate}
+The factorization of physical cell counts is valid only because the positive
+block support is a matching: distinct selected cells then use disjoint row and
+column stub families.
+\end{definition}
+
+\begin{definition}[Canonical high cells]
+Let $U$ be the largest class size in the fixed four-size profile, and put
+$R_0=\lfloor U/2\rfloor$. A cell is \emph{high} if its multiplicity exceeds
+$R_0$. Two high cells cannot share a row or a column, so the collection of all
+high cells is a canonical block matching. For a selected cell $e$, let
+\[
+  s_e,t_e\quad\text{be its endpoint sizes},\qquad
+  m_e=\min\{s_e,t_e\},\qquad
+  j_e=m_e-h_e.
+\]
+Here $m_e$ is the full-containment multiplicity, $j_e$ is the actual
+multiplicity, and $h_e$ is the deficit. The high-cell inequality implies
+$2h_e<m_e$.
+\end{definition}
+
+\begin{definition}[Endpoint table]
+The four consecutive endpoint sizes are indexed by $i,j\in\{0,1,2,3\}$. For a
+block support $P$, its endpoint table $L(P)=(L_{ij})$ records the number of
+support edges joining endpoint types $i$ and $j$. It is a $4\times4$
+nonnegative integer table with row and column margins bounded by the
+corresponding profile multiplicities. The phrase \emph{realized endpoint
+table} means a table attained by at least one finite block support; it does not
+mean an arbitrary element of $\mathbb N^{4\times4}$.
+\end{definition}
+
+\begin{definition}[Bare skeleton and residual attachment]
+The \emph{bare high-skeleton weight} contains the incidence probability of the
+exposed high cells and their local signed rewards. It contains neither the
+local rewards of unexposed cells nor the residual binary cycle-space factor.
+After a high skeleton has been fixed, the conditional expectation of those
+remaining factors is its \emph{residual attachment}. This division of labor is
+maintained throughout Sections~8 and~9; a factor paid in one part is never paid
+again in the other.
+\end{definition}
+
+\begin{remark}[Exact, deterministic, asymptotic, and probabilistic layers]
+Every load-bearing argument below is split into four layers. Finite identities
+are stated before any inequality. Deterministic inequalities are then applied
+to those exact quantities. Phase asymptotics are invoked only after the finite
+summation has been completed. Probability conclusions are deduced last. This
+separation is essential for auditing both the manuscript and the Lean proof.
+\end{remark}
diff --git a/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex b/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex
new file mode 100644
index 0000000..83ce41b
--- /dev/null
+++ b/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex
@@ -0,0 +1,180 @@
+\section{Final assembly and the quantitative constant}
+\label{sec:final-assembly-v3}
+
+We assemble the ordinary coloring lower bound, the signed cocoloring upper
+bound, and the exact constant ledger. No independence between the two final
+events is required.
+
+Let $r_+(n)$ denote the ordinary first-moment root and let
+$r_4^{\mathrm{co}}(n)$ denote the signed four-size root. Section~5 proves
+\begin{equation}
+  r_+(n)-r_4^{\mathrm{co}}(n)
+  =
+  \left[
+    \frac{(\log2)^2}{4}A_4(\delta_n)+o(1)
+  \right]
+  \frac{n}{(\log n)^3},
+  \qquad
+  A_4(\delta):=\log2-D_4(\delta).
+  \label{eq:phase-resolved-root-gap-v3}
+\end{equation}
+The tangent-rounded signed profile is placed at
+\[
+  k_{\mathrm{co}}
+  =
+  \left\lceil
+    \frac{r_4^{\mathrm{co}}(n)+r_+(n)}2
+  \right\rceil+O(1),
+\]
+where the bounded correction enforces the two exact profile conservation laws.
+Consequently
+\begin{equation}
+  r_+(n)-k_{\mathrm{co}}
+  =
+  \left[
+    \frac{(\log2)^2}{8}A_4(\delta_n)+o(1)
+  \right]
+  \frac{n}{(\log n)^3}.
+  \label{eq:midpoint-retained-gap-v3}
+\end{equation}
+Indeed, taking the midpoint divides the leading root separation by two, while
+the ceiling and tangent correction contribute only $O(1)$ classes.
+
+Section~4 gives a deterministic integer $k_\chi^-$ such that
+\[
+  \mathbb P\bigl(\chi(G_n)>k_\chi^-\bigr)\longrightarrow1
+\]
+and
+\begin{equation}
+  k_\chi^- - k_{\mathrm{co}}
+  =
+  \left[
+    \frac{(\log2)^2}{8}A_4(\delta_n)+o(1)
+  \right]
+  \frac{n}{(\log n)^3}.
+  \label{eq:integer-location-gap-v3}
+\end{equation}
+
+Proposition~\ref{prop:normalized-second-moment-v3} and Paley--Zygmund give a
+signed witness with probability at least $e^{-\Lambda_n}$, where
+\[
+  \Lambda_n=o\!\left(\frac{n}{(\log n)^4}\right).
+\]
+Section~10 applies the rare-seed amplifier and the simultaneous leftover
+coloring theorem. It produces a deterministic $a_n$ such that
+\[
+  a_n=o\!\left(\frac{n}{(\log n)^3}\right)
+\]
+and
+\[
+  \mathbb P\bigl(\zeta(G_n)\le k_{\mathrm{co}}+a_n\bigr)
+  \longrightarrow1.
+\]
+Intersecting the two high-probability events by a union bound and using
+\eqref{eq:integer-location-gap-v3} proves the phase-resolved conclusion
+\begin{equation}
+  \chi(G_n)-\zeta(G_n)
+  \ge
+  \left[
+    \frac{(\log2)^2}{8}A_4(\delta_n)-o(1)
+  \right]
+  \frac{n}{(\log n)^3}
+  \label{eq:phase-resolved-final-v3}
+\end{equation}
+with high probability.
+
+\subsection{Exact four-support certificate}
+
+For completeness, we record the elementary uniform certificate used to turn
+\eqref{eq:phase-resolved-final-v3} into a fixed constant. Let $\lambda_4$ be
+the tilt of the limiting four-deficit optimizer. Exact rational estimates give
+\[
+  \frac{49}{20}\log2
+  <
+  \lambda_4
+  <
+  \frac{83}{20}\log2.
+\]
+Split the omitted limiting mass at $(29/10)\log2$. If $L(\lambda)$ and
+$H(\lambda)$ denote the omitted low- and high-deficit ratios, respectively,
+the following four bounds hold:
+\[
+  L\!\left(\frac{49}{20}\log2\right)<\frac{263}{1000},
+  \qquad
+  H\!\left(\frac{29}{10}\log2\right)<\frac3{200},
+\]
+\[
+  L\!\left(\frac{29}{10}\log2\right)<\frac{33}{250},
+  \qquad
+  H\!\left(\frac{83}{20}\log2\right)<\frac{29}{200}.
+\]
+Monotonicity of the two omitted tails therefore gives
+\[
+  L(\lambda_4)+H(\lambda_4)<\frac{139}{500}.
+\]
+Evaluating the unrestricted dual objective at the four-support optimizer yields
+\[
+  D_4(\delta)
+  \le
+  \log\bigl(1+L(\lambda_4)+H(\lambda_4)\bigr)
+  <
+  \log\!\left(\frac{639}{500}\right).
+\]
+Hence, uniformly for $0\le\delta\le1$,
+\begin{equation}
+  A_4(\delta)
+  =
+  \log2-D_4(\delta)
+  >
+  \log\!\left(\frac{1000}{639}\right).
+  \label{eq:exact-four-support-certificate-v3}
+\end{equation}
+
+Combining \eqref{eq:phase-resolved-final-v3} and
+\eqref{eq:exact-four-support-certificate-v3} gives
+\[
+  \chi(G_n)-\zeta(G_n)
+  \ge
+  \left[
+    \frac{(\log2)^2}{8}
+    \log\!\left(\frac{1000}{639}\right)-o(1)
+  \right]
+  \frac{n}{(\log n)^3}
+\]
+with high probability. The fixed coefficient is
+\[
+  \frac{(\log2)^2}{8}
+  \log\!\left(\frac{1000}{639}\right)
+  =0.026896409808379\ldots.
+\]
+
+\ifErdosProofClosed
+This proves Theorem~\ref{thm:main-v3}. Since $n/(\log n)^3\to\infty$, the
+chromatic--cochromatic difference tends to infinity with high probability
+along the full sequence of integers.
+\else
+Equations \eqref{eq:phase-resolved-final-v3} and
+\eqref{eq:exact-four-support-certificate-v3} prove the target theorem
+conditional on the four formal gates stated in Appendix~A. The publication
+switch remains disabled until those gates are independently validated.
+\fi
+
+\begin{corollary}[Simultaneous complement form]
+Under the hypotheses of Theorem~\ref{thm:main-v3},
+\[
+  \min\{\chi(G_n),\chi(\overline{G_n})\}-\zeta(G_n)
+  \ge
+  \left[
+    \frac{(\log2)^2}{8}
+    \log\!\left(\frac{1000}{639}\right)-o(1)
+  \right]
+  \frac{n}{(\log n)^3}
+\]
+with high probability.
+\end{corollary}
+
+\begin{proof}
+The law of $\overline{G_n}$ is again $G(n,1/2)$, and
+$\zeta(\overline G)=\zeta(G)$. Apply the theorem simultaneously to $G_n$ and
+its complement and intersect the two events by a union bound.
+\end{proof}
diff --git a/625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex b/625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex
new file mode 100644
index 0000000..22a5b86
--- /dev/null
+++ b/625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex
@@ -0,0 +1,170 @@
+\appendix
+
+\section{Formalization map and publication gates}
+\label{app:formalization-status-v3}
+
+This appendix records the relation between the manuscript and the private Lean
+4.31 project.  It is part of the verification draft because the size of the
+formal code base must not be confused with completion of the top-level theorem.
+A declaration is treated as proof evidence only after exact-signature review,
+warning-fatal replay under the pinned toolchain, a forbidden-shortcut scan, an
+axiom audit, and independent mathematical review.
+
+\subsection{Status vocabulary}
+
+\begin{description}
+\item[Welded.] The exact declaration has passed focused and root replay, its
+axioms have been audited, and it belongs to the canonical private import
+closure.
+\item[Running.] An exact one-hole theorem request has been approved and
+submitted, but no returned candidate is proof evidence until the complete
+independent replay protocol has passed.
+\item[Needs review.] The mathematical task is known, but its exact theorem
+signature, constants, quantifiers, and dependency ledger have not all been
+frozen.
+\item[Blocked.] A downstream theorem whose declared dependencies are not yet
+all welded.
+\end{description}
+
+\subsection{Section 8 finite chain}
+
+The following finite Section~8 declarations are welded privately.  The
+\verb|\path| form is used deliberately so that long theorem names can break at
+underscores without leaving the page.
+
+\begingroup
+\small
+\begin{longtable}{>{\raggedright\arraybackslash}p{0.19\linewidth}
+                  >{\raggedright\arraybackslash}p{0.58\linewidth}
+                  >{\raggedright\arraybackslash}p{0.12\linewidth}}
+\toprule
+Manuscript role & Lean declaration or DAG node & Status\\
+\midrule
+\endhead
+High-support encoding &
+\path{encodeRawNearMiddle_injective} & Welded\\
+Physical fiber and partial weight &
+\path{profileHighSkeletonWeight_eq_fourEndpointPartialAggregateWeight} & Welded\\
+One global deficit charge &
+\path{profileHighSkeletonWeight_le_fourEndpointFullReference_mul_deficitCharge} & Welded\\
+Fixed-support deficit product &
+\path{sum_fourEndpointAllHighChoiceWeight_le_threeQuarterProduct} & Welded\\
+Encoded full-support comparison &
+\path{profileHighSkeletonWeight_le_fourEndpointEncodedFullSupportCharge} & Welded\\
+Weighted realized-table regrouping &
+\path{sum_fourEndpointFullSupportReferenceWeight_mul_tableWeight_eq_sum_realized_W_mul_tableWeight} & Welded\\
+Realized-table deficit sum &
+\path{sum_profileHighSkeletonWeight_le_realizedTableThreeQuarterProduct} & Welded\\
+Coarse phase corridor &
+\path{eventually_five_fourths_log_sub_le_q_mul_endpointBudget} & Welded\\
+Canonical common-charge smallness &
+\path{eventually_fourEndpointThreeQuarterRho_le_one} & Running\\
+\bottomrule
+\end{longtable}
+\endgroup
+
+The welded finite chain verifies the completion-free physical-fiber
+factorization, the exact local-to-full comparison, the single global
+falling-factorial loss, the deficit product, and both unweighted and weighted
+regrouping over realized endpoint tables.  The current running theorem is the
+remaining real-to-\texttt{ENNReal} phase estimate for the explicit sum of the
+sixteen endpoint bases.
+
+The main text uses the coarse common-charge route
+\[
+  \rho_{16}\le1
+  \quad\Longrightarrow\quad
+  \left(1+(\alpha+1)\rho_{16}\right)^K.
+\]
+This route is aligned with the private finite reduction.  The stronger
+pointwise hypothesis $\rho_{ij}\le1/2$ yields the table-preserving product
+$\prod_{i,j}(1+2\rho_{ij})^{L_{ij}}$ and remains a reusable corollary, but it is
+not required for the shortest proof closure.
+
+\subsection{Other remaining theorem nodes}
+
+The top-level proof also depends on the following nodes.
+
+\begin{longtable}{>{\raggedright\arraybackslash}p{0.22\linewidth}
+                  >{\raggedright\arraybackslash}p{0.49\linewidth}
+                  >{\raggedright\arraybackslash}p{0.18\linewidth}}
+\toprule
+Paper section & Exact remaining obligation & Status\\
+\midrule
+\endhead
+Sections 2--4 & Freeze the concrete phase center, slope, and root package, then
+export the chromatic lower-tail theorem with the required full-sequence
+quantifiers. & Needs review\\
+Section 5 & Assemble the welded four-support entropy certificate, the root
+separation, tangent rounding, and the positive signed first moment into one
+exact theorem consumed by the final adapter. & Needs review\\
+Section 7 & Split and prove the empty-corner, central-rate, and full-corner
+asymptotic sums uniformly in the phase; only the exact full-corner reindexing is
+currently welded. & Needs review\\
+Sections 8--9 & Combine phase smallness, endpoint transport, the skeleton
+quotient estimate, and the welded residual attachment theorem into the global
+normalized-second-moment hypothesis. & Blocked on the preceding nodes\\
+Sections 10--11 & The conditional rare-seed amplifier and final event adapter
+are welded, but their concrete hypotheses must be instantiated by the preceding
+nodes. & Conditional adapter welded\\
+\bottomrule
+\end{longtable}
+
+The partial-diagonal node is the largest remaining analytic formalization.  It
+should be divided into four exact declarations rather than submitted as one
+broad request:
+\[
+  \text{empty corner},\quad
+  \text{central rate},\quad
+  \text{full-corner wrapper},\quad
+  \text{partial-diagonal assembly}.
+\]
+The same discipline should be used for the phase and first-moment nodes.
+
+\subsection{Publication gate}
+
+The compile-time switch \verb|\ErdosProofClosedtrue| may be enabled only after
+all of the following hold on one integrated commit:
+
+\begin{enumerate}
+\item the canonical common-charge smallness theorem is welded;
+\item the skeleton quotient and global attachment sum are welded;
+\item the complete partial-diagonal asymptotic theorem is welded;
+\item the concrete phase/chromatic-tail package is welded;
+\item the signed four-size first-moment assembly is welded;
+\item the conditional final adapter is replayed against those exact outputs;
+\item the public theorem-facing Lean root is regenerated and warning-fatal;
+\item the manuscript constants, quantifiers, bibliography, and theorem names
+are synchronized with that root;
+\item the full TeX source compiles without unresolved references, citations,
+or status placeholders;
+\item an independent mathematical review confirms that no private or public
+staging lemma is being counted twice.
+\end{enumerate}
+
+Until these gates close, the verification banner and conditional theorem
+statement in the front matter are mandatory.
+
+\subsection{Recommended theorem-facing Lean organization}
+
+The internal project contains hundreds of fine-grained modules, including both
+legacy and simplified proof routes.  For publication, the formalization should
+export a small curated root:
+\begin{itemize}
+\item \path{Erdos625/Paper/Phase.lean};
+\item \path{Erdos625/Paper/FirstMoment.lean};
+\item \path{Erdos625/Paper/PartialDiagonals.lean};
+\item \path{Erdos625/Paper/HighSkeletons.lean};
+\item \path{Erdos625/Paper/Attachments.lean};
+\item \path{Erdos625/Paper/Amplification.lean};
+\item \path{Erdos625/Paper/Main.lean}.
+\end{itemize}
+The paper-facing root should import only the declarations corresponding to
+named manuscript results.  The complete historical development may remain in
+a separate exhaustive root, and the superseded cycle/walk route should be
+marked as legacy rather than appearing in the main theorem dependency chain.
+
+A machine-readable manifest should map every named paper result to its exact
+Lean declaration, source file, commit, status, and axiom audit.  The
+formalization appendix and reproducibility table can then be generated from
+that manifest, eliminating manual status drift.
diff --git a/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex b/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex
new file mode 100644
index 0000000..8701670
--- /dev/null
+++ b/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex
@@ -0,0 +1,194 @@
+% Front matter for the self-contained Version 3 manuscript.
+% The compile-time switch \ifErdosProofClosed is defined by the master file.
+% It must remain false until the proof-closure checklist in Appendix A is green
+% on one integrated commit.
+
+\begin{abstract}
+\ifErdosProofClosed
+Let $G_n\sim G(n,1/2)$. We prove that the difference between the chromatic
+number $\chi(G_n)$ and the cochromatic number $\zeta(G_n)$ is bounded below by
+a positive constant times $n/(\log n)^3$ with probability tending to one. The
+argument is uniform across the full rounding phase of the independence-number
+threshold. Its first-moment component compares ordinary colorings with signed
+cocoloring witnesses supported on four consecutive class sizes. For the second
+moment, we derive an exact sign-compatibility identity, encode the large
+overlap cells by a matching with local deficits, sum the corresponding physical
+matching fibers exactly, and control the residual even-subgraph factor by
+injective restriction outside the exposed matching. A bounded-differences
+argument then amplifies the resulting positive-probability seed to a
+high-probability cocoloring.
+\else
+This verification draft assembles a self-contained proof architecture for a
+full-sequence lower bound on $\chi(G_n)-\zeta(G_n)$ in $G(n,1/2)$. It includes
+the complete manuscript argument, the replacement high-skeleton and residual
+attachment sections, and an explicit map to the current Lean formalization.
+The displayed target theorem is not promoted as proved until the remaining
+phase, partial-diagonal, and global assembly gates listed in Appendix~A are
+validated on one integrated commit. This status distinction is part of the
+manuscript rather than being left only in repository metadata.
+\fi
+\end{abstract}
+
+\maketitle
+
+\ifErdosProofClosed\else
+\begin{center}
+\fbox{\parbox{0.91\linewidth}{\small
+\textbf{Verification draft.}
+The finite Section~8 bridge through the realized endpoint-table deficit sum is
+kernel-checked privately, but the full theorem is still conditional on the
+remaining formal gates stated in Appendix~A. The publication switch in the
+master file must remain disabled until those gates close.}}
+\end{center}
+\fi
+
+\section*{Introduction}
+\addcontentsline{toc}{section}{Introduction}
+\label{sec:introduction-v3}
+
+All graphs in this paper are finite, simple, and undirected. A
+\emph{cocoloring} of a graph $G$ is a partition of $V(G)$ into nonempty
+classes, each of which is either an independent set or a clique. The least
+number of classes in such a partition is the \emph{cochromatic number}
+$\zeta(G)$. We write $\chi(G)$ for the chromatic number. These are the
+standard graph invariants; the signed objects introduced below are auxiliary
+counting witnesses and do not define a new invariant.
+
+Let $G_n\sim G(n,1/2)$ be the labeled random graph on $[n]$ in which the
+$\binom n2$ possible edges occur independently with probability $1/2$. An
+event holds \emph{with high probability} if its probability tends to one as
+$n\to\infty$.
+
+Erd\H{o}s and Gimbel asked whether
+\[
+  \chi(G_n)-\zeta(G_n)\longrightarrow\infty
+\]
+with high probability \citep[p.~263]{erdos-gimbel-1993}. The problem was
+later restated by Gimbel \citep[Section~7.4]{gimbel-2016} and is cataloged as
+Erd\H{o}s Problem~625 \citep{bloom-erdos625}. The intended final result is the
+following full-sequence quantitative statement.
+
+\ifErdosProofClosed
+\begin{theorem}\label{thm:main-v3}
+For $G_n\sim G(n,1/2)$,
+\[
+  \mathbb P\!\left(
+    \chi(G_n)-\zeta(G_n)
+    \ge
+    \frac{(\log 2)^2}{8}
+    \log\!\left(\frac{1000}{639}\right)
+    \frac{n}{(\log n)^3}
+  \right)
+  \longrightarrow 1.
+\]
+In particular, $\chi(G_n)-\zeta(G_n)$ tends to infinity with high probability
+along the full sequence of integers $n$.
+\end{theorem}
+\else
+\begin{theorem}[Target theorem]\label{thm:main-v3}
+Assume the concrete phase package, the signed four-size first-moment assembly,
+the complete partial-diagonal estimate, and the global attachment assembly
+listed in Appendix~A. Then, for $G_n\sim G(n,1/2)$,
+\[
+  \mathbb P\!\left(
+    \chi(G_n)-\zeta(G_n)
+    \ge
+    \frac{(\log 2)^2}{8}
+    \log\!\left(\frac{1000}{639}\right)
+    \frac{n}{(\log n)^3}
+  \right)
+  \longrightarrow 1.
+\]
+\end{theorem}
+\fi
+
+The full-sequence quantifier is essential. Near a jump of the
+independence-number threshold, changing the relevant class size by one changes
+the feasible profile. A result proved only on a density-one set of phase
+values therefore need not extend to every integer $n$. Every asymptotic
+estimate below is stated uniformly in the complete phase parameter, including
+sequences approaching either endpoint of a phase interval.
+
+\subsection*{Background}
+
+The chromatic number of dense random graphs has been studied since the work of
+Grimmett and McDiarmid \citep{grimmett-mcdiarmid-1975}. The first-order
+asymptotic was established by Bollob\'as \citep{bollobas-1988}; later
+refinements include \citet{mcdiarmid-1990},
+\citet{panagiotou-steger-2009}, and \citet{heckel-2018}. The cochromatic
+number belongs to the theory of generalized chromatic numbers for hereditary
+graph properties developed by Scheinerman and Bollob\'as--Thomason
+\citep{scheinerman-1992,bollobas-thomason-1995}.
+
+For the chromatic--cochromatic difference, Heckel and, independently, Steiner
+obtained the first quantitative evidence toward divergence
+\citep{heckel-2024-question,steiner-2024}. Heckel subsequently proved a much
+larger lower bound on a phase-dependent set containing approximately $95\%$ of
+the integers \citep{heckel-2025-difference}. The remaining difficulty is to
+control the complete phase uniformly. The present argument uses the signed
+first-moment gain and rare-seed amplification from that work, but replaces the
+pairwise sign bound by an exact overlap identity and treats every phase with
+one four-size profile.
+
+\subsection*{Contributions}
+
+The proof is organized around five results that are mathematically distinct
+and should be read separately.
+
+\begin{enumerate}
+\item A phase-uniform comparison between the ordinary coloring root and a
+four-size signed cocoloring root gives a separation of order
+$n/(\log n)^3$.
+\item The sign compatibility of two witnesses is evaluated exactly. The
+result is a product of local cell rewards multiplied by the cardinality of a
+binary cycle space.
+\item A completion-free high-skeleton theorem identifies every
+matching-supported physical demand fiber with a product of literal one-cell
+partial matching fibers. The ambient falling-factorial loss is then charged
+once, after the fiber sum.
+\item An exact regrouping identity transports full-support reference weights
+through the realized endpoint-table decomposition. The main proof uses a
+coarse common charge, while a sharper table-preserving version is retained as
+a separate reusable statement.
+\item Deletion of the exposed matching is injective on the family of even
+residual edge sets. This gives a direct restriction-product estimate and
+removes the need for a simple-cycle or walk-kernel decomposition in the final
+argument.
+\end{enumerate}
+
+The exact signed-overlap identity, the completion-free matching-fiber
+factorization, the weighted realized-table regrouping, the restriction-product
+lemma, and the rare-seed amplifier are stated as independent propositions or
+lemmas. This separates the reusable finite mathematics from the phase-specific
+random-graph estimates.
+
+\subsection*{Proof structure}
+
+The proof has three layers.
+
+The \emph{location layer} compares the ordinary first-moment root with the
+signed four-size root. The \emph{existence layer} proves a normalized
+second-moment estimate for one tangent-rounded signed profile. The
+\emph{amplification layer} converts the positive-probability signed witness into
+a high-probability upper bound for $\zeta(G_n)$ and intersects it with the
+chromatic lower bound.
+
+The difficult overlap calculation is itself divided into four operations:
+partial diagonals, canonical high cells, residual attachments, and final
+normalization. Each operation has a separate theorem contract. In particular,
+no residual local or cycle-space factor is charged in the high-skeleton
+section, and no high-cell multiplicity is charged again in the residual
+section.
+
+\subsection*{Organization}
+
+Section~1 fixes the phase notation and elementary inequalities. Sections~2--4
+locate the ordinary coloring root and derive an unrestricted lower bound for
+$\chi(G_n)$. Section~5 constructs the signed four-size profile and proves the
+root separation. Section~6 gives the exact signed-overlap identity, and
+Section~7 controls partial diagonals. Section~8 proves the completion-free
+high-skeleton estimate and endpoint transport. Section~9 treats the residual
+attachment by matching restriction. Section~10 proves the rare-seed amplifier,
+and Section~11 assembles the final events and the strengthened constant.
+Appendix~A records the exact paper-to-Lean map and the remaining verification
+gates.
diff --git a/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex b/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex
new file mode 100644
index 0000000..69d4a7c
--- /dev/null
+++ b/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex
@@ -0,0 +1,136 @@
+\section*{Proof architecture}
+\addcontentsline{toc}{section}{Proof architecture}
+\label{sec:proof-architecture-v3}
+
+The proof consists of three logically separate stages: location, existence,
+and amplification. This section records only the dependency structure. Every
+identity and estimate is proved in the numbered section where it is used.
+
+\subsection*{Location: two first-moment roots}
+
+Let $r_+(n)$ be the continuous root of the ordinary profile first moment, and
+let $r_4^{\mathrm{co}}(n)$ be the root of the signed objective restricted to
+the four deficits $2,3,4,5$. If $\delta_n$ is the phase parameter, write
+\[
+  A_4(\delta)=\log2-D_4(\delta),
+\]
+where $D_4(\delta)$ is the entropy loss caused by restricting the limiting
+deficit distribution to four values. The phase-uniform first-moment analysis
+gives
+\[
+  r_+(n)-r_4^{\mathrm{co}}(n)
+  =
+  \left[
+    \frac{(\log2)^2}{4}A_4(\delta_n)+o(1)
+  \right]
+  \frac{n}{(\log n)^3}.
+\]
+The signed witness is placed at the tangent-rounded midpoint of these roots.
+Rounding costs $O(1)$ classes and therefore does not alter the scale. The
+retained root gap is
+\[
+  \left[
+    \frac{(\log2)^2}{8}A_4(\delta_n)+o(1)
+  \right]
+  \frac{n}{(\log n)^3}.
+\]
+The exact four-support certificate gives
+\[
+  A_4(\delta)>\log\!\left(\frac{1000}{639}\right)
+  \qquad(0\le\delta\le1).
+\]
+
+\subsection*{Existence: one normalized second moment}
+
+For two ordered signed witnesses, let $r=(r_{ab})$ be their overlap table.
+The sign sum is evaluated exactly:
+\[
+  \operatorname{wt}_{\mathrm{sign}}(r)
+  =
+  \left(\prod_{a,b}g(r_{ab})\right)2^{\beta(H(r))}.
+\]
+The normalized second moment is then divided into partial diagonals, canonical
+high cells, and residual attachments.
+
+Section~7 proves that the partial-diagonal contribution is $1+o(1)$. In the
+remaining tables, every cell above half the phase cap is unique in its row and
+column, so the high support is a block matching.
+
+For a fixed block support $P$, actual multiplicities $j_e=m_e-h_e$, and
+$J=\sum_ej_e$, the complete physical matching fiber has aggregate weight
+\[
+  w(P,j)
+  =
+  \frac{\prod_{e\in P}(s_e)_{j_e}(t_e)_{j_e}}
+       {(n)_J\prod_{e\in P}j_e!}
+  \prod_{e\in P}g(j_e).
+\]
+The one-cell partial-to-full ratio is exact, and the only nonlocal change is
+one falling-factorial ratio. Writing $H=\sum_eh_e$,
+\[
+  \frac{(n)_{J+H}}{(n)_J}=(n-J)_H\le n^H.
+\]
+The factor $n^H$ is paid once, after the physical fiber has been summed.
+
+The main proof uses the canonical common charge
+\[
+  \rho_{16}(n,\alpha)
+  :=
+  \sum_{i,j=0}^{3}
+  \frac{n m_{ij}}
+       {2^{\lfloor(3m_{ij}-1)/4\rfloor}},
+  \qquad
+  m_{ij}=\min\{u_i,u_j\}.
+\]
+The finite deficit sum is bounded by
+\[
+  \sum_{\text{high skeletons}}w_{\mathrm{hi}}
+  \le
+  \left(\sum_LW(L)\right)
+  \left(1+(\alpha+1)\rho_{16}\right)^K,
+\]
+where $K$ is the total number of four-endpoint block slots. This is the
+canonical route because it needs only $\rho_{16}\le1$ and avoids a separate
+geometric-series theorem. The phase estimates imply
+\[
+  \rho_{16}=O\!\left(\frac{\log n}{n^{1/4}}\right),
+  \qquad
+  K(\alpha+1)\rho_{16}=O(n^{3/4}\log n)
+  =o\!\left(\frac{n}{(\log n)^4}\right).
+\]
+Endpoint transport and the partial-diagonal theorem then give
+\[
+  \operatorname{BareSkeletonSum}_n
+  \le
+  \exp\!\left\{o\!\left(\frac{n}{(\log n)^4}\right)\right\}.
+\]
+
+A sharper table-preserving statement is also available. If every local base is
+at most $1/2$, then the complete positive-deficit fiber is at most twice that
+base, and the exact weighted regrouping retains the product
+$\prod_{i,j}(1+2\rho_{ij})^{L_{ij}}$. This stronger finite theorem is useful
+independently, but it is not needed for the shortest closure route.
+
+After a high skeleton has been fixed, Section~9 defines one residual activity
+$q_{ab}$. The local increment activity is pointwise at most $q_{ab}$, and
+deleting the exposed matching is injective on the family of even residual edge
+sets. Consequently both residual products are bounded by
+\[
+  \exp\!\left(2\sum_{a,b}q_{ab}\right).
+\]
+A two-regime estimate makes this uniform at the scale
+$o(n/(\log n)^4)$, completing the normalized second-moment estimate.
+
+\subsection*{Amplification and final assembly}
+
+Paley--Zygmund yields a signed witness with probability at least
+$e^{-\Lambda_n}$, where
+\[
+  \Lambda_n=o\!\left(\frac{n}{(\log n)^4}\right).
+\]
+The largest induced subgraph admitting the prescribed number of cocoloring
+classes is one-Lipschitz under vertex-block exposure. A one-sided
+bounded-differences argument moves the rare seed to the mean, and a
+simultaneous leftover-coloring theorem colors the omitted vertices with
+$o(n/(\log n)^3)$ additional classes. Intersecting the resulting cocoloring
+upper bound with the ordinary coloring lower bound proves the final gap.
diff --git a/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex
new file mode 100644
index 0000000..16791e4
--- /dev/null
+++ b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex
@@ -0,0 +1,515 @@
+\section{Canonical high cells and endpoint transport}
+\label{sec:canonical-high-cells-v3}
+
+This section bounds the contribution of all canonical high cells before any
+residual local reward or cycle-space factor is charged.  The proof has five
+logically separate stages:
+
+\begin{enumerate}
+\item sum the complete physical matching fiber for a fixed high-cell demand;
+\item compare each actual multiplicity with its full-containment value;
+\item pay the ambient falling-factorial loss once, after the fiber sum;
+\item sum all admissible positive deficits by a finite product;
+\item regroup the full references by endpoint table and transport them to the
+partial-diagonal weights of Section~7.
+\end{enumerate}
+
+No individual partial matching is assigned a preferred full completion.
+
+\subsection{Canonical support and exact aggregate weight}
+
+Let $U$ be the largest size in the fixed four-size profile and put
+\[
+  R_0:=\left\lfloor\frac U2\right\rfloor.
+\]
+A cell of an overlap table is \emph{high} if its multiplicity is greater than
+$R_0$.  Two high cells cannot share a row or a column, since either occurrence
+would use more than $U$ stubs in that row or column.  Hence the set of all high
+cells is a canonical bipartite matching, denoted by $P$.
+
+For $e\in P$, let $s_e$ and $t_e$ be the endpoint block sizes and define
+\[
+  m_e:=\min\{s_e,t_e\},
+  \qquad
+  d_e:=|s_e-t_e|,
+  \qquad
+  j_e:=m_e-h_e.
+\]
+The actual multiplicity is $j_e$ and the deficit is $h_e$.  Since
+$j_e>U/2$ and $m_e\le U$,
+\begin{equation}
+  2h_e<m_e.
+  \label{eq:half-deficit-v3}
+\end{equation}
+Put $J:=\sum_{e\in P}j_e$.
+
+A size-$j$ physical partial matching between labeled blocks of sizes $s$ and
+$t$ has cardinality
+\[
+  \binom sj\binom tj j!
+  =
+  \frac{(s)_j(t)_j}{j!}.
+\]
+Indeed, one chooses the row stubs, the column stubs, and then a bijection
+between the two selected sets.
+
+\begin{proposition}[Completion-free aggregate weight]
+\label{prop:aggregate-high-weight-v3}
+For a fixed matching support $P$ and multiplicity vector
+$j=(j_e)_{e\in P}$, the sum of the bare weights of all physical partial
+matchings realizing these data 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).
+  \label{eq:aggregate-high-weight-v3}
+\end{equation}
+\end{proposition}
+
+\begin{proof}
+Because $P$ is a matching, distinct selected cells use disjoint row and column
+stub families.  The complete physical fiber is therefore the Cartesian product
+of the one-cell partial-matching fibers, so its cardinality is the product of
+the one-cell cardinalities displayed above.  A prescribed set of $J$ stub
+pairs has probability $(n)_J^{-1}$ in the uniform bipartite configuration
+matching, and the exposed cells contribute the local signed reward
+$\prod_{e\in P}g(j_e)$.  Multiplication gives
+\eqref{eq:aggregate-high-weight-v3}.
+\end{proof}
+
+\begin{remark}
+The matching hypothesis is essential.  If two positive cells share a row or a
+column, their choices compete for the same stubs and the product of the
+one-cell cardinalities is false.
+\end{remark}
+
+\subsection{Exact local ratio and one global denominator loss}
+
+For endpoint sizes $m$ and $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},
+  \qquad
+  R_{m,d}(0):=1.
+  \label{eq:local-deficit-ratio-v3}
+\end{equation}
+The empty product is one.
+
+\begin{lemma}[Exact one-cell deficit ratio]
+\label{lem:exact-local-ratio-v3}
+The ratio of the aggregate one-cell factor at multiplicity $m-h$ to its
+full-containment value at multiplicity $m$ is $R_{m,d}(h)$.
+\end{lemma}
+
+\begin{proof}
+The ratio of the physical matching counts is
+\[
+  \frac{(m)_{m-h}(m+d)_{m-h}}{(m-h)!}
+  \frac{m!}{(m)_m(m+d)_m}
+  =
+  \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)}.
+\]
+The signed local reward satisfies
+\[
+  \frac{g(m-h)}{g(m)}
+  =
+  2^{-hm+h(h+1)/2}.
+\]
+Multiplying these exact identities proves the lemma.
+\end{proof}
+
+Let
+\[
+  J_*:=\sum_{e\in P}m_e,
+  \qquad
+  H:=J_*-J=\sum_{e\in P}h_e.
+\]
+The only nonlocal ratio between the actual and full-containment weights is
+\begin{equation}
+  \frac{(n)_{J_*}}{(n)_J}
+  =(n-J)_H
+  \le n^H.
+  \label{eq:one-global-falling-factorial-v3}
+\end{equation}
+
+\begin{lemma}[Aggregate deficit comparison]
+\label{lem:aggregate-deficit-comparison-v3}
+For every admissible deficit vector $h=(h_e)_{e\in P}$,
+\begin{equation}
+  w(P,m-h)
+  \le
+  w_{\mathrm{full}}(P)
+  \prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e).
+  \label{eq:aggregate-deficit-comparison-v3}
+\end{equation}
+\end{lemma}
+
+\begin{proof}
+Apply Lemma~\ref{lem:exact-local-ratio-v3} in each selected cell.  Apply
+\eqref{eq:one-global-falling-factorial-v3} once to the ambient denominator,
+and then use $n^H=\prod_e n^{h_e}$.
+\end{proof}
+
+Thus the global finite-population loss is paid only after the physical fiber
+has been summed.
+
+\subsection{The finite all-deficit product}
+
+For one selected cell, enlarge the exact positive-deficit set to
+\[
+  A_e:=\{h\in\mathbb N:h\ge1,\ 2h<m_e\}.
+\]
+All summands are nonnegative, so this enlargement preserves the upper-bound
+direction.
+
+\begin{lemma}[Optional-choice product]
+\label{lem:optional-choice-product-v3}
+Let $u_e(h)\ge0$ for $e\in P$ and $h\in A_e$.  Then
+\[
+  \sum_{\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 $\omega_e$ is either the zero-deficit choice, of weight one, or one
+positive deficit $h\in A_e$.
+\end{lemma}
+
+\begin{proof}
+Expand the finite product.  Every monomial chooses independently in each cell
+either the constant term or one positive-deficit term, and every optional
+choice appears exactly once.
+\end{proof}
+
+For $2h<m$, the integer inequality
+\begin{equation}
+  h\left\lfloor\frac{3m-1}{4}\right\rfloor
+  \le
+  hm-\frac{h(h+1)}2
+  \label{eq:three-quarter-budget-v3}
+\end{equation}
+combined with $\binom mh\le m^h$ and
+\eqref{eq:local-deficit-ratio-v3} gives
+\begin{equation}
+  n^hR_{m,d}(h)
+  \le
+  \left(
+    \frac{nm}{2^{\lfloor(3m-1)/4\rfloor}}
+  \right)^h.
+  \label{eq:three-quarter-charge-v3}
+\end{equation}
+
+Index the four endpoint sizes by $i,j\in\{0,1,2,3\}$, and let $m_{ij}$ be the
+smaller endpoint size for type $(i,j)$.  Put
+\[
+  \rho_{ij}
+  :=
+  \frac{n m_{ij}}{2^{\lfloor(3m_{ij}-1)/4\rfloor}},
+  \qquad
+  \rho_{16}:=\sum_{i,j=0}^{3}\rho_{ij}.
+\]
+Every local base is at most $\rho_{16}$.
+
+\begin{lemma}[Coarse local deficit sum]
+\label{lem:coarse-local-deficit-sum-v3}
+Suppose $\rho_{16}\le1$.  Then, for every selected cell $e$,
+\[
+  \sum_{h\in A_e}n^hR_{m_e,d_e}(h)
+  \le
+  (\alpha+1)\rho_{16}.
+\]
+\end{lemma}
+
+\begin{proof}
+By \eqref{eq:three-quarter-charge-v3}, each summand is at most
+$\rho_{ij}^h$, where $(i,j)$ is the endpoint type of $e$.  Since
+$\rho_{ij}\le\rho_{16}\le1$ and $h\ge1$, one has
+$\rho_{ij}^h\le\rho_{16}$.  The deficit parameter belongs to a set of at most
+$\alpha+1$ integers, so summing gives the stated bound.
+\end{proof}
+
+\begin{proposition}[Fixed-support all-deficit bound]
+\label{prop:fixed-support-all-deficit-v3}
+If $\rho_{16}\le1$, then
+\begin{equation}
+  \sum_{h:\,m-h\text{ high}}w(P,m-h)
+  \le
+  w_{\mathrm{full}}(P)
+  \left(1+(\alpha+1)\rho_{16}\right)^{|P|}.
+  \label{eq:fixed-support-all-deficit-v3}
+\end{equation}
+\end{proposition}
+
+\begin{proof}
+Combine Lemma~\ref{lem:aggregate-deficit-comparison-v3}, the harmless
+enlargement to $A_e$, Lemma~\ref{lem:optional-choice-product-v3}, and
+Lemma~\ref{lem:coarse-local-deficit-sum-v3}.
+\end{proof}
+
+The projection of a block matching onto its row endpoint is injective.  If
+$K=\sum_{i=0}^{3}k_i$ is the total number of row block slots, then
+\begin{equation}
+  |P|\le K.
+  \label{eq:support-cardinality-v3}
+\end{equation}
+
+\subsection{Exact reference grouping}
+
+For a realized endpoint table $L$, let $W(L)$ be the total zero-deficit
+reference weight obtained by summing all full physical decorations of every
+block support with endpoint table $L$.  A realized table belongs to the finite
+image of the block-support space; it is not an arbitrary natural-valued
+$4\times4$ table.
+
+\begin{proposition}[Reference grouping]
+\label{prop:reference-grouping-v3}
+The full-support references satisfy
+\begin{equation}
+  \sum_P w_{\mathrm{full}}(P)
+  =
+  \sum_{L\ \mathrm{realized}}W(L).
+  \label{eq:reference-grouping-v3}
+\end{equation}
+More generally, for every nonnegative endpoint-table function $F$,
+\begin{equation}
+  \sum_P w_{\mathrm{full}}(P)F(L(P))
+  =
+  \sum_{L\ \mathrm{realized}}W(L)F(L).
+  \label{eq:weighted-reference-grouping-v3}
+\end{equation}
+\end{proposition}
+
+\begin{proof}
+Expand the full-support reference as a finite sum over its physical
+decorations.  The disjoint union of all decorated supports is canonically
+equivalent to the dependent sum over realized endpoint tables and their
+decorated-support fibers.  This equivalence preserves both the reference atom
+and the endpoint table.  Transport the finite sum through the equivalence.  The
+factor $F(L)$ is constant on each table fiber and may be pulled outside its
+inner sum; the remaining inner sum is, by definition, $W(L)$.  Taking
+$F\equiv1$ gives \eqref{eq:reference-grouping-v3}.
+\end{proof}
+
+Combining Proposition~\ref{prop:fixed-support-all-deficit-v3},
+\eqref{eq:support-cardinality-v3}, and
+\eqref{eq:reference-grouping-v3} yields
+\begin{equation}
+  \sum_{\text{high skeletons}}w_{\mathrm{hi}}
+  \le
+  \left(\sum_{L\ \mathrm{realized}}W(L)\right)
+  \left(1+(\alpha+1)\rho_{16}\right)^K.
+  \label{eq:coarse-realized-table-reduction-v3}
+\end{equation}
+
+\begin{remark}[Sharper table-preserving route]
+If every $\rho_{ij}\le1/2$, then
+$\sum_{h\ge1}\rho_{ij}^h\le2\rho_{ij}$.  Applying
+\eqref{eq:weighted-reference-grouping-v3} with
+$F(L)=\prod_{i,j}(1+2\rho_{ij})^{L_{ij}}$ gives
+\[
+  \sum_{\text{high skeletons}}w_{\mathrm{hi}}
+  \le
+  \sum_{L\ \mathrm{realized}}
+    W(L)\prod_{i,j}(1+2\rho_{ij})^{L_{ij}}.
+\]
+The main proof uses \eqref{eq:coarse-realized-table-reduction-v3}: its single
+hypothesis $\rho_{16}\le1$ is sufficient and matches the canonical finite Lean
+reduction.
+\end{remark}
+
+\subsection{Endpoint transport}
+
+Write the four endpoint sizes as
+\[
+  u_i=a-i,
+  \qquad 0\le i\le3,
+  \qquad a=\alpha-2.
+\]
+For a full-containment table $L=(\ell_{ij})$, put
+\[
+  r_i=\sum_j\ell_{ij},
+  \qquad
+  c_j=\sum_i\ell_{ij},
+  \qquad
+  x_{ij}=\min\{u_i,u_j\},
+  \qquad
+  J(L)=\sum_{i,j}x_{ij}\ell_{ij}.
+\]
+Its exact reference weight is
+\begin{equation}
+  W(L)=
+  \frac{\prod_i(k_i)_{r_i}\prod_j(k_j)_{c_j}}
+       {\prod_{i,j}\ell_{ij}!}
+  \frac1{(n)_{J(L)}}
+  \prod_{i,j}
+  \left[
+    \frac{(u_i)_{x_{ij}}(u_j)_{x_{ij}}}{x_{ij}!}g(x_{ij})
+  \right]^{\ell_{ij}}.
+  \label{eq:endpoint-reference-weight-v3}
+\end{equation}
+For a one-sided margin vector $r$, define
+\begin{equation}
+  D(r)=
+  \frac{\prod_i(k_i)_{r_i}^2}{\prod_i r_i!}
+  \frac{\prod_i[u_i!g(u_i)]^{r_i}}{(n)_{m_r}},
+  \qquad
+  m_r=\sum_i u_ir_i.
+  \label{eq:one-sided-diagonal-weight-v3}
+\end{equation}
+This is the partial-diagonal weight of Section~7.
+
+For endpoint types whose sizes differ by $d$, define
+\[
+  Q_{ij}:=
+  (n+1)^{d/2}
+  \frac{\sqrt{(t)_d}}{d!}
+  2^{-\{ds+\binom d2\}/2},
+  \qquad t=s+d,
+\]
+and set $Q_{ii}=1$.  Uniformly over the four endpoint types,
+\begin{equation}
+  Q_{ij}\le\frac{\eta_n^d}{d!},
+  \qquad
+  \eta_n=
+  2^{3/2}\sqrt{\frac{(n+1)a}{2^a}}
+  =O\!\left(\frac{(\log n)^{3/2}}{\sqrt n}\right).
+  \label{eq:endpoint-eta-v3}
+\end{equation}
+
+Let
+\[
+  A_L=\frac{\prod_i r_i!}{\prod_{i,j}\ell_{ij}!},
+  \qquad
+  C_L=\frac{\prod_j c_j!}{\prod_{i,j}\ell_{ij}!},
+  \qquad
+  Q^L=\prod_{i,j}Q_{ij}^{\ell_{ij}}.
+\]
+The exact falling-factorial transport and local endpoint identities give the
+square-free comparison
+\begin{equation}
+  W(L)^2
+  \le
+  \bigl(D(r)A_LQ^L\bigr)\bigl(D(c)C_LQ^L\bigr).
+  \label{eq:square-free-endpoint-transport-v3}
+\end{equation}
+
+\begin{proposition}[Endpoint-table sum]
+\label{prop:endpoint-table-sum-v3}
+Uniformly in the phase,
+\begin{equation}
+  \sum_LW(L)
+  \le
+  \exp\!\left\{O(\eta_nK)\right\}
+  \sum_rD(r)
+  \le
+  \exp\!\left\{O(\sqrt{n\log n})\right\}.
+  \label{eq:endpoint-table-sum-v3}
+\end{equation}
+The sum on the left may be taken over all feasible endpoint tables; enlarging
+from realized tables is harmless.
+\end{proposition}
+
+\begin{proof}
+By the arithmetic--geometric mean inequality and
+\eqref{eq:square-free-endpoint-transport-v3},
+\[
+  2W(L)
+  \le
+  D(r)A_LQ^L+D(c)C_LQ^L.
+\]
+Sum the first term over all tables.  For fixed row margin $r$, discard the
+column-margin constraints.  Since all terms are nonnegative, this enlarges the
+sum.  The multinomial theorem gives
+\[
+  \sum_{L:\,\operatorname{row}(L)=r}A_LQ^L
+  \le
+  \prod_i\left(\sum_jQ_{ij}\right)^{r_i}
+  \le
+  (1+C\eta_n)^K.
+\]
+Thus the first half is at most
+$(1+C\eta_n)^K\sum_rD(r)$.  The second half is identical after exchanging
+rows and columns.  Section~7 proves $\sum_rD(r)=1+o(1)$ uniformly in the
+phase.  Finally, $K=\Theta(n/\log n)$ and
+\eqref{eq:endpoint-eta-v3} give
+$\eta_nK=O(\sqrt{n\log n})$.
+\end{proof}
+
+\subsection{Phase smallness of the common charge}
+
+The phase satisfies
+\[
+  \alpha
+  =
+  \left(\frac{2}{\log 2}+o(1)\right)\log n.
+\]
+For all sufficiently large $n$,
+\begin{equation}
+  \frac52\log n\le\alpha.
+  \label{eq:coarse-phase-corridor-v3}
+\end{equation}
+Every endpoint minimum satisfies $m_{ij}\ge\alpha-5$, and elementary floor
+arithmetic gives
+\[
+  3\alpha-19
+  \le
+  4\left\lfloor\frac{3m_{ij}-1}{4}\right\rfloor.
+\]
+Using $\log 2>2/3$ and \eqref{eq:coarse-phase-corridor-v3},
+\begin{equation}
+  \frac54\log n-\frac{19}{6}
+  \le
+  (\log 2)
+  \left\lfloor\frac{3m_{ij}-1}{4}\right\rfloor.
+  \label{eq:coarse-log-budget-v3}
+\end{equation}
+Exponentiation yields
+\[
+  2^{\lfloor(3m_{ij}-1)/4\rfloor}
+  \ge
+  e^{-19/6}n^{5/4}.
+\]
+Since $m_{ij}=O(\log n)$,
+\begin{equation}
+  \rho_{16}
+  =O\!\left(\frac{\log n}{n^{1/4}}\right)
+  \longrightarrow0.
+  \label{eq:rho-sixteen-small-v3}
+\end{equation}
+In particular, $\rho_{16}\le1$ for all sufficiently large $n$.
+
+Moreover,
+\[
+  \log\left(1+(\alpha+1)\rho_{16}\right)^K
+  \le
+  K(\alpha+1)\rho_{16}
+  =O(n^{3/4}\log n)
+  =o\!\left(\frac{n}{(\log n)^4}\right).
+\]
+Combining this estimate, \eqref{eq:coarse-realized-table-reduction-v3}, and
+Proposition~\ref{prop:endpoint-table-sum-v3} proves the required estimate.
+
+\begin{proposition}[Bare high-skeleton estimate]
+\label{prop:bare-high-skeleton-v3}
+There is a deterministic sequence $\varepsilon_n\to0$ such that
+\begin{equation}
+  \operatorname{BareSkeletonSum}_n
+  \le
+  \exp\!\left\{
+    \varepsilon_n\frac{n}{(\log n)^4}
+  \right\}.
+  \label{eq:bare-skeleton-final-v3}
+\end{equation}
+\end{proposition}
+
+No residual local factor or binary cycle-space factor has been charged in this
+section.  Those factors are treated in Section~9.
diff --git a/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex b/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex
new file mode 100644
index 0000000..c99c27b
--- /dev/null
+++ b/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex
@@ -0,0 +1,325 @@
+\section{Residual attachments by matching restriction}
+\label{sec:residual-attachments-v3}
+
+Section~8 bounded the sum of the bare high-skeleton weights. It deliberately
+did not charge the local rewards of unexposed cells or the binary cycle-space
+factor of the residual support. We now condition on one feasible canonical
+high skeleton and bound exactly these remaining factors.
+
+\subsection{Exact conditional decomposition}
+
+Fix a canonical high skeleton with exposed block matching $M$, exposed
+multiplicities $j$, and total exposed mass $J$. Put
+\[
+  m_0:=n-J.
+\]
+Let $(d_a)_a$ and $(d'_b)_b$ be the residual row and column degrees. Both degree
+sums equal $m_0$, and every degree is at most the phase cap $U$.
+
+The unexposed pairs form a uniform bipartite configuration matching with these
+residual degrees. Let $r'_{ab}$ be its cell counts and let
+$H_{\mathrm{res}}$ be the simple support graph of cells with
+$r'_{ab}\ge2$. The residual event imposes the cap
+$r'_{ab}\le\lfloor U/2\rfloor$ and forbids any further pair in a cell of $M$.
+Define
+\begin{equation}
+  \mathcal A(M,j)
+  :=
+  \mathbb E_{\mathrm{res}}\!\left[
+    \left(\prod_{a,b}g(r'_{ab})\right)
+    2^{\beta(M\cup H_{\mathrm{res}})}
+    \mathbf 1_{\mathcal E(M,j)}
+  \right].
+  \label{eq:residual-attachment-v3}
+\end{equation}
+The expectation is only over the residual configuration matching.
+
+The exact overlap decomposition gives
+\begin{equation}
+  \frac{\mathbb E Z^2}{(\mathbb E Z)^2}
+  =
+  \sum_{(M,j)}w_{\mathrm{hi}}(M,j)\,\mathcal A(M,j),
+  \label{eq:exact-attachment-decomposition-v3}
+\end{equation}
+where the sum is over the finite family of feasible canonical high skeletons.
+Thus Proposition~\ref{prop:bare-high-skeleton-v3} reduces the second moment to
+a uniform estimate for $\mathcal A(M,j)$.
+
+\subsection{Local threshold activities}
+
+For a residual cell $(a,b)$ outside $M$, put
+\begin{equation}
+  \theta_{ab}:=
+  \frac{\mathrm e\,d_ad'_b}{m_0}.
+  \label{eq:theta-v3}
+\end{equation}
+Let
+\[
+  \Delta_x:=g(x)-g(x-1),
+  \qquad
+  R:=\left\lfloor\frac U2\right\rfloor,
+\]
+and define
+\begin{equation}
+  \lambda_{ab}
+  :=
+  \sum_{x=3}^{R}\Delta_x\frac{\theta_{ab}^x}{x!},
+  \qquad
+  q_{ab}
+  :=
+  \frac{\theta_{ab}^2}{2}+\lambda_{ab}.
+  \label{eq:lambda-q-v3}
+\end{equation}
+On the exposed matching $M$, set $\lambda_{ab}=q_{ab}=0$.
+
+The local reward has the threshold expansion
+\[
+  g(r)=1+\sum_{x=3}^{R}\Delta_x\mathbf 1_{\{r\ge x\}}
+  \qquad(0\le r\le R).
+\]
+If a residual cell is selected in an even edge set, the base threshold two is
+used once and a higher threshold replaces, rather than duplicates, that base
+demand. Applying the joint prescribed-cell configuration bound to every
+threshold demand in the finite expansion gives the following exact finite
+interface.
+
+\begin{lemma}[Fixed even-set expansion]
+\label{lem:fixed-even-set-expansion-v3}
+For every residual edge set $F$,
+\[
+  \mathbb E_{\mathrm{res}}[
+    \text{capped local reward with the thresholds of }F]
+  \le
+  \prod_{a,b}
+  \begin{cases}
+    1,&(a,b)\in M,\\
+    q_{ab},&(a,b)\in F\setminus M,\\
+    1+\lambda_{ab},&(a,b)\notin F\cup M.
+  \end{cases}
+\]
+\end{lemma}
+
+\begin{proof}
+Expand every capped local factor into its nonnegative threshold alternatives.
+For a cell in $F\setminus M$, use either the threshold-two term or one higher
+increment term, but not both in the same monomial. Apply the joint
+configuration-model prescribed-cell estimate once to the complete demand of
+each monomial. The threshold-two contribution is
+$\theta_{ab}^2/2$, the higher-threshold contributions sum to
+$\lambda_{ab}$, and cells outside $F\cup M$ contribute
+$1+\lambda_{ab}$. Dropping the cap and no-return indicator only enlarges the
+nonnegative sum.
+\end{proof}
+
+Summing the preceding bound over the binary cycle space yields
+\begin{equation}
+  \mathcal A(M,j)
+  \le
+  \left(\prod_{a,b}(1+\lambda_{ab})\right)
+  \sum_{F\ \mathrm{even}}
+    \prod_{e\in F\setminus M}q_e.
+  \label{eq:lambda-even-factorization-v3}
+\end{equation}
+
+\subsection{Restriction outside the exposed matching}
+
+The following lemma is independent of the random-graph application.
+
+\begin{lemma}[Restriction-product bound]
+\label{lem:restriction-product-v3}
+Let $E$ be a finite set, let $\mathcal C$ be a finite family of subsets of
+$E$, and let $I\subseteq E$. Suppose that the map
+\[
+  A\longmapsto A\setminus I
+\]
+is injective on $\mathcal C$. For nonnegative activities $(q_e)_{e\in E}$,
+\[
+  \sum_{A\in\mathcal C}
+    \prod_{e\in A\setminus I}q_e
+  \le
+  \prod_{e\in E\setminus I}(1+q_e).
+\]
+\end{lemma}
+
+\begin{proof}
+The restrictions $A\setminus I$ form a subfamily of the power set of
+$E\setminus I$ and occur without repetition. Enlarge the sum to the full power
+set and apply the finite product identity
+\[
+  \sum_{B\subseteq E\setminus I}\prod_{e\in B}q_e
+  =
+  \prod_{e\in E\setminus I}(1+q_e).
+\]
+\end{proof}
+
+Apply the lemma to the even edge sets of $M\cup H_{\mathrm{res}}$ and to
+$I=M$. The required injectivity is elementary. If two even sets have the same
+restriction outside $M$, their symmetric difference is an even subset of the
+matching $M$. A nonempty subset of a matching has a vertex of degree one, so
+that symmetric difference must be empty. Therefore
+\begin{equation}
+  \sum_{F\ \mathrm{even}}
+    \prod_{e\in F\setminus M}q_e
+  \le
+  \prod_{e\notin M}(1+q_e).
+  \label{eq:even-family-product-v3}
+\end{equation}
+
+Since $0\le\lambda_{ab}\le q_{ab}$ pointwise, equations
+\eqref{eq:lambda-even-factorization-v3} and
+\eqref{eq:even-family-product-v3}, together with $1+x\le e^x$, give
+\begin{equation}
+  \mathcal A(M,j)
+  \le
+  \exp\!\left(2\sum_{a,b}q_{ab}\right).
+  \label{eq:q-only-attachment-v3}
+\end{equation}
+Thus the local rewards and the cycle-space factor are controlled by one total
+activity.
+
+\subsection{The intrinsic residual regime}
+
+Assume
+\begin{equation}
+  2^U\le m_0^3.
+  \label{eq:intrinsic-residual-regime-v3}
+\end{equation}
+The sequence of majorants
+\[
+  g(x)\frac{\theta^x}{x!},
+  \qquad 3\le x\le R,
+\]
+has consecutive ratio $2^x\theta/(x+1)$ up to the harmless initial values of
+$g$. The ratio increases with $x$. Its decreasing part is bounded by the first
+term, its transition contains only a bounded number of terms, and its
+increasing part is bounded by the endpoint. Under
+\eqref{eq:intrinsic-residual-regime-v3} and the degree cap, the endpoint is
+exponentially smaller than the quadratic term. Consequently there is an
+absolute $C_0$ such that
+\begin{equation}
+  q_{ab}\le C_0\theta_{ab}^2
+  \label{eq:q-quadratic-v3}
+\end{equation}
+uniformly in every residual cell.
+
+The exact second-moment identity for the cell intensities is
+\[
+  \sum_{a,b}\theta_{ab}^2
+  =
+  \frac{\mathrm e^2}{m_0^2}
+  \left(\sum_a d_a^2\right)
+  \left(\sum_b(d'_b)^2\right).
+\]
+Since every degree is at most $U$ and both degree sums equal $m_0$,
+\[
+  \sum_a d_a^2\le Um_0,
+  \qquad
+  \sum_b(d'_b)^2\le Um_0.
+\]
+Together with \eqref{eq:q-quadratic-v3}, this yields
+\begin{equation}
+  \sum_{a,b}q_{ab}\le C_1U^2.
+  \label{eq:total-q-v3}
+\end{equation}
+Equation \eqref{eq:q-only-attachment-v3} now gives
+\begin{equation}
+  \mathcal A(M,j)\le\exp(CU^2)
+  \qquad\text{if }2^U\le m_0^3.
+  \label{eq:intrinsic-attachment-v3}
+\end{equation}
+
+\subsection{The complementary residual regime}
+
+If \eqref{eq:intrinsic-residual-regime-v3} fails, then
+\begin{equation}
+  m_0<2^{\lceil U/3\rceil}.
+  \label{eq:small-residual-mass-v3}
+\end{equation}
+Indeed, $m_0\ge2^{\lceil U/3\rceil}$ would imply
+$m_0^3\ge2^U$.
+
+In this regime, discard all residual restrictions. The local rewards satisfy
+\[
+  \sum_{a,b}\binom{r'_{ab}}2
+  \le
+  \frac{U-1}{2}m_0,
+\]
+while the cycle rank of the residual support together with the exposed
+matching is at most $m_0/2$. Hence
+\begin{equation}
+  \mathcal A(M,j)
+  \le
+  2^{Um_0/2}
+  \qquad\text{if }2^U>m_0^3.
+  \label{eq:complementary-attachment-v3}
+\end{equation}
+
+\begin{proposition}[Uniform residual attachment]
+\label{prop:uniform-residual-attachment-v3}
+There is an absolute constant $C$ such that, for every feasible canonical high
+skeleton,
+\[
+  \mathcal A(M,j)
+  \le
+  \begin{cases}
+    \exp(CU^2),&2^U\le m_0^3,\\
+    2^{Um_0/2},&2^U>m_0^3.
+  \end{cases}
+\]
+\end{proposition}
+
+The phase satisfies $U=O(\log n)$ and
+\[
+  2^U=\Theta\!\left(\frac{n^2}{(\log n)^2}\right).
+\]
+In the first regime, $CU^2=O((\log n)^2)$. In the second,
+\eqref{eq:small-residual-mass-v3} gives
+\[
+  Um_0
+  =
+  O\!\left(n^{2/3}(\log n)^{1/3}\right).
+\]
+Both quantities are $o(n/(\log n)^4)$ uniformly in the high skeleton.
+Therefore there is a deterministic sequence $\eta_n\to0$ such that
+\begin{equation}
+  \mathcal A(M,j)
+  \le
+  \exp\!\left\{
+    \eta_n\frac{n}{(\log n)^4}
+  \right\}
+  \label{eq:uniform-attachment-error-v3}
+\end{equation}
+for every feasible skeleton.
+
+\begin{proposition}[Normalized signed second moment]
+\label{prop:normalized-second-moment-v3}
+There is a deterministic sequence $\Lambda_n$ satisfying
+\[
+  \Lambda_n=o\!\left(\frac{n}{(\log n)^4}\right)
+\]
+such that
+\begin{equation}
+  1
+  \le
+  \frac{\mathbb E Z^2}{(\mathbb E Z)^2}
+  \le
+  e^{\Lambda_n}.
+  \label{eq:normalized-second-moment-v3}
+\end{equation}
+\end{proposition}
+
+\begin{proof}
+Insert \eqref{eq:uniform-attachment-error-v3} into the exact decomposition
+\eqref{eq:exact-attachment-decomposition-v3} and factor out the uniform
+attachment bound. Proposition~\ref{prop:bare-high-skeleton-v3} bounds the
+remaining sum. The lower bound is the nonnegativity of the variance.
+\end{proof}
+
+Paley--Zygmund now gives
+\[
+  \mathbb P(Z>0)
+  \ge
+  \frac{(\mathbb E Z)^2}{\mathbb E Z^2}
+  \ge e^{-\Lambda_n}.
+\]
+This is the rare seed amplified in Section~10.
diff --git a/625/audits/SELF_CONTAINED_BULLETPROOF_MANUSCRIPT_PASS_2026-08-04.md b/625/audits/SELF_CONTAINED_BULLETPROOF_MANUSCRIPT_PASS_2026-08-04.md
new file mode 100644
index 0000000..4b03962
--- /dev/null
+++ b/625/audits/SELF_CONTAINED_BULLETPROOF_MANUSCRIPT_PASS_2026-08-04.md
@@ -0,0 +1,224 @@
+# Erdős 625: self-contained manuscript and formalization pass
+
+**Date:** 4 August 2026  
+**Base:** public PR #56, `agent/625-ams-manuscript-clarity`  
+**Branch:** `agent/625-self-contained-bulletproof-manuscript`
+
+## 1. Objective
+
+The 13-page AMS draft in PR #56 is a polished proof synopsis, not a
+self-contained paper. This pass turns it into a complete generated manuscript
+that includes the canonical proofs of Sections 1--7 and 10, replaces Sections
+8--9 by the shorter audited route, supplies a new final constant ledger, and
+places the exact formalization status inside the PDF.
+
+The editorial standard is reader-first mathematical exposition:
+
+- every standard invariant is defined before use;
+- every manuscript-specific proof object is distinguished from the standard
+  graph-theoretic objects;
+- finite identities, deterministic inequalities, asymptotic estimates, and
+  probability conclusions are separated;
+- no sentence substitutes for a load-bearing theorem;
+- no private or public CI status is used as a proxy for a mathematical proof;
+- the theorem status is visible in the PDF, not only in pull-request metadata.
+
+## 2. Self-contained assembly
+
+`625/scripts/build_self_contained_ams_v3.py` checks the exact Git-blob SHA of
+`625/arxiv/main.tex`, extracts the complete canonical Sections 1--7 and 10 by
+semantic section markers, converts the legacy ruled statement boxes to the
+ordinary `amsthm` hierarchy, normalizes notation and mathematical English, and
+inserts the audited replacement Sections 8, 9, and 11.
+
+The generated manuscript therefore contains the full argument rather than only
+an introduction, roadmap, and the two difficult replacement sections.
+
+The generator fails closed if the canonical source changes. This prevents
+line-number drift or a silent mixture of two different mathematical versions.
+
+## 3. Status-safe front matter
+
+The master TeX defines a compile-time switch:
+
+```tex
+\newif\ifErdosProofClosed
+\ErdosProofClosedfalse
+```
+
+The default verification mode:
+
+- prints an explicit status banner;
+- states the target theorem conditionally on the remaining formal gates;
+- uses an audit-safe abstract;
+- keeps the publication switch disabled.
+
+The publication mode may be enabled only after the checklist in Appendix A is
+green on one integrated commit and has received independent mathematical
+review.
+
+## 4. Canonical Section VIII route
+
+The former draft mixed two valid but different finite routes.
+
+The sharp route assumes every local endpoint base is at most `1/2` and retains
+
+```text
+product_(i,j) (1 + 2 rho_ij)^(L_ij).
+```
+
+The coarse route defines the sum of the sixteen endpoint bases
+
+```text
+rho_16 = sum_(i,j) rho_ij
+```
+
+and needs only `rho_16 <= 1`, giving
+
+```text
+(1 + (alpha+1) rho_16)^K.
+```
+
+The main manuscript now uses the coarse route because it is the cleanest route
+consumed by the private finite reduction. The sharp weighted regrouping is
+stated separately as a stronger reusable result.
+
+The new Section VIII contains complete statements and proofs of:
+
+1. the completion-free aggregate high-skeleton weight;
+2. the exact one-cell deficit ratio;
+3. the one-global-denominator comparison;
+4. the finite optional-choice product;
+5. the coarse common-charge deficit sum;
+6. exact unweighted and weighted reference regrouping;
+7. square-free endpoint transport and multinomial summation;
+8. the coarse phase corridor and the bound
+   `rho_16 = O(log n / n^(1/4))`;
+9. the final bare-skeleton estimate.
+
+The sentence “endpoint transportation absorbs the remaining product” has been
+removed. The endpoint transportation is now a named proposition with its
+formulas and proof.
+
+## 5. Self-contained Section IX
+
+The replacement residual section now defines, rather than merely names,
+
+```text
+theta_ab
+Delta_x
+lambda_ab
+q_ab
+```
+
+and proves the following sequence:
+
+1. the exact conditional attachment decomposition;
+2. the fixed-even-set threshold expansion;
+3. injectivity of deletion outside the exposed matching;
+4. the restriction-product bound;
+5. pointwise `lambda_ab <= q_ab`;
+6. the q-only envelope `A(M,j) <= exp(2 sum q_ab)`;
+7. the intrinsic total-q estimate at scale `U^2`;
+8. the complementary deterministic residual-size estimate;
+9. the uniform attachment error;
+10. the normalized signed second moment.
+
+The legacy simple-cycle, walk-kernel, mixed-cycle, and `tau` calculations are
+not part of the main exposition.
+
+## 6. Constant ledger
+
+The final section derives the phase-resolved coefficient before inserting a
+fixed certificate:
+
+```text
+(log 2)^2/8 * (log 2 - D_4(delta_n)).
+```
+
+It then records the exact rational four-support certificate
+
+```text
+D_4(delta) < log(639/500),
+log 2 - D_4(delta) > log(1000/639),
+```
+
+and obtains the fixed coefficient
+
+```text
+(log 2)^2/8 * log(1000/639)
+  = 0.026896409808379...
+```
+
+The midpoint factor is justified directly: the root separation has coefficient
+`/4`, midpoint placement retains one half, and all integer and amplification
+corrections are lower order. No additional fixed halving is inserted.
+
+## 7. Formalization appendix
+
+Appendix A maps the paper-level results to exact private Lean declarations and
+uses four explicit statuses: `welded`, `running`, `needs review`, and
+`blocked`.
+
+As of 4 August 2026:
+
+- the Section VIII finite chain through the realized-table deficit sum is
+  welded privately;
+- the coarse phase corridor is welded;
+- the exact common-charge theorem
+  `eventually_fourEndpointThreeQuarterRho_le_one` has one approved, running
+  Aristotle request and is not yet proof evidence;
+- concrete phase inputs/chromatic tail, the four-size first-moment assembly,
+  the complete partial-diagonal asymptotics, and the global final attachment
+  assembly remain unclosed.
+
+The appendix forbids enabling publication mode before those gates close.
+
+## 8. Lean project recommendations
+
+The current root imports hundreds of fine-grained modules, including legacy and
+simplified routes. For publication, create a curated theorem-facing hierarchy:
+
+```text
+Erdos625/Paper/Phase.lean
+Erdos625/Paper/FirstMoment.lean
+Erdos625/Paper/PartialDiagonals.lean
+Erdos625/Paper/HighSkeletons.lean
+Erdos625/Paper/Attachments.lean
+Erdos625/Paper/Amplification.lean
+Erdos625/Paper/Main.lean
+```
+
+Keep an exhaustive internal root for historical development, but remove the
+legacy cycle/walk route from the paper-facing dependency chain.
+
+The remaining broad DAG nodes should be split before proof search. In
+particular, partial diagonals should become:
+
+```text
+empty-corner estimate
+central-rate negativity
+full-corner asymptotic wrapper
+partial-diagonal assembly
+```
+
+A machine-readable paper--Lean manifest should generate the formalization table
+and axiom report automatically.
+
+## 9. Validation contract
+
+The dedicated workflow must:
+
+- generate the body from the frozen canonical source;
+- run the structural checker under ordinary and optimized Python;
+- compile the complete AMS manuscript with BibTeX;
+- reject unresolved references and citations;
+- reject missing status markers, undefined proof-object notation, and the old
+  synopsis-only transition sentences;
+- require all numbered Sections 1--11 and Appendix A;
+- require a substantial page and word count consistent with a full paper;
+- upload the generated PDF and generated body as review artifacts.
+
+A successful build validates the TeX assembly and editorial invariants. It is
+not evidence that the remaining Lean or mathematical proof obligations have
+closed.
diff --git a/625/experiments/check_self_contained_manuscript_v3.py b/625/experiments/check_self_contained_manuscript_v3.py
new file mode 100644
index 0000000..e500086
--- /dev/null
+++ b/625/experiments/check_self_contained_manuscript_v3.py
@@ -0,0 +1,210 @@
+#!/usr/bin/env python3
+"""Fail-closed structural checks for the Erdős 625 Version 3 manuscript."""
+
+from __future__ import annotations
+
+import re
+import subprocess
+from collections import Counter
+from pathlib import Path
+
+
+ROOT = Path(__file__).resolve().parents[1]
+ARXIV = ROOT / "arxiv"
+GENERATOR = ROOT / "scripts" / "build_self_contained_ams_v3.py"
+GENERATED = ARXIV / "AMS_SELF_CONTAINED_BODY_V3.generated.tex"
+MASTER = ARXIV / "AMS_SELF_CONTAINED_DRAFT_V3.tex"
+
+SOURCE_FILES = [
+    ARXIV / "FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex",
+    ARXIV / "CONVENTIONS_AND_PROOF_OBJECTS_V3.tex",
+    ARXIV / "PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex",
+    ARXIV / "SECTION8_SELF_CONTAINED_V3.tex",
+    ARXIV / "SECTION9_SELF_CONTAINED_V3.tex",
+    ARXIV / "FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex",
+    ARXIV / "FORMALIZATION_STATUS_APPENDIX_V3.tex",
+]
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise RuntimeError(message)
+
+
+def flatten(text: str) -> str:
+    """Normalize TeX source whitespace without changing control sequences."""
+    return re.sub(r"\s+", " ", text)
+
+
+def strip_tex(text: str) -> str:
+    text = re.sub(r"%.*", " ", text)
+    text = re.sub(r"\\[A-Za-z@]+\*?(?:\[[^]]*\])?", " ", text)
+    text = text.replace("{", " ").replace("}", " ")
+    text = re.sub(r"\$[^$]*\$", " ", text)
+    return re.sub(r"\s+", " ", text)
+
+
+def check_balanced_environments(text: str, name: str) -> None:
+    begins = Counter(re.findall(r"\\begin\{([^}]+)\}", text))
+    ends = Counter(re.findall(r"\\end\{([^}]+)\}", text))
+    require(
+        begins == ends,
+        f"{name}: unbalanced environments: {begins - ends}, {ends - begins}",
+    )
+
+
+def main() -> None:
+    for path in [MASTER, GENERATOR, *SOURCE_FILES]:
+        require(path.is_file(), f"missing file: {path}")
+
+    subprocess.run(["python", str(GENERATOR)], cwd=ROOT.parent, check=True)
+    require(GENERATED.is_file(), "generator did not create the manuscript body")
+
+    master = MASTER.read_text(encoding="utf-8")
+    generated = GENERATED.read_text(encoding="utf-8")
+    sources = {path.name: path.read_text(encoding="utf-8") for path in SOURCE_FILES}
+    combined = "\n".join([master, generated, *sources.values()])
+
+    require(r"\ErdosProofClosedfalse" in master, "publication switch is not fail-closed")
+    require(r"\ErdosProofClosedtrue" not in master, "publication mode was enabled")
+    require(
+        "Verification draft"
+        in sources["FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex"],
+        "visible verification status is missing",
+    )
+
+    required_master_inputs = (
+        "AMS_THEOREM_ENVIRONMENTS_V3",
+        "FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3",
+        "CONVENTIONS_AND_PROOF_OBJECTS_V3",
+        "PROOF_ARCHITECTURE_SELF_CONTAINED_V3",
+        "AMS_SELF_CONTAINED_BODY_V3.generated",
+        "FORMALIZATION_STATUS_APPENDIX_V3",
+    )
+    missing_inputs = [token for token in required_master_inputs if token not in master]
+    require(not missing_inputs, f"master file missing inputs: {missing_inputs}")
+
+    required_body_markers = (
+        r"\section{Phase notation and elementary estimates}",
+        r"\input{SECTION8_SELF_CONTAINED_V3}",
+        r"\input{SECTION9_SELF_CONTAINED_V3}",
+        r"\section{Rare-event amplification}",
+        r"\input{FINAL_ASSEMBLY_SELF_CONTAINED_V3}",
+        "Canonical source Git blob: c4d090b73cd5efcdb98cc30f79bb5f53c6c9bc97",
+    )
+    missing_body = [token for token in required_body_markers if token not in generated]
+    require(not missing_body, f"generated body missing markers: {missing_body}")
+    require(
+        generated.count(r"\section{") >= 8,
+        "generated body does not contain the canonical numbered sections",
+    )
+    # The frozen source contributes 1,915 generated lines after the deliberate
+    # removal of the old Sections 8, 9, and 11.  The replacement sections are
+    # separate audited inputs, so this gate checks against that exact source
+    # volume rather than an arbitrary journal-length target.
+    require(
+        len(generated.splitlines()) >= 1800,
+        f"generated body is unexpectedly short: {len(generated.splitlines())} lines",
+    )
+
+    section8 = sources["SECTION8_SELF_CONTAINED_V3.tex"]
+    section8_flat = flatten(section8)
+    for token in (
+        "Completion-free aggregate weight",
+        "Exact one-cell deficit ratio",
+        "Aggregate deficit comparison",
+        "Optional-choice product",
+        "Reference grouping",
+        "Endpoint-table sum",
+        "Phase smallness of the common charge",
+        r"\rho_{16}",
+        "canonical finite Lean reduction",
+    ):
+        require(token in section8_flat, f"Section 8 missing: {token}")
+
+    section9 = sources["SECTION9_SELF_CONTAINED_V3.tex"]
+    section9_flat = flatten(section9)
+    for token in (
+        r"\theta_{ab}",
+        r"\lambda_{ab}",
+        r"q_{ab}",
+        "Fixed even-set expansion",
+        "Restriction-product bound",
+        "The intrinsic residual regime",
+        "The complementary residual regime",
+        "Normalized signed second moment",
+    ):
+        require(token in section9_flat, f"Section 9 missing: {token}")
+
+    final = sources["FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex"]
+    final_flat = flatten(final)
+    for token in (
+        r"\frac{(\log2)^2}{8}A_4(\delta_n)",
+        r"\log\!\left(\frac{1000}{639}\right)",
+        "Exact four-support certificate",
+        "Simultaneous complement form",
+    ):
+        require(token in final_flat, f"final assembly missing: {token}")
+
+    appendix = sources["FORMALIZATION_STATUS_APPENDIX_V3.tex"]
+    appendix_flat = flatten(appendix)
+    for token in (
+        "Welded",
+        "Running",
+        "Needs review",
+        "eventually_fourEndpointThreeQuarterRho_le_one",
+        "Publication gate",
+        "Recommended theorem-facing Lean organization",
+    ):
+        require(token in appendix_flat, f"formalization appendix missing: {token}")
+
+    forbidden = (
+        "TODO",
+        "TBD",
+        "proof omitted",
+        "details are standard",
+        "The endpoint transportation estimate absorbs",
+        r"\exp\!left",
+        r"\begin{lemmabox}",
+        r"\begin{propositionbox}",
+        r"\begin{resultbox}",
+        r"\ln",
+    )
+    offenders = [token for token in forbidden if token in combined]
+    require(not offenders, f"forbidden manuscript markers: {offenders}")
+
+    labels = re.findall(r"\\label\{([^}]+)\}", combined)
+    label_counts = Counter(labels)
+    # The target theorem is written in two mutually exclusive TeX branches.
+    # Exactly one branch is expanded in any build, so the shared semantic label
+    # is intentional and cannot produce a duplicate in the compiled document.
+    require(
+        label_counts.get("thm:main-v3", 0) == 2,
+        "the two status branches must share exactly one target-theorem label",
+    )
+    duplicates = sorted(
+        label
+        for label, count in label_counts.items()
+        if count > 1 and label != "thm:main-v3"
+    )
+    require(not duplicates, f"duplicate labels: {duplicates}")
+
+    for name, text in {"master": master, "generated": generated, **sources}.items():
+        check_balanced_environments(text, name)
+        require(text.count("{") == text.count("}"), f"{name}: unbalanced braces")
+
+    words = re.findall(r"[A-Za-z][A-Za-z'-]+", strip_tex(combined))
+    require(
+        len(words) >= 5000,
+        f"manuscript prose extraction is unexpectedly short: {len(words)} words",
+    )
+
+    print("ERDOS 625 SELF-CONTAINED MANUSCRIPT CHECK: PASS")
+    print(f"  generated body lines: {len(generated.splitlines())}")
+    print(f"  approximate prose words: {len(words)}")
+    print(f"  unique semantic labels: {len(label_counts)}")
+    print("  publication switch: disabled")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/625/scripts/build_self_contained_ams_v3.py b/625/scripts/build_self_contained_ams_v3.py
new file mode 100644
index 0000000..9a2f944
--- /dev/null
+++ b/625/scripts/build_self_contained_ams_v3.py
@@ -0,0 +1,168 @@
+#!/usr/bin/env python3
+"""Generate the complete AMS Version 3 manuscript body.
+
+The canonical TeX remains frozen while the proof is incomplete. This script
+extracts the complete Sections 1--7 and 10 from that source, normalizes their
+legacy statement environments, and inserts the audited replacement Sections 8,
+9, and 11. The exact canonical Git-blob SHA is checked before line-independent
+section markers are used.
+"""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import re
+from pathlib import Path
+
+
+EXPECTED_CANONICAL_BLOB = "c4d090b73cd5efcdb98cc30f79bb5f53c6c9bc97"
+
+START_SECTION_1 = r"\section{Notation and elementary"
+START_SECTION_8 = r"\section{Canonical high cells and dense endpoint"
+START_SECTION_10 = r"\section{Rare-event amplification}"
+START_SECTION_11 = r"\section{Completion of the proof}"
+
+
+def git_blob_sha(raw: bytes) -> str:
+    header = f"blob {len(raw)}\0".encode("ascii")
+    return hashlib.sha1(header + raw).hexdigest()
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise RuntimeError(message)
+
+
+def slice_between(text: str, start: str, end: str) -> str:
+    begin = text.find(start)
+    finish = text.find(end)
+    require(begin >= 0, f"missing start marker: {start}")
+    require(finish >= 0, f"missing end marker: {end}")
+    require(begin < finish, f"reversed markers: {start!r}, {end!r}")
+    return text[begin:finish]
+
+
+def normalize_legacy_section(text: str) -> str:
+    # Remove navigation-only commands that are redundant in the generated AMS
+    # draft. Labels immediately following them are retained.
+    text = re.sub(r"(?m)^\\phantomsection\s*$\n?", "", text)
+    text = re.sub(
+        r"(?m)^\\addcontentsline\{toc\}\{subsection\}\{[^\n]*\}\s*$\n?",
+        "",
+        text,
+    )
+
+    # Convert the ruled legacy boxes to the ordinary amsthm hierarchy. The
+    # source labels occur immediately before the environments and remain valid.
+    text = re.sub(
+        r"\\begin\{lemmabox\}\{Lemma\s+[0-9.]+\s+\(([^{}]*)\)\}",
+        r"\\begin{lemma}[\1]",
+        text,
+    )
+    text = re.sub(
+        r"\\begin\{propositionbox\}\{Proposition\s+[0-9.]+\s+\(([^{}]*)\)\}",
+        r"\\begin{proposition}[\1]",
+        text,
+    )
+    text = re.sub(
+        r"\\begin\{resultbox\}\{Theorem\s+[0-9.]+\}",
+        r"\\begin{theorem}",
+        text,
+    )
+    text = text.replace(r"\end{lemmabox}", r"\end{lemma}")
+    text = text.replace(r"\end{propositionbox}", r"\end{proposition}")
+    text = text.replace(r"\end{resultbox}", r"\end{theorem}")
+
+    # Normalize the mathematical English and notation without altering any
+    # finite identity, hypothesis, or summation domain.
+    replacements = {
+        r"\ln": r"\log",
+        "colouring": "coloring",
+        "colourings": "colorings",
+        "coloured": "colored",
+        "colour": "color",
+        "cocolouring": "cocoloring",
+        "cocolourings": "cocolorings",
+        "cocolourable": "cocolorable",
+        "fibre": "fiber",
+        "fibres": "fibers",
+        "neighbourhood": "neighborhood",
+        "neighbourhoods": "neighborhoods",
+        "catalogued": "cataloged",
+    }
+    for old, new in replacements.items():
+        text = text.replace(old, new)
+
+    text = text.replace(
+        "\\section{Notation and elementary\nfacts}",
+        "\\section{Phase notation and elementary estimates}",
+    )
+
+    # Section 10 must point to the replacement normalized-second-moment
+    # proposition rather than to the legacy proposition number.
+    text = text.replace(
+        "Proposition 9.2",
+        "Proposition~\\ref{prop:normalized-second-moment-v3}",
+    )
+    return text
+
+
+def generate(source: Path, output: Path) -> None:
+    raw = source.read_bytes()
+    blob = git_blob_sha(raw)
+    require(
+        blob == EXPECTED_CANONICAL_BLOB,
+        f"canonical source drift: expected {EXPECTED_CANONICAL_BLOB}, found {blob}",
+    )
+    text = raw.decode("utf-8")
+
+    sections_1_to_7 = normalize_legacy_section(
+        slice_between(text, START_SECTION_1, START_SECTION_8)
+    )
+    section_10 = normalize_legacy_section(
+        slice_between(text, START_SECTION_10, START_SECTION_11)
+    )
+
+    generated = "\n".join(
+        [
+            "% GENERATED FILE: do not edit directly.",
+            f"% Canonical source Git blob: {blob}",
+            "% Generator: 625/scripts/build_self_contained_ams_v3.py",
+            "",
+            sections_1_to_7.rstrip(),
+            "",
+            r"\input{SECTION8_SELF_CONTAINED_V3}",
+            "",
+            r"\input{SECTION9_SELF_CONTAINED_V3}",
+            "",
+            section_10.rstrip(),
+            "",
+            r"\input{FINAL_ASSEMBLY_SELF_CONTAINED_V3}",
+            "",
+        ]
+    )
+    output.parent.mkdir(parents=True, exist_ok=True)
+    output.write_text(generated, encoding="utf-8")
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser()
+    root = Path(__file__).resolve().parents[1]
+    parser.add_argument(
+        "--source",
+        type=Path,
+        default=root / "arxiv" / "main.tex",
+    )
+    parser.add_argument(
+        "--output",
+        type=Path,
+        default=root / "arxiv" / "AMS_SELF_CONTAINED_BODY_V3.generated.tex",
+    )
+    args = parser.parse_args()
+    generate(args.source, args.output)
+    print(f"generated {args.output}")
+
+
+if __name__ == "__main__":
+    main()