Referee-proofread and harden the Erdős 625 manuscript

.github/workflows/erdos625-self-contained-manuscript.yml

@@ -16,7 +16,9 @@ on:
       - "625/arxiv/references.bib"
       - "625/scripts/build_self_contained_ams_v3.py"
       - "625/experiments/check_self_contained_manuscript_v3.py"
+      - "625/experiments/check_constant_ledger_v3.py"
       - "625/audits/SELF_CONTAINED_BULLETPROOF_MANUSCRIPT_PASS_2026-08-04.md"
+      - "625/audits/REFEREE_READABILITY_AND_TIER_ONE_PASS_2026-08-05.md"
       - ".github/workflows/erdos625-self-contained-manuscript.yml"
   workflow_dispatch:
 
@@ -36,15 +38,22 @@ jobs:
         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
+          python -m py_compile 625/experiments/check_constant_ledger_v3.py
+      - name: Verify the exact four-support constant
+        run: |
+          python 625/experiments/check_constant_ledger_v3.py \
+            | tee /tmp/erdos625-constant-ledger.txt
       - 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
+      - name: Upload generated TeX body and exact ledger
         uses: actions/upload-artifact@v4
         with:
           name: erdos625-self-contained-generated-body
-          path: 625/arxiv/AMS_SELF_CONTAINED_BODY_V3.generated.tex
+          path: |
+            625/arxiv/AMS_SELF_CONTAINED_BODY_V3.generated.tex
+            /tmp/erdos625-constant-ledger.txt
           if-no-files-found: error
 
   build-complete-pdf:
@@ -113,6 +122,10 @@ jobs:
           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 25 -singlefile -png -r 144 \
+            AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-025
+          pdftoppm -f 32 -singlefile -png -r 144 \
+            AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-032
           pdftoppm -f "$pages" -singlefile -png -r 144 \
             AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-last
       - name: Upload complete manuscript artifacts
@@ -124,5 +137,7 @@ jobs:
             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-025.png
+            /tmp/erdos625-renders/page-032.png
             /tmp/erdos625-renders/page-last.png
           if-no-files-found: error

625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex

@@ -21,7 +21,7 @@
 \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}
+\setlist[enumerate]{leftmargin=2.15em,itemsep=0.16em,topsep=0.36em}
 \setlength{\emergencystretch}{3em}
 \allowdisplaybreaks
 \providecommand{\tightlist}{%
@@ -39,18 +39,18 @@
 
 \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.
+% Verification status switch. This must remain false until the 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},
+  pdftitle={A Full-Sequence Quantitative 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
+\title[Chromatic and cochromatic numbers]{A Full-Sequence Quantitative 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}

625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex

@@ -4,6 +4,7 @@
 % amsthm environments directly.
 
 \theoremstyle{plain}
+\newtheorem*{maintheorem}{Main theorem}
 \newtheorem{theorem}{Theorem}[section]
 \newtheorem{proposition}[theorem]{Proposition}
 \newtheorem{lemma}[theorem]{Lemma}
@@ -17,8 +18,8 @@
 \theoremstyle{remark}
 \newtheorem{remark}[theorem]{Remark}
 
-% Compatibility only. The generator normally converts legacy statement boxes
-% to theorem, lemma, and proposition environments before compilation.
+% Compatibility only. The generator 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}

625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex

