Make the Erdős 625 manuscript self-contained and verification-safe

.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

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}

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}

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}