From c664f92af2e6e4d2b5aaf05f864940767614ded8 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:39:48 +0300 Subject: [PATCH 01/20] Polish theorem hierarchy for the referee draft --- 625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex b/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex index 56b808a..c4df0bc 100644 --- a/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex +++ b/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} From 262a27422d91a79b4e3d99f593248485252ba9ee Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:41:57 +0300 Subject: [PATCH 02/20] Rewrite the abstract and introduction for referees --- ...TMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex | 254 +++++++++--------- 1 file changed, 127 insertions(+), 127 deletions(-) diff --git a/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex b/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex index 8701670..053b6fb 100644 --- a/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex +++ b/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex @@ -5,27 +5,32 @@ \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. +Let $G_n\sim G(n,1/2)$. We prove, along the full sequence of integers $n$, that +\[ + \chi(G_n)-\zeta(G_n)=\Omega\!\left(\frac{n}{(\log n)^3}\right) +\] +with probability tending to one, where $\chi$ and $\zeta$ denote the chromatic +and cochromatic numbers. This resolves the question of Erd\H{o}s and Gimbel +asking whether the difference tends to infinity with high probability. The +principal difficulty is uniformity across the rounding phase of the +independence-number threshold. We overcome it with a signed first-moment +profile supported on four consecutive class sizes. For the second moment, we +derive an exact sign-compatibility identity, sum every large-cell matching +fiber before taking estimates, regroup the full-containment references by their +endpoint tables, and control the residual cycle-space contribution by +restriction outside an exposed matching. A bounded-differences argument then +amplifies the resulting rare witness 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. +Let $G_n\sim G(n,1/2)$. This verification draft gives a self-contained +derivation of a full-sequence lower bound of order $n/(\log n)^3$ for +$\chi(G_n)-\zeta(G_n)$, conditional on the explicitly isolated closure +obligations in Appendix~A. The argument is uniform across the rounding phase of +the independence-number threshold. Its new finite core consists of an exact +sign-compatibility identity, a completion-free summation of the large-cell +matching fibers, an exact regrouping by endpoint table, and a restriction +inequality for residual even subgraphs. The verification status is stated here +because the mathematical manuscript and the formal dependency graph must not +drift apart. \fi \end{abstract} @@ -33,12 +38,10 @@ \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.}} +\small\emph{Verification status.} The theorem below remains conditional on the +phase, first-moment, partial-diagonal, and global assembly gates listed in +Appendix~A. The publication switch must remain disabled until those gates have +been replayed together on one integrated commit. \end{center} \fi @@ -46,30 +49,24 @@ \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 +A \emph{cocoloring} of a graph $G$ is a partition of $V(G)$ into nonempty +classes, each inducing either an empty graph or a complete graph. 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$. +$\zeta(G)$. Since an ordinary proper coloring is a cocoloring using only empty +classes, one always has $\zeta(G)\le\chi(G)$. -Erd\H{o}s and Gimbel asked whether +Let $G_n\sim G(n,1/2)$ be the labeled random graph on $[n]$. 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. +with high probability \citep[p.~263]{erdos-gimbel-1993}. The question was +restated by Gimbel \citep[Section~7.4]{gimbel-2016} and is cataloged as +Erd\H{o}s Problem~625 \citep{bloom-erdos625}. We obtain the following +quantitative full-sequence statement. \ifErdosProofClosed -\begin{theorem}\label{thm:main-v3} +\begin{maintheorem} For $G_n\sim G(n,1/2)$, \[ \mathbb P\!\left( @@ -83,9 +80,9 @@ \section*{Introduction} \] In particular, $\chi(G_n)-\zeta(G_n)$ tends to infinity with high probability along the full sequence of integers $n$. -\end{theorem} +\end{maintheorem} \else -\begin{theorem}[Target theorem]\label{thm:main-v3} +\begin{maintheorem}[Conditional verification statement] 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)$, @@ -99,96 +96,99 @@ \section*{Introduction} \right) \longrightarrow 1. \] -\end{theorem} +\end{maintheorem} \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 +The phrase \emph{full sequence} is substantive. The natural class-size cutoff +jumps whenever the independence-number phase crosses an integer. At such a +jump, changing one admissible class size changes the optimizing profile and +its first-moment root. An estimate proved only for a density-one set of phase +values does not automatically extend to every integer $n$. All asymptotic +estimates in this paper are therefore uniform up to both endpoints of every +phase interval. + +\subsection*{Relation to previous work} + +The first-order asymptotic for the chromatic number of a dense random graph was +proved by Bollob\'as \citep{bollobas-1988}, following the early work of +Grimmett and McDiarmid \citep{grimmett-mcdiarmid-1975}; 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 associated with hereditary graph properties \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. +For the difference $\chi(G_n)-\zeta(G_n)$, Heckel and, independently, Steiner +first connected divergence to the nonconcentration of the chromatic number +\citep{heckel-2024-question,steiner-2024}. Heckel subsequently proved a +near-linear lower bound for a phase-dependent set containing approximately +$95\%$ of the integers \citep{heckel-2025-difference}. The unresolved part is +precisely the exceptional phase. Our argument retains the signed first-moment +idea and the rare-seed amplification from that work, but replaces the pairwise +sign estimate by an exact overlap identity and uses one four-size profile that +remains valid throughout the complete phase interval. -\subsection*{Contributions} +\subsection*{Main ideas} -The proof is organized around five results that are mathematically distinct -and should be read separately. +The proof has four reusable components. \begin{enumerate} -\item A phase-uniform comparison between the ordinary coloring root and a -four-size signed cocoloring root gives a separation of order +\item \textbf{Uniform root separation.} We compare the ordinary coloring root +with the signed cocoloring root supported on four consecutive class sizes. The +comparison is uniform in the complete phase and produces 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. + +\item \textbf{Exact sign compatibility.} For two signed witnesses, the sum over +all compatible sign assignments factors into local cell rewards and the size +of a binary cycle space. No sign correlation is estimated before this exact +identity has been extracted. + +\item \textbf{Large cells without chosen completions.} Cells above half the +class-size cap form a matching. We sum the entire physical matching fiber, +compare it with full containment, and pay the ambient falling-factorial loss +once. The resulting reference weights are regrouped exactly by their endpoint +tables. + +\item \textbf{Residual restriction and amplification.} After the large cells +have been exposed, deletion outside their matching is injective on even +residual edge sets. This converts the residual cycle-space sum into a product +bound. Paley--Zygmund supplies a rare signed witness, and a one-sided +bounded-differences argument amplifies it to a high-probability cocoloring. \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. +The four-size support is the smallest fixed support that simultaneously spans +the entire phase interval and leaves a uniform entropy advantage over ordinary +coloring. Restricting to four values incurs an explicit entropy loss +$D_4(\delta)$, but Section~11 proves the uniform certificate +\[ + \log 2-D_4(\delta) + > + \log\!\left(\frac{1000}{639}\right). +\] +Thus the finite support is not merely a technical truncation: it is the device +that converts phase dependence into a full-sequence theorem. + +\subsection*{Guide to the argument} + +The \emph{location step} identifies two continuous first-moment roots. The +signed witness is placed at a tangent-rounded midpoint, retaining half of their +leading separation while satisfying the exact profile conservation laws. + +The \emph{existence step} studies the normalized second moment of this one +signed profile. Partial diagonals are handled first. The remaining overlap +tables are divided into canonical high cells and residual cells. Sections~8 +and~9 keep these two accounts disjoint: no residual factor is paid in the +high-cell estimate, and no high-cell multiplicity is paid again in the +residual estimate. + +The \emph{amplification step} converts the second-moment seed into a typical +statement. The largest induced subgraph admitting the prescribed number of +cocoloring classes is one-Lipschitz under vertex-block exposure. Its +concentration, together with a simultaneous coloring bound for every leftover +set, makes the amplification uniform in the seed exponent. + +Section~1 fixes the phase notation. Sections~2--5 locate and compare the two +roots. Section~6 proves the exact signed-overlap identity, and Section~7 treats +partial diagonals. Sections~8 and~9 contain the large-cell and residual +estimates. Section~10 proves the amplifier, Section~11 performs the constant +ledger, and Appendix~A records the paper-to-Lean map and the remaining +verification gates. From 678e6a535f6f0ebf6b2bcbf6357454b5de9d5db1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:43:23 +0300 Subject: [PATCH 03/20] Condense the proof-object preliminaries --- .../CONVENTIONS_AND_PROOF_OBJECTS_V3.tex | 195 +++++++----------- 1 file changed, 77 insertions(+), 118 deletions(-) diff --git a/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex b/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex index 13cb60b..c90c693 100644 --- a/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex +++ b/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 Date: Wed, 5 Aug 2026 14:44:29 +0300 Subject: [PATCH 04/20] Replace the technical synopsis with a proof guide --- .../PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex | 159 ++++++++---------- 1 file changed, 69 insertions(+), 90 deletions(-) diff --git a/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex b/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex index 69d4a7c..f1bc1fc 100644 --- a/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex +++ b/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex @@ -1,136 +1,115 @@ -\section*{Proof architecture} -\addcontentsline{toc}{section}{Proof architecture} +\section*{Guide to the proof} +\addcontentsline{toc}{section}{Guide to the proof} \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. +The argument has three stages---location, existence, and amplification---but +the second stage contains most of the new combinatorics. This guide records the +role of each estimate before the detailed proof begins. -\subsection*{Location: two first-moment roots} +\subsection*{1. Locating 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 +the four deficits $2,3,4,5$. If $\delta_n$ denotes the phase, put \[ - A_4(\delta)=\log2-D_4(\delta), + A_4(\delta)=\log 2-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 +where $D_4$ is the entropy loss caused by the four-point restriction. The +phase-uniform analysis gives \[ r_+(n)-r_4^{\mathrm{co}}(n) = \left[ - \frac{(\log2)^2}{4}A_4(\delta_n)+o(1) + \frac{(\log 2)^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 +The signed witness is placed at a tangent-rounded midpoint of these two roots. +The exact conservation correction costs only $O(1)$ classes, so the retained +separation is one half of the leading root gap. Section~11 proves the uniform +certificate \[ - \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) + A_4(\delta)> + \log\!\left(\frac{1000}{639}\right) \qquad(0\le\delta\le1). \] -\subsection*{Existence: one normalized second moment} +\subsection*{2. Extracting the exact overlap structure} -For two ordered signed witnesses, let $r=(r_{ab})$ be their overlap table. -The sign sum is evaluated exactly: +For two ordered signed witnesses, let $r=(r_{ab})$ be their overlap table. The +sum over compatible sign assignments is evaluated before any estimate is +made: \[ \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. +The product is local; the factor $2^{\beta(H(r))}$ is the cardinality of a +binary cycle space. This identity is the point at which the signed problem +separates into cellwise rewards and a topological residual factor. -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. +The normalized second moment is then split by overlap geometry. Section~7 +handles partial diagonals. In every remaining table, a cell above half the +class-size cap is unique in its row and column, so all high cells form 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 +\subsection*{3. Summing high cells before estimating them} + +Fix a high-cell support $P$ and realized multiplicities +$j_e=m_e-h_e$. Because $P$ is a matching, the physical choices in different +cells are independent at the level of finite counting. Their complete +aggregate is \[ w(P,j) = \frac{\prod_{e\in P}(s_e)_{j_e}(t_e)_{j_e}} - {(n)_J\prod_{e\in P}j_e!} + {(n)_{\sum_ej_e}\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$, +Only after this exact fiber has been summed do we compare $j_e$ with the +full-containment multiplicity $m_e$. The local ratios factor, while the sole +nonlocal change is \[ - \frac{(n)_{J+H}}{(n)_J}=(n-J)_H\le n^H. + \frac{(n)_{\sum_em_e}}{(n)_{\sum_ej_e}} + =(n-\textstyle\sum_ej_e)_{\sum_eh_e} + \le n^{\sum_eh_e}. \] -The factor $n^H$ is paid once, after the physical fiber has been summed. +Thus the finite-population loss is paid once rather than once per cell. -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 +The positive deficits are summed by a finite optional-choice product. The +full-containment references are then partitioned by endpoint table, and the +resulting table sum is transported to the one-sided partial-diagonal weights +from Section~7. The four-size phase estimates make the total high-cell cost \[ - \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\}. \] +The underlying fiber identity, deficit product, and reference regrouping are +valid for any finite endpoint alphabet; only the final transport estimate is +specialized to four consecutive sizes. -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. +\subsection*{4. Restricting residual cycles and amplifying the seed} -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 +After the high cells are exposed, Section~9 assigns one activity $q_{ab}$ to +each residual cell. Expanding the local rewards produces a weighted sum over +even residual edge sets. Deleting the exposed matching is injective on this +family: the symmetric difference of two sets with the same restriction would +be an even subset of a matching, and hence empty. The residual cycle-space sum +is therefore bounded by a full product, giving \[ + \mathcal A(M,j) + \le \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 +A two-regime estimate makes the exponent +$o(n/(\log n)^4)$ uniformly in the exposed skeleton. Together with the +high-cell estimate, this yields \[ - \Lambda_n=o\!\left(\frac{n}{(\log n)^4}\right). + \frac{\mathbb E Z^2}{(\mathbb E Z)^2} + \le + \exp\!\left\{o\!\left(\frac{n}{(\log n)^4}\right)\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. +Paley--Zygmund supplies a witness with probability $e^{-o(n/(\log n)^4)}$. +Section~10 then uses vertex-block bounded differences and a simultaneous +leftover-coloring estimate to turn this rare seed into a high-probability +cocoloring at a cost $o(n/(\log n)^3)$. Intersecting it with the ordinary +chromatic lower bound completes the gap estimate. From 812b01df64dce291e428a78a17c67a97d4f4409e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:45:25 +0300 Subject: [PATCH 05/20] Retitle and streamline the referee manuscript --- 625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex b/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex index 5f63ea3..05eb695 100644 --- a/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex +++ b/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} From cf08e54ebe9b774e0396c72781369e4a1d9c0ffa Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:47:39 +0300 Subject: [PATCH 06/20] Normalize proofs and prose in the generated sections --- 625/scripts/build_self_contained_ams_v3.py | 84 ++++++++++++++++++++-- 1 file changed, 78 insertions(+), 6 deletions(-) diff --git a/625/scripts/build_self_contained_ams_v3.py b/625/scripts/build_self_contained_ams_v3.py index 9a2f944..8a4f2c7 100644 --- a/625/scripts/build_self_contained_ams_v3.py +++ b/625/scripts/build_self_contained_ams_v3.py @@ -2,9 +2,10 @@ """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 +extracts the complete Sections 1--7 and 10 from that source, converts their +legacy theorem and proof markup to the ordinary AMS hierarchy, applies a small +set of line-audited prose normalizations, and inserts the replacement Sections +8, 9, and 11. The canonical Git-blob SHA is checked before line-independent section markers are used. """ @@ -45,7 +46,7 @@ def slice_between(text: str, start: str, end: str) -> str: 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. + # draft. Labels immediately following theorem statements are retained. text = re.sub(r"(?m)^\\phantomsection\s*$\n?", "", text) text = re.sub( r"(?m)^\\addcontentsline\{toc\}\{subsection\}\{[^\n]*\}\s*$\n?", @@ -74,10 +75,36 @@ def normalize_legacy_section(text: str) -> str: 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. + # Convert the legacy paragraph proofs to genuine amsthm proof environments. + # Section 7 has one proof divided into three named ranges, so it is handled + # separately before the generic proof conversion. + text = re.sub( + r"\\paragraph\{Proof: the empty corner\.\}\\label\{[^}]+\}\s*", + r"\\begin{proof}\n\\displayheading{Empty corner}\n", + text, + ) + text = re.sub( + r"\\paragraph\{Proof: the central range\.\}\\label\{[^}]+\}\s*", + r"\\displayheading{Central range}\n", + text, + ) + text = re.sub( + r"\\paragraph\{Proof: the full corner\.\}\\label\{[^}]+\}\s*", + r"\\displayheading{Full corner}\n", + text, + ) + text = re.sub( + r"\\paragraph\{Proof\.\}\\label\{[^}]+\}\s*", + r"\\begin{proof}\n", + text, + ) + text = text.replace(r"\(\square\)", r"\end{proof}") + + # Normalize mathematical English and notation without changing any finite + # identity, hypothesis, quantifier, or summation domain. replacements = { r"\ln": r"\log", + r"\log2": r"\log 2", "colouring": "coloring", "colourings": "colorings", "coloured": "colored", @@ -99,6 +126,51 @@ def normalize_legacy_section(text: str) -> str: "\\section{Phase notation and elementary estimates}", ) + prose_replacements = { + ( + "The profile optimization has two jobs. It must locate the zero of the\n" + "first-moment exponent, and it must compare two different supports at the\n" + "same average class size. The affine part of the deficit weight cancels under\n" + "the fixed-mean constraint; only the curved part distinguishes the supports.\n" + "The following lemma packages both facts, together with the uniform derivative\n" + "needed to convert an entropy advantage into a root displacement." + ): ( + "The profile optimization serves two purposes: it locates the first-moment\n" + "root and compares two supports at the same mean class size. Under the\n" + "fixed-mean constraint the affine deficit term cancels, so only the curved\n" + "term distinguishes the supports. The next lemma collects the root corridor,\n" + "the uniform slope, and the support comparison used below." + ), + ( + "It is proved directly for the four-size signed profile, including both\n" + "corners and every intermediate mass, and no tame-profile theorem is invoked." + ): ( + "We prove it directly for the four-size signed profile, uniformly at both\n" + "corners and throughout the intermediate range; no external tame-profile\n" + "theorem is used." + ), + ( + "The proof has three ranges, classified by the vertex mass occupied by the\n" + "marked common classes." + ): ( + "We split the common-subprofile sum according to the vertex mass occupied by\n" + "the marked classes." + ), + ( + "We use the same seed-to-typical strategic principle, but not that theorem as a black box:\n" + "Lemma 10.2 proves the quantitative implication needed here for an arbitrary\n" + "seed exponent \\(\\Lambda_n\\), and Lemma 10.1 supplies the simultaneous\n" + "leftover coloring that controls the added parts." + ): ( + "The amplification follows the same seed-to-typical principle, but the form\n" + "needed here is proved inside the paper. Lemma 10.2 treats an arbitrary seed\n" + "exponent \\(\\Lambda_n\\), and Lemma 10.1 supplies a simultaneous coloring\n" + "bound for every leftover vertex set." + ), + } + for old, new in prose_replacements.items(): + text = text.replace(old, new) + # Section 10 must point to the replacement normalized-second-moment # proposition rather than to the legacy proposition number. text = text.replace( From dcba8e65a4fcc0137cc197a395913bcc0e49d1dc Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:57:00 +0300 Subject: [PATCH 07/20] Harden and clarify the high-skeleton argument --- 625/arxiv/SECTION8_SELF_CONTAINED_V3.tex | 342 ++++++++++++++--------- 1 file changed, 205 insertions(+), 137 deletions(-) diff --git a/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex index 16791e4..e0bab9c 100644 --- a/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex +++ b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex @@ -1,33 +1,26 @@ \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: +This section estimates the contribution of the large overlap cells. The finite +combinatorics and the phase asymptotics are kept separate. We first sum the +entire physical matching fiber for a fixed high-cell demand. We then compare +realized multiplicities with full containment, sum all positive deficits, and +regroup the full-containment references by endpoint table. Only in the final +subsection do we insert the four-size phase estimates. No residual local reward +or cycle-space factor is charged here; those factors belong to Section~9. -\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} +\subsection{The complete physical fiber} -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 +Let $U$ be the largest class 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$. +A cell is \emph{high} if its multiplicity exceeds $R_0$. Two high cells cannot +share a row or a column: otherwise that row or column would contain more than +$U$ stubs. Hence all high cells form a canonical bipartite matching, denoted by +$P$. -For $e\in P$, let $s_e$ and $t_e$ be the endpoint block sizes and define +For $e\in P$, let $s_e$ and $t_e$ be its endpoint block sizes and set \[ m_e:=\min\{s_e,t_e\}, \qquad @@ -35,23 +28,22 @@ \subsection{Canonical support and exact aggregate weight} \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$, +Thus $m_e$ is the full-containment multiplicity, $j_e$ is the realized +multiplicity, and $h_e$ is the deficit. Since $j_e>U/2$ and $m_e\le U$, \begin{equation} 2h_e2/3$ and \eqref{eq:coarse-phase-corridor-v3}, +Using $\log 2>2/3$ and \eqref{eq:coarse-phase-corridor-v3}, we obtain \begin{equation} \frac54\log n-\frac{19}{6} \le @@ -472,31 +536,20 @@ \subsection{Phase smallness of the common charge} \left\lfloor\frac{3m_{ij}-1}{4}\right\rfloor. \label{eq:coarse-log-budget-v3} \end{equation} -Exponentiation yields +Hence \[ 2^{\lfloor(3m_{ij}-1)/4\rfloor} \ge e^{-19/6}n^{5/4}. \] -Since $m_{ij}=O(\log n)$, +Since every $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. +Thus $\rho_{16}\le1$ for all sufficiently large $n$. \begin{proposition}[Bare high-skeleton estimate] \label{prop:bare-high-skeleton-v3} @@ -511,5 +564,20 @@ \subsection{Phase smallness of the common charge} \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. +\begin{proof} +The deficit factor in \eqref{eq:coarse-realized-table-reduction-v3} satisfies +\[ + \log\left(1+(\alpha+1)\rho_{16}\right)^K + \le + K(\alpha+1)\rho_{16} + =O(n^{3/4}\log n). +\] +Proposition~\ref{prop:endpoint-table-sum-v3} contributes +$O(\sqrt{n\log n})$ to the logarithm. Both quantities are +$o(n/(\log n)^4)$. Combining these estimates with +\eqref{eq:coarse-realized-table-reduction-v3} proves the proposition. +\end{proof} + +No residual local reward or binary cycle-space factor has been included in +\operatorname{BareSkeletonSum}_n. Section~9 treats exactly those remaining +factors. From caa12aca84c076a99beba56d0377f1869acec77d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:05:02 +0300 Subject: [PATCH 08/20] Make the residual second-moment argument referee complete --- 625/arxiv/SECTION9_SELF_CONTAINED_V3.tex | 297 +++++++++++++++-------- 1 file changed, 200 insertions(+), 97 deletions(-) diff --git a/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex b/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex index c99c27b..9f0c2fe 100644 --- a/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex +++ b/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex @@ -1,25 +1,25 @@ \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. +Section~8 bounded the sum of the bare high-skeleton weights. It did not include +the rewards of unexposed cells or the binary cycle-space factor of the residual +support. We now condition on one feasible high skeleton and estimate precisely +those remaining factors. -\subsection{Exact conditional decomposition} +\subsection{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 +Let $(d_a)_a$ and $(d'_b)_b$ be the residual row and column degrees. Their two 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 +$H_{\mathrm{res}}$ be the simple support graph of cells with $r'_{ab}\ge2$. +The residual event $\mathcal E(M,j)$ imposes the cap $r'_{ab}\le\lfloor U/2\rfloor$ and forbids any further pair in a cell of $M$. Define \begin{equation} @@ -32,20 +32,20 @@ \subsection{Exact conditional decomposition} \right]. \label{eq:residual-attachment-v3} \end{equation} -The expectation is only over the residual configuration matching. +Only the residual configuration matching is random in this expectation. -The exact overlap decomposition gives +The exact overlap decomposition is \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)$. +where the sum ranges over the finite family of feasible canonical high +skeletons. In view of Proposition~\ref{prop:bare-high-skeleton-v3}, it remains +to bound $\mathcal A(M,j)$ uniformly in $(M,j)$. -\subsection{Local threshold activities} +\subsection{Threshold expansion and cell activities} For a residual cell $(a,b)$ outside $M$, put \begin{equation} @@ -70,65 +70,110 @@ \subsection{Local threshold activities} \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$. +On $M$, set $\lambda_{ab}=q_{ab}=0$. -The local reward has the threshold expansion +We first record the configuration estimate used in the expansion. For a finite +array of nonnegative demands $x=(x_{ab})$, write +$x_a=\sum_bx_{ab}$, $x'_b=\sum_ax_{ab}$, and $X=\sum_{a,b}x_{ab}$. Markov's +inequality applied to the product of binomial cell counts gives \[ - g(r)=1+\sum_{x=3}^{R}\Delta_x\mathbf 1_{\{r\ge x\}} - \qquad(0\le r\le R). + \mathbb P_{\mathrm{res}}(r'_{ab}\ge x_{ab}\text{ for all }a,b) + \le + \frac{ + \prod_a(d_a)_{x_a}\prod_b(d'_b)_{x'_b} + }{ + (m_0)_X\prod_{a,b}x_{ab}! + }. +\] +If $X\le m_0$, then $(m_0)_X\ge(m_0/\mathrm e)^X$; if $X>m_0$, the event is +empty. Hence +\begin{equation} + \mathbb P_{\mathrm{res}}(r'_{ab}\ge x_{ab}\text{ for all }a,b) + \le + \prod_{a,b}\frac{\theta_{ab}^{x_{ab}}}{x_{ab}!}. + \label{eq:prescribed-cell-residual-v3} +\end{equation} +This joint estimate is the reason that cells sharing a row or a column may be +expanded simultaneously. + +For $0\le r\le R$, +\[ + g(r)=1+\sum_{x=3}^{R}\Delta_x\mathbf 1_{\{r\ge x\}}. +\] +Let $E_0$ be the set of all residual cell positions outside $M$, and let +$\mathcal C(M)$ be the family of even subsets of $M\cup E_0$. For +$F\in\mathcal C(M)$, define +\[ +\begin{split} + \Phi_F(r') + := + &\prod_{e\in F\setminus M} + \left( + \mathbf 1_{\{r'_e\ge2\}} + + + \sum_{x=3}^{R}\Delta_x\mathbf 1_{\{r'_e\ge x\}} + \right)\\ + &\times + \prod_{e\in E_0\setminus F} + \left( + 1+ + \sum_{x=3}^{R}\Delta_x\mathbf 1_{\{r'_e\ge x\}} + \right). +\end{split} +\] +The first product contains the support threshold required when $e$ belongs to +the even set. On the event $\mathcal E(M,j)$, expansion of the cycle-space +cardinality and of all local rewards gives the exact identity +\[ + \left(\prod_{a,b}g(r'_{ab})\right) + 2^{\beta(M\cup H_{\mathrm{res}})} + = + \sum_{F\in\mathcal C(M)}\Phi_F(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$, +For every $F\in\mathcal C(M)$, \[ - \mathbb E_{\mathrm{res}}[ - \text{capped local reward with the thresholds of }F] + \mathbb E_{\mathrm{res}}\!\left[ + \Phi_F(r')\mathbf 1_{\mathcal E(M,j)} + \right] \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} + \prod_{e\in F\setminus M}q_e + \prod_{e\in E_0\setminus F}(1+\lambda_e). \] \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. +Expand $\Phi_F$ into its nonnegative threshold monomials. In a cell of +$F\setminus M$, a monomial chooses either the threshold-two term or one higher +increment; it never chooses both. In a cell outside $F\cup M$, it chooses +nothing or one higher increment. Apply +\eqref{eq:prescribed-cell-residual-v3} once to the complete demand of each +monomial. The threshold-two contribution is $\theta_e^2/2$, the higher +increments sum to $\lambda_e$, and the empty choice contributes one. Dropping +the cap and no-return indicator only enlarges the nonnegative expectation. \end{proof} -Summing the preceding bound over the binary cycle space yields +Summing over $F$ and then inserting the missing factors +$1+\lambda_e\ge1$ gives \begin{equation} \mathcal A(M,j) \le - \left(\prod_{a,b}(1+\lambda_{ab})\right) - \sum_{F\ \mathrm{even}} + \left(\prod_{e\in E_0}(1+\lambda_e)\right) + \sum_{F\in\mathcal C(M)} \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. +The next finite lemma is independent of random graphs. \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 +$E$, and let $I\subseteq E$. Suppose that \[ A\longmapsto A\setminus I \] @@ -144,38 +189,41 @@ \subsection{Restriction outside the exposed matching} \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). -\] +set and expand the finite product. \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 +Apply the lemma with $E=M\cup E_0$, $I=M$, and +$\mathcal C=\mathcal C(M)$. The required injectivity is immediate but +important. If two even sets have the same restriction outside $M$, their +symmetric difference is an even subset of the matching $M$. Every nonempty +subset of a matching has a vertex of degree one, so this symmetric difference +must be empty. Therefore \begin{equation} - \sum_{F\ \mathrm{even}} + \sum_{F\in\mathcal C(M)} \prod_{e\in F\setminus M}q_e \le - \prod_{e\notin M}(1+q_e). + \prod_{e\in E_0}(1+q_e). \label{eq:even-family-product-v3} \end{equation} -Since $0\le\lambda_{ab}\le q_{ab}$ pointwise, equations +Since $0\le\lambda_e\le q_e$, equations \eqref{eq:lambda-even-factorization-v3} and -\eqref{eq:even-family-product-v3}, together with $1+x\le e^x$, give +\eqref{eq:even-family-product-v3}, together with $1+x\le e^x$, imply \begin{equation} \mathcal A(M,j) \le - \exp\!\left(2\sum_{a,b}q_{ab}\right). + \exp\!\left(2\sum_{e\in E_0}q_e\right). \label{eq:q-only-attachment-v3} \end{equation} -Thus the local rewards and the cycle-space factor are controlled by one total -activity. +Thus both the local rewards and the cycle-space cardinality are controlled by +one total residual activity. + +\begin{remark} +Lemma~\ref{lem:restriction-product-v3} applies to any weighted set family whose +restriction map is injective. Here the family happens to be a binary cycle +space and injectivity follows solely from the fact that the deleted edge set is +a matching. +\end{remark} \subsection{The intrinsic residual regime} @@ -184,25 +232,68 @@ \subsection{The intrinsic residual regime} 2^U\le m_0^3. \label{eq:intrinsic-residual-regime-v3} \end{equation} -The sequence of majorants +Then $m_0\ge2^{U/3}$ and, by the degree cap, \[ - g(x)\frac{\theta^x}{x!}, - \qquad 3\le x\le R, + \theta_{ab} + \le + \mathrm e U^2 2^{-U/3}. \] -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{lemma}[Quadratic activity bound] +\label{lem:q-quadratic-v3} +There is an absolute constant $C_0$ such that, under +\eqref{eq:intrinsic-residual-regime-v3}, \begin{equation} q_{ab}\le C_0\theta_{ab}^2 \label{eq:q-quadratic-v3} \end{equation} -uniformly in every residual cell. +for every residual cell. +\end{lemma} -The exact second-moment identity for the cell intensities is +\begin{proof} +Fix a cell and write $\theta=\theta_{ab}$. The assertion is trivial when +$\theta=0$. Since $0\le\Delta_x\le g(x)$, it is enough to bound +\[ + a_x:=g(x)\frac{\theta^x}{x!}, + \qquad 3\le x\le R. +\] +For $x\ge3$, +\[ + \frac{a_{x+1}}{a_x} + = + \frac{2^x\theta}{x+1}, + \qquad + \frac{a_{x+2}/a_{x+1}}{a_{x+1}/a_x} + = + 2\frac{x+1}{x+2}>1. +\] +Thus $(a_x)$ is log-convex, and its maximum on $[3,R]$ occurs at an endpoint. +Consequently +\[ + \lambda_{ab} + \le + R(a_3+a_R). +\] +Now $a_3=(2/3)\theta^3$. Since +$R\theta=O(U^3 2^{-U/3})$, one has $Ra_3\le\theta^2$ for all sufficiently +large $U$. + +For the other endpoint, using +$R=\lfloor U/2\rfloor$ and +$\theta\le\mathrm e U^2 2^{-U/3}$ gives +\[ + \log_2\!\left(\frac{a_R}{\theta^2}\right) + \le + -\frac{U^2}{24}+O(U\log U). +\] +Hence $Ra_R\le\theta^2$ for all sufficiently large $U$. It follows that +$\lambda_{ab}\le2\theta^2$ in that range. For the finitely many remaining +values of $U$, the quotient $q_{ab}/\theta^2$ is bounded on the compact interval +$0\le\theta\le\mathrm e U^2 2^{-U/3}$, with limit $1/2$ at $\theta=0$. +Enlarging the constant proves the lemma. +\end{proof} + +The cell intensities satisfy the exact identity \[ \sum_{a,b}\theta_{ab}^2 = @@ -216,12 +307,12 @@ \subsection{The intrinsic residual regime} \qquad \sum_b(d'_b)^2\le Um_0. \] -Together with \eqref{eq:q-quadratic-v3}, this yields +Lemma~\ref{lem:q-quadratic-v3} therefore gives \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 +Together with \eqref{eq:q-only-attachment-v3}, this proves \begin{equation} \mathcal A(M,j)\le\exp(CU^2) \qquad\text{if }2^U\le m_0^3. @@ -230,22 +321,31 @@ \subsection{The intrinsic residual regime} \subsection{The complementary residual regime} -If \eqref{eq:intrinsic-residual-regime-v3} fails, then +Suppose instead that $2^U>m_0^3$. 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 +We may now discard every residual restriction. Since each residual cell count +is at most $U$, \[ - \sum_{a,b}\binom{r'_{ab}}2 + \prod_{a,b}g(r'_{ab}) \le - \frac{U-1}{2}m_0, + 2^{\sum_{a,b}\binom{r'_{ab}}2} + \le + 2^{(U-1)m_0/2}. +\] +Moreover, every edge of $H_{\mathrm{res}}$ uses at least two residual pairs, +so $|E(H_{\mathrm{res}})|\le m_0/2$. Equivalently, the restriction argument +above gives +\[ + 2^{\beta(M\cup H_{\mathrm{res}})} + \le + 2^{|E(H_{\mathrm{res}})|} + \le + 2^{m_0/2}. \] -while the cycle rank of the residual support together with the exposed -matching is at most $m_0/2$. Hence +Multiplication yields \begin{equation} \mathcal A(M,j) \le @@ -256,8 +356,8 @@ \subsection{The complementary residual regime} \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, +There is an absolute constant $C$ such that every feasible canonical high +skeleton satisfies \[ \mathcal A(M,j) \le @@ -268,19 +368,21 @@ \subsection{The complementary residual regime} \] \end{proposition} -The phase satisfies $U=O(\log n)$ and +The phase estimates give \[ + U=O(\log n), + \qquad 2^U=\Theta\!\left(\frac{n^2}{(\log n)^2}\right). \] -In the first regime, $CU^2=O((\log n)^2)$. In the second, +In the intrinsic regime, $CU^2=O((\log n)^2)$. In the complementary regime, \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 +Both exponents are $o(n/(\log n)^4)$, uniformly in the high skeleton. Hence +there is a deterministic sequence $\eta_n\to0$ such that \begin{equation} \mathcal A(M,j) \le @@ -311,15 +413,16 @@ \subsection{The complementary residual regime} \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. +attachment bound. Proposition~\ref{prop:bare-high-skeleton-v3} controls the +remaining high-skeleton sum. The lower bound follows from nonnegativity of the +variance. \end{proof} -Paley--Zygmund now gives +Paley--Zygmund now yields \[ \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. +Section~10 amplifies this rare seed to a high-probability cocoloring. From 8803fde440d9da74cffd9bc0b70bca3d9fc16ebf Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:15:21 +0300 Subject: [PATCH 09/20] Clarify the final theorem and exact constant certificate --- .../FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex | 225 ++++++++++++------ 1 file changed, 153 insertions(+), 72 deletions(-) diff --git a/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex b/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex index 83ce41b..48d5626 100644 --- a/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex +++ b/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex @@ -1,21 +1,23 @@ \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. +We now combine the chromatic lower location, the signed cocoloring upper +location, and the amplification estimate. The two final events are intersected +by a union bound; no independence is used. -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 +\subsection{The phase-resolved gap} + +Let $r_+(n)$ be the ordinary first-moment root and let +$r_4^{\mathrm{co}}(n)$ be the signed four-size root. Section~5 gives \begin{equation} r_+(n)-r_4^{\mathrm{co}}(n) = \left[ - \frac{(\log2)^2}{4}A_4(\delta_n)+o(1) + \frac{(\log 2)^2}{4}A_4(\delta_n)+o(1) \right] \frac{n}{(\log n)^3}, \qquad - A_4(\delta):=\log2-D_4(\delta). + A_4(\delta):=\log 2-D_4(\delta). \label{eq:phase-resolved-root-gap-v3} \end{equation} The tangent-rounded signed profile is placed at @@ -24,23 +26,26 @@ \section{Final assembly and the quantitative constant} = \left\lceil \frac{r_4^{\mathrm{co}}(n)+r_+(n)}2 - \right\rceil+O(1), + \right\rceil+b_n, + \qquad + |b_n|\le C, \] -where the bounded correction enforces the two exact profile conservation laws. -Consequently +where the bounded integer correction enforces the two exact profile +conservation laws. Hence \begin{equation} r_+(n)-k_{\mathrm{co}} = \left[ - \frac{(\log2)^2}{8}A_4(\delta_n)+o(1) + \frac{(\log 2)^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. +The factor $1/8$ has only two sources: the root separation in +\eqref{eq:phase-resolved-root-gap-v3} carries $1/4$, and midpoint placement +divides it by two. The ceiling and tangent correction contribute $O(1)$. -Section~4 gives a deterministic integer $k_\chi^-$ such that +Section~4 constructs a deterministic integer $k_\chi^-$ such that \[ \mathbb P\bigl(\chi(G_n)>k_\chi^-\bigr)\longrightarrow1 \] @@ -49,7 +54,7 @@ \section{Final assembly and the quantitative constant} k_\chi^- - k_{\mathrm{co}} = \left[ - \frac{(\log2)^2}{8}A_4(\delta_n)+o(1) + \frac{(\log 2)^2}{8}A_4(\delta_n)+o(1) \right] \frac{n}{(\log n)^3}. \label{eq:integer-location-gap-v3} @@ -60,59 +65,135 @@ \section{Final assembly and the quantitative constant} \[ \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 +The amplifier in Section~10 produces a deterministic sequence +$a_n=o(n/(\log n)^3)$ such that \[ \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 +Intersecting this event with the chromatic lower event and using +\eqref{eq:integer-location-gap-v3}, we obtain a deterministic +$\epsilon_n\to0$ for which \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} + \mathbb P\!\left( + \chi(G_n)-\zeta(G_n) + \ge + \left[ + \frac{(\log 2)^2}{8}A_4(\delta_n)-\epsilon_n + \right] + \frac{n}{(\log n)^3} + \right) + \longrightarrow1. \label{eq:phase-resolved-final-v3} \end{equation} -with high probability. -\subsection{Exact four-support certificate} +\subsection{An 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 +It remains to replace the phase-dependent factor $A_4(\delta)$ by one explicit +constant. Put $q=\log 2$, let \[ - \frac{49}{20}\log2 - < - \lambda_4 - < - \frac{83}{20}\log2. + w_i(\lambda)=\exp\!\left(\lambda i-\frac q2i^2\right), + \qquad + Z_4(\lambda)=\sum_{i=2}^{5}w_i(\lambda), +\] +and write +\[ + M_4(\lambda) + = + \frac{\sum_{i=2}^{5}i w_i(\lambda)}{Z_4(\lambda)}. \] -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: +For the omitted low and high parts of the unrestricted support, define \[ - L\!\left(\frac{49}{20}\log2\right)<\frac{263}{1000}, + L(\lambda) + := + \frac{\sum_{i=-1}^{1}w_i(\lambda)}{Z_4(\lambda)}, \qquad - H\!\left(\frac{29}{10}\log2\right)<\frac3{200}, + H(\lambda) + := + \frac{\sum_{i=6}^{\infty}w_i(\lambda)}{Z_4(\lambda)}. \] +The mean $M_4$ is strictly increasing, $L$ is strictly decreasing, and $H$ is +strictly increasing. Indeed, the derivative of each log partition ratio is the +difference of the corresponding tilted means, and the three supports are +ordered as \[ - L\!\left(\frac{29}{10}\log2\right)<\frac{33}{250}, + \{-1,0,1\}<\{2,3,4,5\}<\{6,7,\ldots\}. +\] + +The following inequalities are exact rational certificates: +\[ +\begin{array}{c|c|c} +\lambda & \text{mean certificate} & \text{omitted-mass certificate}\\ +\hline +\frac{49}{20}q + & M_4(\lambda)<\frac2q + & L(\lambda)<\frac{263}{1000}\\[2mm] +\frac{29}{10}q + & {} + & L(\lambda)<\frac{33}{250},\quad + H(\lambda)<\frac3{200}\\[2mm] +\frac{83}{20}q + & M_4(\lambda)>1+\frac2q + & H(\lambda)<\frac{29}{200}. +\end{array} +\] +For completeness, here is a fully reproducible verification. Set +\[ + r=2^{1/20}, + \qquad + r_-:=\frac{1035264923841377}{10^{15}}, \qquad - H\!\left(\frac{83}{20}\log2\right)<\frac{29}{200}. + r_+:=\frac{1035264923841378}{10^{15}}. \] -Monotonicity of the two omitted tails therefore gives +The integer inequalities $r_-^{20}<2 \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 +Combining \eqref{eq:phase-resolved-final-v3} with the strict uniform margin in +\eqref{eq:exact-four-support-certificate-v3} yields \[ - \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} + \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) + \longrightarrow1. \] -with high probability. The fixed coefficient is +The coefficient equals \[ - \frac{(\log2)^2}{8} + \frac{(\log 2)^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 +This proves the main theorem. 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. +This proves the conditional verification statement, subject to the closure +gates listed in Appendix~A. The publication switch remains disabled until +those gates have been independently replayed together. \fi \begin{corollary}[Simultaneous complement form] -Under the hypotheses of Theorem~\ref{thm:main-v3}, +Under the hypotheses used above, \[ \min\{\chi(G_n),\chi(\overline{G_n})\}-\zeta(G_n) \ge \left[ - \frac{(\log2)^2}{8} + \frac{(\log 2)^2}{8} \log\!\left(\frac{1000}{639}\right)-o(1) \right] \frac{n}{(\log n)^3} @@ -174,7 +255,7 @@ \subsection{Exact four-support certificate} \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. +The complement $\overline{G_n}$ again has law $G(n,1/2)$, and +$\zeta(\overline G)=\zeta(G)$. Apply the preceding result to $G_n$ and its +complement and intersect the two events by a union bound. \end{proof} From 1776ae4ef927a98a67524a38d7094477c066ed0a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:19:24 +0300 Subject: [PATCH 10/20] Add an exact rational check of the four-support constant --- 625/experiments/check_constant_ledger_v3.py | 155 ++++++++++++++++++++ 1 file changed, 155 insertions(+) create mode 100644 625/experiments/check_constant_ledger_v3.py diff --git a/625/experiments/check_constant_ledger_v3.py b/625/experiments/check_constant_ledger_v3.py new file mode 100644 index 0000000..6f92f64 --- /dev/null +++ b/625/experiments/check_constant_ledger_v3.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Exact rational certificate for the Erdős 625 four-support constant.""" + +from __future__ import annotations + +from fractions import Fraction + + +DEN = 10**15 +R_LO = Fraction(1035264923841377, DEN) +R_HI = Fraction(1035264923841378, DEN) +LOG_SERIES_TERMS = 200 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def power_bounds(exponent: int) -> tuple[Fraction, Fraction]: + """Bounds for r**exponent, where r = 2**(1/20).""" + if exponent >= 0: + return R_LO**exponent, R_HI**exponent + return 1 / (R_HI ** (-exponent)), 1 / (R_LO ** (-exponent)) + + +def weight_exponent(p: int, i: int) -> int: + """Exponent of r at lambda = (p/20) log 2.""" + return p * i - 10 * i * i + + +def sum_bounds( + p: int, + indices: range | list[int], + coefficients: list[int] | None = None, +) -> tuple[Fraction, Fraction]: + indices = list(indices) + if coefficients is None: + coefficients = [1] * len(indices) + require(len(indices) == len(coefficients), "coefficient length mismatch") + lower = Fraction(0) + upper = Fraction(0) + for i, coefficient in zip(indices, coefficients): + lo, hi = power_bounds(weight_exponent(p, i)) + lower += coefficient * lo + upper += coefficient * hi + return lower, upper + + +def quotient_bounds( + numerator: tuple[Fraction, Fraction], + denominator: tuple[Fraction, Fraction], +) -> tuple[Fraction, Fraction]: + n_lo, n_hi = numerator + d_lo, d_hi = denominator + require(d_lo > 0, "nonpositive denominator") + return n_lo / d_hi, n_hi / d_lo + + +def mean_bounds(p: int) -> tuple[Fraction, Fraction]: + indices = list(range(2, 6)) + return quotient_bounds( + sum_bounds(p, indices, indices), + sum_bounds(p, indices), + ) + + +def low_tail_bounds(p: int) -> tuple[Fraction, Fraction]: + return quotient_bounds( + sum_bounds(p, [-1, 0, 1]), + sum_bounds(p, range(2, 6)), + ) + + +def high_tail_upper(p: int) -> Fraction: + """Bound H by summing w_6 and then using a geometric tail from w_7.""" + denominator_lower, _ = sum_bounds(p, range(2, 6)) + _, w6_upper = power_bounds(weight_exponent(p, 6)) + _, w7_upper = power_bounds(weight_exponent(p, 7)) + # For i >= 7, w_{i+1}/w_i is at most w_8/w_7. + _, ratio_upper = power_bounds(p - 20 * 7 - 10) + require(ratio_upper < 1, "tail ratio is not contractive") + return (w6_upper + w7_upper / (1 - ratio_upper)) / denominator_lower + + +def log_two_bounds() -> tuple[Fraction, Fraction]: + partial = sum( + Fraction(1, k * 2**k) + for k in range(1, LOG_SERIES_TERMS + 1) + ) + remainder = Fraction( + 1, + (LOG_SERIES_TERMS + 1) * 2**LOG_SERIES_TERMS, + ) + return partial, partial + remainder + + +def main() -> None: + require( + R_LO**20 < 2 < R_HI**20, + "invalid rational enclosure for 2**(1/20)", + ) + + q_lo, q_hi = log_two_bounds() + _, m49_hi = mean_bounds(49) + m83_lo, _ = mean_bounds(83) + + require(q_hi * m49_hi < 2, "lower tilt does not lie below 2/log 2") + require( + q_lo * (m83_lo - 1) > 2, + "upper tilt does not lie above 1+2/log 2", + ) + + _, l49_hi = low_tail_bounds(49) + _, l58_hi = low_tail_bounds(58) + h58_hi = high_tail_upper(58) + h83_hi = high_tail_upper(83) + + require( + l49_hi < Fraction(263, 1000), + "L(49 log 2 / 20) certificate failed", + ) + require( + h58_hi < Fraction(3, 200), + "H(29 log 2 / 10) certificate failed", + ) + require( + l58_hi < Fraction(33, 250), + "L(29 log 2 / 10) certificate failed", + ) + require( + h83_hi < Fraction(29, 200), + "H(83 log 2 / 20) certificate failed", + ) + + require( + Fraction(263, 1000) + Fraction(3, 200) == Fraction(139, 500), + "first split ledger failed", + ) + require( + Fraction(33, 250) + Fraction(29, 200) < Fraction(139, 500), + "second split ledger failed", + ) + + print("ERDOS 625 CONSTANT LEDGER: PASS") + print(f" M(49 log 2 / 20) upper: {float(m49_hi):.15f}") + print(f" M(83 log 2 / 20) lower: {float(m83_lo):.15f}") + print(f" L(49 log 2 / 20) upper: {float(l49_hi):.15f}") + print(f" L(29 log 2 / 10) upper: {float(l58_hi):.15f}") + print(f" H(29 log 2 / 10) upper: {float(h58_hi):.15f}") + print(f" H(83 log 2 / 20) upper: {float(h83_hi):.15f}") + + +if __name__ == "__main__": + main() From a27ac5bcbfceeb08274ec3ae90a640033ddfc93a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:22:21 +0300 Subject: [PATCH 11/20] Add referee-readability and exact-ledger manuscript gates --- .../check_self_contained_manuscript_v3.py | 51 +++++++++---------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/625/experiments/check_self_contained_manuscript_v3.py b/625/experiments/check_self_contained_manuscript_v3.py index e500086..a682e5a 100644 --- a/625/experiments/check_self_contained_manuscript_v3.py +++ b/625/experiments/check_self_contained_manuscript_v3.py @@ -12,6 +12,7 @@ ROOT = Path(__file__).resolve().parents[1] ARXIV = ROOT / "arxiv" GENERATOR = ROOT / "scripts" / "build_self_contained_ams_v3.py" +CONSTANT_CHECKER = ROOT / "experiments" / "check_constant_ledger_v3.py" GENERATED = ARXIV / "AMS_SELF_CONTAINED_BODY_V3.generated.tex" MASTER = ARXIV / "AMS_SELF_CONTAINED_DRAFT_V3.tex" @@ -54,10 +55,11 @@ def check_balanced_environments(text: str, name: str) -> None: def main() -> None: - for path in [MASTER, GENERATOR, *SOURCE_FILES]: + for path in [MASTER, GENERATOR, CONSTANT_CHECKER, *SOURCE_FILES]: require(path.is_file(), f"missing file: {path}") subprocess.run(["python", str(GENERATOR)], cwd=ROOT.parent, check=True) + subprocess.run(["python", str(CONSTANT_CHECKER)], cwd=ROOT.parent, check=True) require(GENERATED.is_file(), "generator did not create the manuscript body") master = MASTER.read_text(encoding="utf-8") @@ -67,11 +69,10 @@ def main() -> None: 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", - ) + front = sources["FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex"] + require("Verification status" in front, "visible verification status is missing") + require(r"\fbox" not in front, "front matter still contains a boxed status banner") + require(r"\begin{maintheorem}" in front, "unnumbered main theorem is missing") required_master_inputs = ( "AMS_THEOREM_ENVIRONMENTS_V3", @@ -98,10 +99,10 @@ def main() -> None: 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( + generated.count(r"\begin{proof}") >= 10, + "legacy proofs were not converted to AMS proof environments", + ) require( len(generated.splitlines()) >= 1800, f"generated body is unexpectedly short: {len(generated.splitlines())} lines", @@ -115,12 +116,14 @@ def main() -> None: "Aggregate deficit comparison", "Optional-choice product", "Reference grouping", + "Reusable finite core", + "Square-free endpoint transport", "Endpoint-table sum", - "Phase smallness of the common charge", + "Insertion of the phase estimates", r"\rho_{16}", - "canonical finite Lean reduction", ): require(token in section8_flat, f"Section 8 missing: {token}") + require("Lean" not in section8, "Section 8 contains implementation-status prose") section9 = sources["SECTION9_SELF_CONTAINED_V3.tex"] section9_flat = flatten(section9) @@ -128,8 +131,10 @@ def main() -> None: r"\theta_{ab}", r"\lambda_{ab}", r"q_{ab}", + r"\Phi_F", "Fixed even-set expansion", "Restriction-product bound", + "Quadratic activity bound", "The intrinsic residual regime", "The complementary residual regime", "Normalized signed second moment", @@ -139,9 +144,11 @@ def main() -> None: 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"\frac{(\log 2)^2}{8}A_4(\delta_n)", r"\log\!\left(\frac{1000}{639}\right)", - "Exact four-support certificate", + "exact rational certificates", + "1035264923841377", + "check\\_constant\\_ledger\\_v3.py", "Simultaneous complement form", ): require(token in final_flat, f"final assembly missing: {token}") @@ -164,10 +171,13 @@ def main() -> None: "proof omitted", "details are standard", "The endpoint transportation estimate absorbs", + "canonically equivalent to the dependent sum", r"\exp\!left", r"\begin{lemmabox}", r"\begin{propositionbox}", r"\begin{resultbox}", + r"\paragraph{Proof", + r"\(\square\)", r"\ln", ) offenders = [token for token in forbidden if token in combined] @@ -175,18 +185,7 @@ def main() -> None: 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" - ) + duplicates = sorted(label for label, count in label_counts.items() if count > 1) require(not duplicates, f"duplicate labels: {duplicates}") for name, text in {"master": master, "generated": generated, **sources}.items(): From bcc700d9fc1ca5cf789ce4039417c227a1942cc1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:24:46 +0300 Subject: [PATCH 12/20] Extend manuscript CI to the referee and constant checks --- .../erdos625-self-contained-manuscript.yml | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/.github/workflows/erdos625-self-contained-manuscript.yml b/.github/workflows/erdos625-self-contained-manuscript.yml index 4d50797..d1031c7 100644 --- a/.github/workflows/erdos625-self-contained-manuscript.yml +++ b/.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 From eb5325cb79a96c44a4c18923a1e0b7b3f41099f0 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:27:03 +0300 Subject: [PATCH 13/20] Record the referee-readability and publication-rank audit --- ...EADABILITY_AND_TIER_ONE_PASS_2026-08-05.md | 142 ++++++++++++++++++ 1 file changed, 142 insertions(+) create mode 100644 625/audits/REFEREE_READABILITY_AND_TIER_ONE_PASS_2026-08-05.md diff --git a/625/audits/REFEREE_READABILITY_AND_TIER_ONE_PASS_2026-08-05.md b/625/audits/REFEREE_READABILITY_AND_TIER_ONE_PASS_2026-08-05.md new file mode 100644 index 0000000..be4da20 --- /dev/null +++ b/625/audits/REFEREE_READABILITY_AND_TIER_ONE_PASS_2026-08-05.md @@ -0,0 +1,142 @@ +# Referee-readability and publication-rank audit + +**Date:** 2026-08-05 +**Scope:** Erdős Problem 625 self-contained AMS verification manuscript +**Base:** `agent/625-self-contained-bulletproof-manuscript` +**Pass:** `agent/625-referee-readable-tier-one-pass` + +## Executive assessment + +This pass improves the manuscript in the dimensions that a demanding random-graph referee can evaluate directly: theorem visibility, proof navigation, exact finite interfaces, separation of asymptotic and combinatorial arguments, and reproducibility of the quantitative constant. + +It does **not** change the verification status of the top-level theorem. A higher publication rank cannot be obtained by prose alone. The decisive remaining requirement is closure and independent replay of the phase, first-moment, partial-diagonal, and global assembly obligations listed in Appendix A. + +If those obligations close without weakening the full-sequence statement, the mathematical contribution is substantially stronger than the earlier 95%-of-integers result: it resolves the exceptional phase and supplies a quantitative lower bound of order `n/(log n)^3` along every integer sequence. That theorem, rather than additional ornamentation, is the basis for a top specialist or broader high-level submission. + +## Readability changes + +### Front matter + +- Replaced the repository-style boxed warning with a short typographic verification note. +- Rewrote the abstract around the mathematical theorem, obstruction, method, and consequence. +- Replaced the numbered “Theorem 0.1” presentation with an unnumbered main theorem. +- Reorganized the introduction into: + 1. problem and theorem; + 2. relation to previous work; + 3. four main ideas; + 4. why four consecutive sizes are used; + 5. a compact guide to the argument. +- Removed duplicated definitions from the introduction. + +### Proof-object preliminaries + +- Condensed the former sequence of Definition 0.x environments into a short notation section. +- Kept only objects used across multiple later sections. +- Distinguished configuration matchings, physical partial matchings, and block supports in one place. +- Stated the no-double-counting convention for high-skeleton and residual factors explicitly. + +### Generated Sections 1–7 and 10 + +- Converted legacy paragraph proofs and terminal square symbols to genuine AMS `proof` environments. +- Retained the three-part proof structure in Section 7 through descriptive internal headings. +- Normalized `log 2` notation and several high-density transition paragraphs. +- Preserved every finite identity, hypothesis, quantifier, and summation domain from the frozen source. + +## Mathematical hardening + +### Section 8 + +The revised section now exposes the finite argument in the order in which it is valid: + +1. sum the complete matching fiber; +2. extract exact one-cell deficit ratios; +3. pay the ambient falling-factorial loss once; +4. sum optional deficits; +5. partition the full references by endpoint table; +6. transport endpoint tables to the partial-diagonal weights; +7. insert the phase estimates. + +The square-free endpoint comparison is no longer attributed to unnamed “local identities.” Its proof now derives: + +- the exact cancellation of profile and multinomial factors; +- the local ratio between a two-sided full-containment atom and the two one-sided atoms; +- the identity `g(t)/g(s)=2^(ds+binom(d,2))`; +- the one ambient falling-factorial inequality; +- the cancellation producing the `Q_ij` factors. + +The section also identifies the genuinely reusable finite core: the fiber sum, single ambient loss, optional-choice product, and endpoint-table regrouping work for any finite endpoint alphabet whose selected cells form a matching. + +### Section 9 + +The former phrase “capped local reward with the thresholds of F” has been replaced by an exact function `Phi_F(r')`. The cycle-space expansion is now an equality before expectation. + +The joint prescribed-cell estimate is derived explicitly from factorial moments: + +```text +P(r'_ab >= x_ab for all a,b) + <= product_ab theta_ab^(x_ab) / x_ab!. +``` + +The proof now explains why thresholds in cells sharing rows or columns may be expanded simultaneously. + +The activity estimate `q_ab <= C theta_ab^2` has been promoted from a ratio heuristic to a lemma. Its proof uses: + +- the intrinsic-regime bound `theta_ab <= e U^2 2^(-U/3)`; +- log-convexity of `g(x) theta^x / x!`; +- endpoint control at `x=3` and `x=floor(U/2)`; +- the exponent `-U^2/24 + O(U log U)` at the upper endpoint; +- a finite compactness argument for the remaining values of `U`. + +The complementary regime now derives both factors explicitly: + +- local rewards contribute at most `2^((U-1)m_0/2)`; +- restriction outside the exposed matching gives the cycle-space bound `2^(m_0/2)`. + +### Quantitative constant + +The coefficient ledger is now supported by an exact rational checker. It uses: + +```text +r = 2^(1/20), +r_- = 1035264923841377 / 10^15, +r_+ = 1035264923841378 / 10^15, +r_-^20 < 2 < r_+^20. +``` + +All finite weights at the three rational tilts are integral powers of `r`. The high tails are bounded by an explicit first term plus a geometric remainder. Rational bounds for `log 2` come from + +```text +sum_{k=1}^N 1/(k 2^k) +``` + +with an exact tail bound. The checker verifies the mean bracket, all four omitted-mass inequalities, and the final `139/500` ledger without floating-point decisions. + +## What would actually raise the paper to a Tier-1 level + +The manuscript is now closer to a form in which experts can audit the proof efficiently. The remaining rank-limiting issues are mathematical and verification-related: + +1. **Close the concrete phase/chromatic-tail package.** Its constants and full-sequence quantifiers must match the paper exactly. +2. **Close the signed four-size first-moment assembly.** The entropy certificate, root displacement, tangent rounding, and positive signed first moment must be one theorem-facing chain. +3. **Close the complete partial-diagonal theorem.** Empty corner, central range, full corner, and assembly should be separate declarations with uniform phase hypotheses. +4. **Close the global high-skeleton and residual assembly.** The outputs of Sections 8 and 9 must feed one exact normalized-second-moment theorem without duplicate factors. +5. **Replay the final adapter on one integrated commit.** No theorem should be counted as closed from an isolated or stale branch. +6. **Obtain independent expert review.** At least one random-graph specialist should check the first-moment location and one combinatorics/formalization reviewer should check the overlap decomposition. +7. **Only then switch the front matter to publication mode.** The verification note and conditional language are mandatory until the preceding gates are green. + +## Validation contract + +The dedicated workflow now checks: + +- deterministic generation from the frozen canonical TeX blob; +- conversion to AMS proof environments; +- absence of legacy boxes, paragraph proofs, terminal manual squares, placeholders, and implementation prose in Section 8; +- presence of the exact `Phi_F` interface and quadratic-activity lemma; +- exact rational constant verification; +- unique labels and balanced environments; +- successful AMS/BibTeX compilation; +- no unresolved references or citations; +- no overfull box wider than 5 pt; +- a full extractable manuscript of at least 30 pages and 15,000 words; +- representative renders of the first page, Sections 8 and 9, and the final page. + +A green workflow certifies assembly, typesetting, structural invariants, and the constant ledger. It does not by itself certify the remaining top-level mathematical obligations. From 2370dcc9fc3d27edf0452e0ff164b4ee99190999 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:33:39 +0300 Subject: [PATCH 14/20] Use marker-free proof conversion instead of a proof count --- 625/experiments/check_self_contained_manuscript_v3.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/625/experiments/check_self_contained_manuscript_v3.py b/625/experiments/check_self_contained_manuscript_v3.py index a682e5a..5d404d2 100644 --- a/625/experiments/check_self_contained_manuscript_v3.py +++ b/625/experiments/check_self_contained_manuscript_v3.py @@ -99,10 +99,6 @@ def main() -> None: generated.count(r"\section{") >= 8, "generated body does not contain the canonical numbered sections", ) - require( - generated.count(r"\begin{proof}") >= 10, - "legacy proofs were not converted to AMS proof environments", - ) require( len(generated.splitlines()) >= 1800, f"generated body is unexpectedly short: {len(generated.splitlines())} lines", From 3fe34df22195abd3dad123d97ed65cf3987522bf Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:40:38 +0300 Subject: [PATCH 15/20] Fix the final high-skeleton notation in text mode --- 625/arxiv/SECTION8_SELF_CONTAINED_V3.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex index e0bab9c..76a0c8f 100644 --- a/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex +++ b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex @@ -579,5 +579,5 @@ \subsection{Insertion of the phase estimates} \end{proof} No residual local reward or binary cycle-space factor has been included in -\operatorname{BareSkeletonSum}_n. Section~9 treats exactly those remaining +$\operatorname{BareSkeletonSum}_n$. Section~9 treats exactly those remaining factors. From 3aa30e3c3f1a22e690c4665849952c484dd1d4b3 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:47:53 +0300 Subject: [PATCH 16/20] Repair the exact constant display fractions --- 625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex b/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex index 48d5626..e9684fb 100644 --- a/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex +++ b/625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex @@ -126,14 +126,14 @@ \subsection{An exact four-support certificate} \lambda & \text{mean certificate} & \text{omitted-mass certificate}\\ \hline \frac{49}{20}q - & M_4(\lambda)<\frac2q + & M_4(\lambda)<\frac{2}{q} & L(\lambda)<\frac{263}{1000}\\[2mm] \frac{29}{10}q & {} & L(\lambda)<\frac{33}{250},\quad - H(\lambda)<\frac3{200}\\[2mm] + H(\lambda)<\frac{3}{200}\\[2mm] \frac{83}{20}q - & M_4(\lambda)>1+\frac2q + & M_4(\lambda)>1+\frac{2}{q} & H(\lambda)<\frac{29}{200}. \end{array} \] @@ -152,10 +152,10 @@ \subsection{An exact four-support certificate} explicitly and bound the remainder geometrically; the ratio $w_{i+1}/w_i$ decreases by a factor $1/2$ when $i$ increases by one. Finally, \[ - \sum_{k=1}^{N}\frac1{k2^k} + \sum_{k=1}^{N}\frac{1}{k2^k} Date: Wed, 5 Aug 2026 15:50:33 +0300 Subject: [PATCH 17/20] Reject hidden control characters in TeX sources --- 625/experiments/check_self_contained_manuscript_v3.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/625/experiments/check_self_contained_manuscript_v3.py b/625/experiments/check_self_contained_manuscript_v3.py index 5d404d2..97e8388 100644 --- a/625/experiments/check_self_contained_manuscript_v3.py +++ b/625/experiments/check_self_contained_manuscript_v3.py @@ -54,6 +54,15 @@ def check_balanced_environments(text: str, name: str) -> None: ) +def check_control_characters(text: str, name: str) -> None: + bad = [ + (index, ord(character)) + for index, character in enumerate(text) + if ord(character) < 32 and character not in "\n\r\t" + ] + require(not bad, f"{name}: hidden control characters: {bad[:8]}") + + def main() -> None: for path in [MASTER, GENERATOR, CONSTANT_CHECKER, *SOURCE_FILES]: require(path.is_file(), f"missing file: {path}") @@ -185,6 +194,7 @@ def main() -> None: require(not duplicates, f"duplicate labels: {duplicates}") for name, text in {"master": master, "generated": generated, **sources}.items(): + check_control_characters(text, name) check_balanced_environments(text, name) require(text.count("{") == text.count("}"), f"{name}: unbalanced braces") From 911fa60d2c52994b9ee2e387a23f0283995eb372 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 15:55:39 +0300 Subject: [PATCH 18/20] Polish generated theorem titles and proof transitions --- 625/scripts/build_self_contained_ams_v3.py | 70 ++++++++++++++++++---- 1 file changed, 59 insertions(+), 11 deletions(-) diff --git a/625/scripts/build_self_contained_ams_v3.py b/625/scripts/build_self_contained_ams_v3.py index 8a4f2c7..039f844 100644 --- a/625/scripts/build_self_contained_ams_v3.py +++ b/625/scripts/build_self_contained_ams_v3.py @@ -44,6 +44,11 @@ def slice_between(text: str, start: str, end: str) -> str: return text[begin:finish] +def capitalize_theorem_title(match: re.Match[str]) -> str: + prefix, first = match.groups() + return prefix + first.upper() + + def normalize_legacy_section(text: str) -> str: # Remove navigation-only commands that are redundant in the generated AMS # draft. Labels immediately following theorem statements are retained. @@ -74,6 +79,11 @@ def normalize_legacy_section(text: str) -> str: 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}") + text = re.sub( + r"(\\begin\{(?:lemma|proposition|theorem|corollary)\}\[)([a-z])", + capitalize_theorem_title, + text, + ) # Convert the legacy paragraph proofs to genuine amsthm proof environments. # Section 7 has one proof divided into three named ranges, so it is handled @@ -99,6 +109,7 @@ def normalize_legacy_section(text: str) -> str: text, ) text = text.replace(r"\(\square\)", r"\end{proof}") + text = re.sub(r"[ \t]+\\end\{proof\}", r"\n\\end{proof}", text) # Normalize mathematical English and notation without changing any finite # identity, hypothesis, quantifier, or summation domain. @@ -141,6 +152,44 @@ def normalize_legacy_section(text: str) -> str: "term distinguishes the supports. The next lemma collects the root corridor,\n" "the uniform slope, and the support comparison used below." ), + ( + "A \\emph{signed cocoloring} is a partition in which every class is\n" + "declared either ``independent'' or ``complete''; it is realized when each\n" + "class induces the graph specified by its declaration. Thus the sign is a\n" + "two-way declaration attached to a class, and the signed counts below count\n" + "witnesses for ordinary cocolorings rather than a new graph invariant." + ): ( + "Recall that a signed cocoloring witness is a profile partition with one\n" + "independent-or-complete declaration on each class. It is realized when each\n" + "class induces the declared graph. These declarations are auxiliary counting\n" + "data, not a new graph invariant." + ), + ( + "There are two logically separate tasks. First, restricting the deficits to\n" + "\\(S_4=\\{2,3,4,5\\}\\) must cost strictly less than \\(\\log 2\\) per part. Second,\n" + "the \\(2^k\\) choices of signs must convert that strict inequality into a\n" + "macroscopic separation of the two roots. Lemma~5.1 proves the first point;\n" + "the derivative estimate from Lemma~3.1 then proves the second." + ): ( + "The four-size comparison has two steps. Restricting the deficits to\n" + "\\(S_4=\\{2,3,4,5\\}\\) must cost strictly less than \\(\\log 2\\) per part. The\n" + "\\(2^k\\) sign choices then convert this strict entropy margin into a\n" + "macroscopic root separation. Lemma~5.1 proves the margin, and the slope\n" + "estimate in Lemma~3.1 converts it into displacement." + ), + ( + "We first bracket this tilt. At \\(\\lambda=2{\\log 2}\\), we make the\n" + "reindexing completely explicit. The old summation index ranges over" + ): ( + "We begin by bracketing this tilt. At \\(\\lambda=2{\\log 2}\\), set\n" + "\\(j=i-2\\). The original summation index ranges over" + ), + ( + "For completeness, the first strict inequality in (5.4) has the following\n" + "direct verification. Put" + ): ( + "We verify the first strict inequality in (5.4) directly. Put" + ), ( "It is proved directly for the four-size signed profile, including both\n" "corners and every intermediate mass, and no tame-profile theorem is invoked." @@ -156,21 +205,20 @@ def normalize_legacy_section(text: str) -> str: "We split the common-subprofile sum according to the vertex mass occupied by\n" "the marked classes." ), - ( - "We use the same seed-to-typical strategic principle, but not that theorem as a black box:\n" - "Lemma 10.2 proves the quantitative implication needed here for an arbitrary\n" - "seed exponent \\(\\Lambda_n\\), and Lemma 10.1 supplies the simultaneous\n" - "leftover coloring that controls the added parts." - ): ( - "The amplification follows the same seed-to-typical principle, but the form\n" - "needed here is proved inside the paper. Lemma 10.2 treats an arbitrary seed\n" - "exponent \\(\\Lambda_n\\), and Lemma 10.1 supplies a simultaneous coloring\n" - "bound for every leftover vertex set." - ), } for old, new in prose_replacements.items(): text = text.replace(old, new) + text = text.replace( + "We use the same seed-to-typical strategic principle, but not that theorem as a black box:", + "We follow the same seed-to-typical principle, but prove the precise form needed here:", + ) + text = text.replace( + "We now prove the amplification needed to turn this possibly rare event\n" + "into a typical one.", + "We next turn this possibly rare event into a typical one.", + ) + # Section 10 must point to the replacement normalized-second-moment # proposition rather than to the legacy proposition number. text = text.replace( From fb15ce5d6f0c5cc085af4b4ec2c4ed92026e4022 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 16:15:41 +0300 Subject: [PATCH 19/20] Add exact certificates for the partial-diagonal rate split --- .../check_partial_diagonal_rate_v3.py | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 625/experiments/check_partial_diagonal_rate_v3.py diff --git a/625/experiments/check_partial_diagonal_rate_v3.py b/625/experiments/check_partial_diagonal_rate_v3.py new file mode 100644 index 0000000..337923f --- /dev/null +++ b/625/experiments/check_partial_diagonal_rate_v3.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Exact rational endpoint checks for the partial-diagonal rate function.""" + +from __future__ import annotations + +from fractions import Fraction + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def main() -> None: + # With z=1/3, + # log 2 = 2 * sum_{m>=0} z^(2m+1)/(2m+1). + q_lower = 2 * (Fraction(1, 3) + Fraction(1, 81)) + q_upper = 2 * (Fraction(1, 3) + Fraction(1, 72)) + require(q_lower > Fraction(69, 100), "lower bound for log 2 failed") + require(q_upper < Fraction(7, 10), "upper bound for log 2 failed") + + # For x=100/47, the same atanh expansion has z=(x-1)/(x+1)=53/147. + z = Fraction(53, 147) + log_100_over_47_lower = 2 * (z + z**3 / 3) + require( + log_100_over_47_lower > Fraction(3, 4), + "lower bound for log(100/47) failed", + ) + + # First convex rate bound, after adding (1-R)/5000. + first_left_endpoint = ( + -(Fraction(7, 2) * Fraction(2, 3) + 1) / 64 + + Fraction(63, 320000) + ) + first_right_endpoint = ( + -Fraction(47, 100) * log_100_over_47_lower + + Fraction(47, 100) * Fraction(3, 4) + + Fraction(53, 500000) + ) + + # Second convex rate bound, after adding (1-R)/200. + second_left_endpoint = ( + -Fraction(47, 100) * log_100_over_47_lower + + Fraction(53, 100) * Fraction(33, 50) + ) + second_right_endpoint = Fraction(0) + + require(first_left_endpoint < 0, "first rate bound failed at R=1/64") + require(first_right_endpoint < 0, "first rate bound failed at R=47/100") + require(second_left_endpoint < 0, "second rate bound failed at R=47/100") + require(second_right_endpoint == 0, "second rate bound failed at R=1") + + print("ERDOS 625 PARTIAL-DIAGONAL RATE CERTIFICATE: PASS") + print(f" log 2 lower: {q_lower} = {float(q_lower):.15f}") + print(f" log 2 upper: {q_upper} = {float(q_upper):.15f}") + print( + " log(100/47) lower: " + f"{log_100_over_47_lower} = {float(log_100_over_47_lower):.15f}" + ) + print(f" first endpoint R=1/64: {first_left_endpoint}") + print(f" first endpoint R=47/100: {first_right_endpoint}") + print(f" second endpoint R=47/100: {second_left_endpoint}") + + +if __name__ == "__main__": + main() From b4fe7adb1201ed6b9648635ef4772aa80b071ef1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 5 Aug 2026 16:19:37 +0300 Subject: [PATCH 20/20] Replace decimal rate checks by exact rational certificates --- 625/scripts/build_self_contained_ams_v3.py | 126 +++++++++++++++++++-- 1 file changed, 117 insertions(+), 9 deletions(-) diff --git a/625/scripts/build_self_contained_ams_v3.py b/625/scripts/build_self_contained_ams_v3.py index 039f844..8b9d864 100644 --- a/625/scripts/build_self_contained_ams_v3.py +++ b/625/scripts/build_self_contained_ams_v3.py @@ -136,6 +136,18 @@ def normalize_legacy_section(text: str) -> str: "\\section{Notation and elementary\nfacts}", "\\section{Phase notation and elementary estimates}", ) + text = text.replace( + "\\section{The complete independence-number\nphase}", + "\\section{The complete independence-number phase}", + ) + text = text.replace( + "\\section{The four-size signed first-moment\nadvantage}", + "\\section{The four-size signed first-moment advantage}", + ) + text = text.replace( + "\\section{Exact signed second-moment\nrepresentation}", + "\\section{Exact signed second-moment representation}", + ) prose_replacements = { ( @@ -177,13 +189,6 @@ def normalize_legacy_section(text: str) -> str: "macroscopic root separation. Lemma~5.1 proves the margin, and the slope\n" "estimate in Lemma~3.1 converts it into displacement." ), - ( - "We first bracket this tilt. At \\(\\lambda=2{\\log 2}\\), we make the\n" - "reindexing completely explicit. The old summation index ranges over" - ): ( - "We begin by bracketing this tilt. At \\(\\lambda=2{\\log 2}\\), set\n" - "\\(j=i-2\\). The original summation index ranges over" - ), ( "For completeness, the first strict inequality in (5.4) has the following\n" "direct verification. Put" @@ -209,9 +214,112 @@ def normalize_legacy_section(text: str) -> str: for old, new in prose_replacements.items(): text = text.replace(old, new) + text = re.sub( + r"We (?:first|begin by) bracket this tilt\..*?Substituting\s+\\\(i=j\+2\\\) in the weight gives", + ( + "We begin by bracketing this tilt. At \\(\\lambda=2{\\log 2}\\), set\n" + "\\(j=i-2\\), a bijection from \\(S_4\\) onto \\(\\{0,1,2,3\\}\\).\n" + "Substituting \\(i=j+2\\) gives" + ), + text, + count=1, + flags=re.S, + ) + text = text.replace( - "We use the same seed-to-typical strategic principle, but not that theorem as a black box:", - "We follow the same seed-to-typical principle, but prove the precise form needed here:", + "\\gamma_4=\\log\\frac{200}{153}. \\tag{5.2}\n\\]", + ( + "\\gamma_4=\\log\\frac{200}{153}. \\tag{5.2}\n" + "\\]\n" + "This coarse certificate is sufficient for the root separation.\n" + "Section~11 sharpens it to obtain the displayed numerical constant." + ), + ) + + rate_certificate = r"""Here is an exact endpoint certificate for this split. Put +$q=\log 2$. The expansion +\[ + q=2\sum_{m\ge0}\frac{1}{(2m+1)3^{2m+1}} +\] +gives +\[ + \frac{69}{100}69/100$, while bounding every denominator in the +tail from $m=1$ below by $3$ gives +$ q<2(1/3+1/72)=25/36<7/10$. + +For $x=100/47$, the same expansion with +$z=(x-1)/(x+1)=53/147$ yields +\begin{equation} + \log\!\left(\frac{100}{47}\right) + >2\left(z+\frac{z^3}{3}\right) + =\frac{7169416}{9529569}. + \label{eq:partial-diagonal-log-certificate-v3} +\end{equation} + +On $1/64\le R\le47/100$, add $Y/5000=(1-R)/5000$ to the first +bound in (7.23). The resulting function is convex in $R$, and its +largest coefficient occurs at $T=2/q$. At $R=1/64$, using +$\log64=6q$ and $q>2/3$, its value is at most +\[ + \frac{-7q/2-1}{64}+\frac{63}{320000}<0. +\] +At $R=47/100$, equations above give the upper bound +\[ + -\frac{47}{100}\frac{7169416}{9529569} + +\frac{141}{400}+\frac{53}{500000} + =-\frac{4721156593}{4764784500000}<0. +\] +Convexity therefore gives $\Phi_T\le-Y/5000$ throughout this interval. + +On $47/100\le R\le1$, use the second bound in (7.23), add $Y/200$, +and use $T\le1+2/q$. The resulting convex function has value zero at +$R=1$. At $R=47/100$, the bounds $q>69/100$ and +\eqref{eq:partial-diagonal-log-certificate-v3} give +\[ + -\frac{47}{100}\frac{7169416}{9529569} + +\frac{53}{100}\frac{33}{50} + =-\frac{180911419}{47647845000}<0. +\] +Hence $\Phi_T\le-Y/200$ on the second interval. The companion script +\texttt{check\_partial\_diagonal\_rate\_v3.py} verifies these rational +comparisons independently. +Thus, whenever""" + text = re.sub( + r"Here is the numerical check used in this split\..*?Thus, whenever", + lambda _: rate_certificate, + text, + count=1, + flags=re.S, + ) + + text = re.sub( + r"We use the same\s+seed-to-typical strategic principle, but not that theorem as a black box:\s*" + r"Lemma 10\.2 proves the quantitative implication needed here for an arbitrary\s*" + r"seed exponent \\(\\Lambda_n\\\), and Lemma 10\.1 supplies the simultaneous\s*" + r"leftover coloring that controls the added parts\.", + ( + "We follow the same seed-to-typical principle, but prove the precise form\n" + "needed here. Lemma 10.2 treats an arbitrary seed exponent\n" + "\\(\\Lambda_n\\), and Lemma 10.1 supplies a simultaneous coloring bound\n" + "for every leftover vertex set." + ), + text, + count=1, + ) + text = re.sub( + r"The ordinary-coloring concentration argument motivating this amplification\s*" + r"appears in \\citet\[Theorem~1\]\{scott-2008-2017\}\. Lemmas 10\.1 and 10\.2 prove the precise\s*" + r"simultaneous-leftover and rare-seed forms required here\.", + ( + "The vertex-exposure argument is motivated by\n" + "\\citet[Theorem~1]{scott-2008-2017}. Lemma 10.1 gives the simultaneous\n" + "leftover bound, and Lemma 10.2 gives the arbitrary-seed amplifier used here." + ), + text, + count=1, ) text = text.replace( "We now prove the amplification needed to turn this possibly rare event\n"