@@ -1,155 +1,114 @@
-\section*{Conventions and proof objects}
-\addcontentsline{toc}{section}{Conventions and proof objects}
+\section*{Notation and proof objects}
+\addcontentsline{toc}{section}{Notation 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.
+We collect here only the conventions that are used throughout several later
+sections. More local notation is introduced where it first becomes necessary.
+This keeps the main argument self-contained without forcing the reader to
+retain a large dictionary before the proof begins.
 
-\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
+\paragraph{Asymptotic conventions.}
+All logarithms are natural. An event holds \emph{with high probability} if its
+probability tends to one as $n\to\infty$. Whenever a phase parameter is
+present, $o(1)$ denotes one deterministic error sequence that is uniform over
+the full phase interval, including sequences approaching either endpoint.
+For integers $x,r\ge0$, we use the falling factorial
 \[
-  (x)_r=x(x-1)\cdots(x-r+1),\qquad (x)_0=1.
+  (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}
+and set $(x)_r=0$ for $r>x$. A quotient involving falling factorials is used
+only after the denominator has been shown to be nonzero.
 
-\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
+\paragraph{Signed witnesses and profiles.}
+A \emph{signed cocoloring witness} is a 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 complete. The marks are counting data; they do not
+define a new graph invariant. In the four-size profile every class has size at
+least two for sufficiently large $n$, so a realized class cannot satisfy both
+requirements. Forgetting the marks therefore recovers its cocoloring without
+multiplicity.
+
+A \emph{profile} is a finite sequence $(k_s)$, where $k_s$ is the number of
+classes of size $s$. It is feasible on $n$ vertices when
 \[
   \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}
+The ordinary first moment counts partitions into independent classes. The
+signed first moment counts the same partitions together with one $I/K$ mark
+per class.
 
-\begin{definition}[Overlap table]
+\paragraph{Overlap table and support graph.}
 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}
+Its row and column sums are the class sizes of the two partitions. It may also
+be viewed as the cell-count table of a bipartite configuration model: every
+underlying vertex pairs one labeled row stub with one labeled column stub.
 
-\begin{definition}[Support graph and cycle rank]
-Given an overlap table $r$, let $H(r)$ be the simple bipartite graph whose edge
-set is
+The \emph{support graph} $H(r)$ is the simple bipartite graph with
 \[
   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
+A subset of its edges is \emph{even} if every vertex has even degree. Writing
+$c(H)$ for the number of connected components, including isolated vertices,
+we 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}
+Then $\beta(H)$ is the dimension of the binary cycle space, so the number of
+even edge sets is $2^{\beta(H)}$. The threshold two is exact: a cell of size
+zero or one contains no edge internal to both partition classes, whereas a
+cell of size at least two forces their two signs to agree.
 
-\begin{definition}[Three matching levels]
-Three distinct matching objects occur.
+\paragraph{Three matching levels.}
+The proof uses three distinct objects that should not be conflated.
 \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{physical partial matching} is a set of selected stub pairs inside
+specified 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.
+column-class slots; its edges indicate the cells declared canonical and high.
 \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}
+The product formula for physical cell counts relies on the third object being
+a matching. Distinct selected cells then use disjoint row and column stub
+families.
 
-\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
+\paragraph{High cells, deficits, and endpoint tables.}
+Let $U$ be the largest class size in the four-size profile and put
+$R_0=\lfloor U/2\rfloor$. A cell is \emph{high} when its multiplicity exceeds
+$R_0$. Two high cells cannot share a row or a column, so the high cells form a
+canonical block support. For a selected cell $e$, let $s_e,t_e$ be its endpoint
+sizes and set
 \[
-  s_e,t_e\quad\text{be its endpoint sizes},\qquad
-  m_e=\min\{s_e,t_e\},\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}
+Here $m_e$ is the full-containment multiplicity, $j_e$ is the realized
+multiplicity, and $h_e$ is the deficit. Highness implies $2h_e<m_e$.
 
-\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}
+The four endpoint sizes are indexed by $i,j\in\{0,1,2,3\}$. For a block support
+$P$, the endpoint table $L(P)=(L_{ij})$ records how many support edges join
+endpoint types $i$ and $j$. A \emph{realized} endpoint table is one attained by
+an actual finite block support; it is not an arbitrary element of
+$\mathbb N^{4\times4}$.
 
-\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}
+\paragraph{Separation of accounts.}
+The \emph{bare high-skeleton weight} contains the incidence probability and
+local rewards of the exposed high cells. It contains neither the rewards of
+unexposed cells nor the residual binary cycle-space factor. Conditional on a
+high skeleton, the expectation of those remaining factors is its
+\emph{residual attachment}. Sections~8 and~9 preserve this separation exactly:
+a factor paid in one account is never paid again in the other.
 
-\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}
+Every load-bearing estimate follows the same order. We first state the finite
+identity, then apply deterministic inequalities, then take phase asymptotics,
+and only at the end deduce a probability statement. This order is useful both
+for mathematical auditing and for the theorem-by-theorem formalization.