diff --git a/.github/workflows/erdos625-self-contained-manuscript.yml b/.github/workflows/erdos625-self-contained-manuscript.yml index 4d507976..442b12ea 100644 --- a/.github/workflows/erdos625-self-contained-manuscript.yml +++ b/.github/workflows/erdos625-self-contained-manuscript.yml @@ -7,6 +7,11 @@ on: - "625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex" - "625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex" - "625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex" + - "625/arxiv/SECTION4_CHROMATIC_LOWER_TAIL_V3.tex" + - "625/arxiv/SECTION5_ROOT_TRANSPORT_V3.tex" + - "625/arxiv/SECTION7_EMPTY_CORNER_V3.tex" + - "625/arxiv/SECTION7_CENTRAL_EXTRACTION_V3.tex" + - "625/arxiv/SECTION7_FULL_CORNER_V3.tex" - "625/arxiv/SECTION8_SELF_CONTAINED_V3.tex" - "625/arxiv/SECTION9_SELF_CONTAINED_V3.tex" - "625/arxiv/FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex" @@ -16,7 +21,14 @@ on: - "625/arxiv/references.bib" - "625/scripts/build_self_contained_ams_v3.py" - "625/experiments/check_self_contained_manuscript_v3.py" + - "625/experiments/check_generator_regexes_v3.py" + - "625/experiments/check_constant_ledger_v3.py" + - "625/experiments/check_partial_diagonal_rate_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" + - "625/audits/PROOF_CLOSURE_CONTRACTS_2026-08-05.md" + - "625/audits/PARTIAL_DIAGONAL_CLOSURE_AUDIT_2026-08-05.md" + - "625/audits/MATHEMATICAL_CLARITY_AND_CLOSURE_PASS_2026-08-06.md" - ".github/workflows/erdos625-self-contained-manuscript.yml" workflow_dispatch: @@ -36,15 +48,39 @@ 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_generator_regexes_v3.py + python -m py_compile 625/experiments/check_constant_ledger_v3.py + python -m py_compile 625/experiments/check_partial_diagonal_rate_v3.py + - name: Validate generator regexes + run: | + python 625/experiments/check_generator_regexes_v3.py \ + | tee /tmp/erdos625-generator-regexes.txt + - name: Verify the exact four-support constant and fixed slack + run: | + python 625/experiments/check_constant_ledger_v3.py \ + | tee /tmp/erdos625-constant-ledger.txt + - name: Verify the partial-diagonal scalar ledger + run: | + python 625/experiments/check_partial_diagonal_rate_v3.py \ + | tee /tmp/erdos625-partial-diagonal-scalar-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, theorem-facing sources, and exact ledgers 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 + 625/arxiv/SECTION4_CHROMATIC_LOWER_TAIL_V3.tex + 625/arxiv/SECTION5_ROOT_TRANSPORT_V3.tex + 625/arxiv/SECTION7_EMPTY_CORNER_V3.tex + 625/arxiv/SECTION7_CENTRAL_EXTRACTION_V3.tex + 625/arxiv/SECTION7_FULL_CORNER_V3.tex + /tmp/erdos625-generator-regexes.txt + /tmp/erdos625-constant-ledger.txt + /tmp/erdos625-partial-diagonal-scalar-ledger.txt if-no-files-found: error build-complete-pdf: @@ -74,6 +110,14 @@ jobs: AMS_SELF_CONTAINED_DRAFT_V3.log; then exit 1 fi + - name: Reject duplicate PDF destinations + working-directory: 625/arxiv + shell: bash + run: | + if grep -F "destination with the same identifier" \ + AMS_SELF_CONTAINED_DRAFT_V3.log; then + exit 1 + fi - name: Reject material overfull boxes working-directory: 625/arxiv shell: bash @@ -113,6 +157,18 @@ 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 12 -singlefile -png -r 144 \ + AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-012 + pdftoppm -f 16 -singlefile -png -r 144 \ + AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-016 + pdftoppm -f 21 -singlefile -png -r 144 \ + AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-021 + pdftoppm -f 23 -singlefile -png -r 144 \ + AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-023 + pdftoppm -f 27 -singlefile -png -r 144 \ + AMS_SELF_CONTAINED_DRAFT_V3.pdf /tmp/erdos625-renders/page-027 + 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 @@ -122,7 +178,18 @@ jobs: path: | 625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.pdf 625/arxiv/AMS_SELF_CONTAINED_BODY_V3.generated.tex + 625/arxiv/SECTION4_CHROMATIC_LOWER_TAIL_V3.tex + 625/arxiv/SECTION5_ROOT_TRANSPORT_V3.tex + 625/arxiv/SECTION7_EMPTY_CORNER_V3.tex + 625/arxiv/SECTION7_CENTRAL_EXTRACTION_V3.tex + 625/arxiv/SECTION7_FULL_CORNER_V3.tex 625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.log /tmp/erdos625-renders/page-001.png + /tmp/erdos625-renders/page-012.png + /tmp/erdos625-renders/page-016.png + /tmp/erdos625-renders/page-021.png + /tmp/erdos625-renders/page-023.png + /tmp/erdos625-renders/page-027.png + /tmp/erdos625-renders/page-032.png /tmp/erdos625-renders/page-last.png if-no-files-found: error diff --git a/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex b/625/arxiv/AMS_SELF_CONTAINED_DRAFT_V3.tex index 5f63ea38..05eb6952 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} diff --git a/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex b/625/arxiv/AMS_THEOREM_ENVIRONMENTS_V3.tex index 56b808a9..c4df0bcc 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} diff --git a/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex b/625/arxiv/CONVENTIONS_AND_PROOF_OBJECTS_V3.tex index 13cb60b7..c90c693a 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_ek_\chi^-\bigr)\longrightarrow1 \] @@ -49,7 +59,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,121 +70,218 @@ \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 with fixed slack} -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 and, crucially, to retain a fixed positive margin over the coefficient +stated in the theorem. 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 +\[ + \{-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)<\frac{2}{q} + & L(\lambda)<\frac{2629}{10000}\\[2mm] +\frac{29}{10}q + & {} + & L(\lambda)<\frac{329}{2500},\quad + H(\lambda)<\frac{37}{2500}\\[2mm] +\frac{83}{20}q + & M_4(\lambda)>1+\frac{2}{q} + & H(\lambda)<\frac{357}{2500}. +\end{array} \] +For completeness, here is a fully reproducible verification. Set \[ - L\!\left(\frac{29}{10}\log2\right)<\frac{33}{250}, + r=2^{1/20}, \qquad - H\!\left(\frac{83}{20}\log2\right)<\frac{29}{200}. + r_-:=\frac{1035264923841377}{10^{15}}, + \qquad + r_+:=\frac{1035264923841378}{10^{15}}. +\] +The integer inequalities $r_-^{20}<2 - \log\!\left(\frac{1000}{639}\right). + \log\!\left(\frac{20000}{12777}\right). \label{eq:exact-four-support-certificate-v3} \end{equation} +The strengthened certificate has an explicit fixed margin over the constant in +the theorem: +\begin{equation} + \log\!\left(\frac{20000}{12777}\right) + = + \log\!\left(\frac{1000}{639}\right) + + + \underbrace{\log\!\left(\frac{12780}{12777}\right)}_{=:~\sigma_4>0}. + \label{eq:fixed-four-support-slack-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 +\eqref{eq:exact-four-support-certificate-v3}, and then taking $n$ large enough +that \[ - \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} + \epsilon_n<\frac{(\log 2)^2}{8}\sigma_4, +\] +yields +\[ + \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 displayed coefficient equals \[ - \frac{(\log2)^2}{8} + \frac{(\log 2)^2}{8} \log\!\left(\frac{1000}{639}\right) =0.026896409808379\ldots. \] +The stronger certificate before absorbing the asymptotic error has coefficient +\[ + \frac{(\log 2)^2}{8} + \log\!\left(\frac{20000}{12777}\right) + =0.026910509263013\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} - \log\!\left(\frac{1000}{639}\right)-o(1) - \right] + \frac{(\log 2)^2}{8} + \log\!\left(\frac{1000}{639}\right) \frac{n}{(\log n)^3} \] with high probability. \end{corollary} \begin{proof} -The law of $\overline{G_n}$ is again $G(n,1/2)$, and -$\zeta(\overline G)=\zeta(G)$. Apply the theorem simultaneously to $G_n$ and -its complement and intersect the two events by a union bound. +The complement $\overline{G_n}$ again has law $G(n,1/2)$, and +$\zeta(\overline G)=\zeta(G)$. The preceding result gives the same exact +coefficient for $G_n$ and for $\overline{G_n}$. Intersect the two events by a +union bound; no further asymptotic loss is introduced. \end{proof} diff --git a/625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex b/625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex index 22a5b86e..5c0308b4 100644 --- a/625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex +++ b/625/arxiv/FORMALIZATION_STATUS_APPENDIX_V3.tex @@ -4,7 +4,7 @@ \section{Formalization map and publication gates} \label{app:formalization-status-v3} This appendix records the relation between the manuscript and the private Lean -4.31 project. It is part of the verification draft because the size of the +4.31 project. It is part of the verification draft because the size of the formal code base must not be confused with completion of the top-level theorem. A declaration is treated as proof evidence only after exact-signature review, warning-fatal replay under the pinned toolchain, a forbidden-shortcut scan, an @@ -21,14 +21,14 @@ \subsection{Status vocabulary} independent replay protocol has passed. \item[Needs review.] The mathematical task is known, but its exact theorem signature, constants, quantifiers, and dependency ledger have not all been -frozen. +frozen and replayed. \item[Blocked.] A downstream theorem whose declared dependencies are not yet all welded. \end{description} \subsection{Section 8 finite chain} -The following finite Section~8 declarations are welded privately. The +The following finite Section~8 declarations are welded privately. The \verb|\path| form is used deliberately so that long theorem names can break at underscores without leaving the page. @@ -66,7 +66,7 @@ \subsection{Section 8 finite chain} The welded finite chain verifies the completion-free physical-fiber factorization, the exact local-to-full comparison, the single global falling-factorial loss, the deficit product, and both unweighted and weighted -regrouping over realized endpoint tables. The current running theorem is the +regrouping over realized endpoint tables. The current running theorem is the remaining real-to-\texttt{ENNReal} phase estimate for the explicit sum of the sixteen endpoint bases. @@ -76,11 +76,102 @@ \subsection{Section 8 finite chain} \quad\Longrightarrow\quad \left(1+(\alpha+1)\rho_{16}\right)^K. \] -This route is aligned with the private finite reduction. The stronger +This route is aligned with the private finite reduction. The stronger pointwise hypothesis $\rho_{ij}\le1/2$ yields the table-preserving product $\prod_{i,j}(1+2\rho_{ij})^{L_{ij}}$ and remains a reusable corollary, but it is not required for the shortest proof closure. +\subsection{Section 5 root-transport interface} + +The manuscript now separates the exact finite support comparison at the +unrestricted root from the asymptotic transport to the phase center. The +standalone source +\path{SECTION5_ROOT_TRANSPORT_V3.tex} defines +\[ + T_+(n)=\alpha-\frac{n}{r_+(n)}, + \qquad + D_{4,n}(T)=\mathcal F_{n,S_+}(T)-\mathcal F_{n,S_4}(T), +\] +and first proves the finite identity +\[ + \Phi_n(r_+)=r_+\{\log 2-D_{4,n}(T_+(n))\}. +\] +It then uses the uniform dual convergence on $K_*$, the bounded limiting +tilts, and the displacement $T_+(n)-T_0$ to define one deterministic error +sequence $\omega_n^{\mathrm{root}}\to0$. The resulting comparison is +\[ + \Phi_n(r_+) + =r_+\{\log 2-D_4(\delta)+O(\omega_n^{\mathrm{root}})\}. +\] +The positive entropy margin and the positive corridor derivative also make the +ordering $r_4^{\mathrm{co}}{\raggedright\arraybackslash}p{0.23\linewidth} + >{\raggedright\arraybackslash}p{0.55\linewidth} + >{\raggedright\arraybackslash}p{0.11\linewidth}} +\toprule +Manuscript role & Lean declaration or theorem-facing evidence & Status\\ +\midrule +\endhead +Empty-corner cutoff activity & +\path{sum_partialDiagonalWeight_le_exp_sum_muCutoffActivity} & Welded\\ +Scalar central-rate inequality & +\path{partialDiagonalRate_uniform_negative} & Welded\\ +Four-deficit structural bridge & +\path{partialDiagonalRate_uniform_negative_fourDeficit} & Welded\\ +Full-corner complementary reindexing & +\path{sum_partialDiagonalWeight_fullCorner_eq} & Welded\\ +Uniform empty-corner asymptotic & +\path{SECTION7_EMPTY_CORNER_V3.tex}; exact Lean theorem not frozen & Needs review\\ +Uniform central Stirling extraction & +\path{SECTION7_CENTRAL_EXTRACTION_V3.tex}; exact Lean theorem not frozen & Needs review\\ +Uniform full-corner ratio estimate & +\path{SECTION7_FULL_CORNER_V3.tex}; exact Lean theorem not frozen & Needs review\\ +Three-range normalized assembly & +\path{SECTION7_FULL_CORNER_V3.tex}; exact Lean theorem not frozen & Needs review\\ +\bottomrule +\end{longtable} +\endgroup + +The scalar rate obstruction is closed: the manuscript and Lean both prove the +$-(1-R)/5000$ margin from the actual four-deficit structural inequalities. The +empty-corner source now iterates the exact recurrence against a uniform +intermediate-denominator bound and records one deterministic error sequence +$\varepsilon_n^{\mathrm{empty}}\to0$. The central source starts from the exact +factorial identity, proves the boundary entropy estimate and the +$\rho$-to-$R$ transport, and records deterministic errors +$\varepsilon_n^{\mathrm{diag}}$ and +$\varepsilon_n^{\mathrm{central}}$. The full-corner source keeps every reverse +recurrence step inside residual mass $n/32$, obtains +$\varepsilon_n^{\mathrm{full}}\to0$, and partitions the coordinate box into +disjoint empty, central, and full ranges before adding the three bounds. + +These additions form a complete candidate manuscript proof of E625-11A--D, +conditional on the exact midpoint profile and positive signed first-moment +margin exported by E625-10. They materially narrow the mathematical closure +boundary, but they do not make E625-11 welded. Each standalone source must be +checked line by line independently, frozen as an exact theorem declaration, +formalized against the actual midpoint-profile objects, and replayed together +with the finite recurrence and reindexing lemmas. The rational checker records +only the scalar constant ledger; it does not certify the asymptotic bridges. + \subsection{Other remaining theorem nodes} The top-level proof also depends on the following nodes. @@ -95,28 +186,29 @@ \subsection{Other remaining theorem nodes} Sections 2--4 & Freeze the concrete phase center, slope, and root package, then export the chromatic lower-tail theorem with the required full-sequence quantifiers. & Needs review\\ -Section 5 & Assemble the welded four-support entropy certificate, the root -separation, tangent rounding, and the positive signed first moment into one -exact theorem consumed by the final adapter. & Needs review\\ -Section 7 & Split and prove the empty-corner, central-rate, and full-corner -asymptotic sums uniformly in the phase; only the exact full-corner reindexing is -currently welded. & Needs review\\ +Section 5 & Independently verify and formalize the finite-target root transport +in \path{SECTION5_ROOT_TRANSPORT_V3.tex}; then assemble it with the welded +four-support entropy certificate, tangent rounding, and the positive signed +first moment into the exact theorem consumed by the final adapter. & Needs review\\ +Section 7 & Independently verify and formalize the complete candidate +three-range package in the three standalone sources; freeze one normalized +partial-diagonal theorem with one phase-uniform eventuality threshold. The +finite recurrence, scalar geometry, structural bridge, and full-corner +reindexing are welded. & Needs review\\ Sections 8--9 & Combine phase smallness, endpoint transport, the skeleton -quotient estimate, and the welded residual attachment theorem into the global -normalized-second-moment hypothesis. & Blocked on the preceding nodes\\ +quotient estimate, the zero-residual case, and the conditioned two-regime +attachment estimate into the global normalized-second-moment hypothesis. & Blocked on the preceding nodes\\ Sections 10--11 & The conditional rare-seed amplifier and final event adapter are welded, but their concrete hypotheses must be instantiated by the preceding nodes. & Conditional adapter welded\\ \bottomrule \end{longtable} -The partial-diagonal node is the largest remaining analytic formalization. It -should be divided into four exact declarations rather than submitted as one -broad request: +The partial-diagonal formalization should retain four exact declarations: \[ - \text{empty corner},\quad - \text{central rate},\quad - \text{full-corner wrapper},\quad + \text{empty-corner bridge},\quad + \text{central Stirling bridge},\quad + \text{full-corner bridge},\quad \text{partial-diagonal assembly}. \] The same discipline should be used for the phase and first-moment nodes. @@ -137,7 +229,7 @@ \subsection{Publication gate} \item the manuscript constants, quantifiers, bibliography, and theorem names are synchronized with that root; \item the full TeX source compiles without unresolved references, citations, -or status placeholders; +duplicate PDF destinations, or status placeholders; \item an independent mathematical review confirms that no private or public staging lemma is being counted twice. \end{enumerate} @@ -148,7 +240,7 @@ \subsection{Publication gate} \subsection{Recommended theorem-facing Lean organization} The internal project contains hundreds of fine-grained modules, including both -legacy and simplified proof routes. For publication, the formalization should +legacy and simplified proof routes. For publication, the formalization should export a small curated root: \begin{itemize} \item \path{Erdos625/Paper/Phase.lean}; @@ -160,11 +252,11 @@ \subsection{Recommended theorem-facing Lean organization} \item \path{Erdos625/Paper/Main.lean}. \end{itemize} The paper-facing root should import only the declarations corresponding to -named manuscript results. The complete historical development may remain in -a separate exhaustive root, and the superseded cycle/walk route should be -marked as legacy rather than appearing in the main theorem dependency chain. +named manuscript results. The complete historical development may remain in a +separate exhaustive root, and the superseded cycle/walk route should be marked +as legacy rather than appearing in the main theorem dependency chain. A machine-readable manifest should map every named paper result to its exact -Lean declaration, source file, commit, status, and axiom audit. The +Lean declaration, source file, commit, status, and axiom audit. The formalization appendix and reproducibility table can then be generated from that manifest, eliminating manual status drift. diff --git a/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex b/625/arxiv/FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex index 87016708..053b6fbe 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. diff --git a/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex b/625/arxiv/PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex index 69d4a7cd..f1bc1fc4 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. diff --git a/625/arxiv/SECTION4_CHROMATIC_LOWER_TAIL_V3.tex b/625/arxiv/SECTION4_CHROMATIC_LOWER_TAIL_V3.tex new file mode 100644 index 00000000..2a0e9bba --- /dev/null +++ b/625/arxiv/SECTION4_CHROMATIC_LOWER_TAIL_V3.tex @@ -0,0 +1,177 @@ +\section{\texorpdfstring{A uniform lower location for +$\chi$}{A uniform lower location for chi}} +\label{a-valid-unrestricted-lower-location-for-chi} + +Let $r_+(n)=r_{S_+,0}$ be the unrestricted zero from Lemma~3.1, and put +\begin{equation*} + k_\chi^-:=\lfloor r_+(n)\rfloor-\lceil\log n\rceil. + \tag{4.1} +\end{equation*} +This is a deterministic integer. Since +$r_+(n)=\Theta(n/\log n)$ uniformly in the phase, one has +$1\le k_\chi^-0$ such that +\begin{equation*} + \frac{d}{dk}L_+(n,k)\ge c_*(\log n)^2 + \qquad + (k_\chi^-\le k\le r_+) + \tag{4.3c} +\end{equation*} +for all sufficiently large $n$, uniformly in the phase. Since +$L_+(n,r_+)=0$, the mean-value theorem and (4.3b) imply +\begin{equation*} + L_+(n,k_\chi^-) + \le-c_*(\log n)^2\Delta_n + \le-c_*(\log n)^3. + \tag{4.4} +\end{equation*} +Combining (4.3) and (4.4), and decreasing the constant once, gives a +deterministic sequence +\[ + \varepsilon_n^{\mathrm{prof}} + := + \exp\{-c_\chi(\log n)^3\} + \longrightarrow0 +\] +such that +\begin{equation*} + E_{n,k_\chi^-,\alpha+1} + \le\varepsilon_n^{\mathrm{prof}}. + \tag{4.4a} +\end{equation*} + +\subsection*{Removing the size cap} + +Let +\[ + \mathcal A_n:=\{\alpha(G_n)\le\alpha+1\}. +\] +Equation (2.9) gives a deterministic phase-uniform sequence +$\varepsilon_n^{\mathrm{cap}}\to0$ such that +\[ + \Prob{\mathcal A_n^c} + \le\varepsilon_n^{\mathrm{cap}}. +\] +On $\mathcal A_n$, every class of every proper coloring has size at most +$\alpha+1$. + +Suppose that $\chi(G_n)\le k_\chi^-$ and choose a proper coloring with +$h\le k_\chi^-$ nonempty classes. If $hk_\chi^-}\longrightarrow1. + \tag{4.6} +\end{equation*} +The direction is strict, as required by the final event intersection. + +Finally, (4.3b) also records the location precision: +\begin{equation*} + |k_\chi^--r_+(n)| + <\log n+2 + =o\!\left(\frac{n}{(\log n)^3}\right). + \tag{4.7} +\end{equation*} +Thus both the probability statement and the location error hold with one set +of phase-independent thresholds along the full sequence of integers. diff --git a/625/arxiv/SECTION5_ROOT_TRANSPORT_V3.tex b/625/arxiv/SECTION5_ROOT_TRANSPORT_V3.tex new file mode 100644 index 00000000..0a630dca --- /dev/null +++ b/625/arxiv/SECTION5_ROOT_TRANSPORT_V3.tex @@ -0,0 +1,80 @@ +% Replacement root-transport passage for Section 5. + +Put +\[ + \Phi_n(k):=L_{S_4}(n,k)+(\log 2)k. +\] +Then $\Phi_n(r_4^{\mathrm{co}})=0$ by definition. To evaluate the same +function at the unrestricted root, let +\[ + T_+(n):=\alpha-\frac{n}{r_+(n)} +\] +and introduce the finite-$n$ support loss +\[ + D_{4,n}(T):= + \mathcal F_{n,S_+}(T)-\mathcal F_{n,S_4}(T). +\] +Since $L_{S_+}(n,r_+)=0$, the exact support-comparison identity (3.8) gives +\begin{equation*} +\begin{aligned} + \Phi_n(r_+) + &=L_{S_4}(n,r_+)-L_{S_+}(n,r_+)+(\log 2)r_+\\ + &=r_+\{\log 2-D_{4,n}(T_+(n))\}. +\end{aligned} +\tag{5.9a} +\end{equation*} +This equality is finite and contains no limiting substitution. + +We now transport its target mean to the phase center. Equation (3.6) gives +\begin{equation*} + T_+(n)=T_0+O\!\left(\frac{\log\log n}{\log n}\right) + \tag{5.9b} +\end{equation*} +uniformly in the phase. On the compact interval $K_*$, equation (3.9) gives +uniform convergence of both finite dual values. The limiting dual value is +differentiable, with +\[ + \mathcal F_S'(T)=-\lambda_S(T), +\] +because the envelope theorem cancels the derivative of the optimizing tilt. +The tilts are uniformly bounded on $K_*$, so both $\mathcal F_{S_+}$ and +$\mathcal F_{S_4}$ are uniformly Lipschitz there. + +More explicitly, choose a deterministic sequence +\[ +\begin{split} + \omega_n^{\mathrm{root}}:= + &\sup_{T\in K_*} + |\mathcal F_{n,S_+}(T)-\mathcal F_{S_+}(T)|\\ + &+\sup_{T\in K_*} + |\mathcal F_{n,S_4}(T)-\mathcal F_{S_4}(T)| + +C|T_+(n)-T_0|, +\end{split} +\] +where $C$ is a common Lipschitz constant for the two limiting dual values. +Then $\omega_n^{\mathrm{root}}\to0$ uniformly in the phase, and +\[ + |D_{4,n}(T_+(n))-D_4(\delta)| + \le \omega_n^{\mathrm{root}}. +\] +Substitution into (5.9a) yields the theorem-facing estimate +\begin{equation*} + L_{S_4}(n,r_+)+(\log 2)r_+ + =r_+\{\log 2-D_4(\delta)+O(\omega_n^{\mathrm{root}})\} + =r_+\{\log 2-D_4(\delta)+o(1)\}. + \tag{5.10} +\end{equation*} +Thus the $o(1)$ in (5.10) is one deterministic error sequence valid across +the complete phase, including integer sequences approaching either endpoint. + +Finally, Lemma~5.1 gives +$\log 2-D_4(\delta)\ge\gamma_4>0$. Hence (5.10) implies +$\Phi_n(r_+)>0$ for all sufficiently large $n$, uniformly in the phase. The +derivative estimate (3.7) is positive throughout the common root corridor, so +$\Phi_n$ is strictly increasing there. Since +$\Phi_n(r_4^{\mathrm{co}})=0$, this proves +\[ + r_4^{\mathrm{co}}0$ after decreasing $c_p$ once. Hence there is an +absolute $C_{\mathrm H}$ such that, for $c_p\le p\le1$ and $0\le y\le p$, +\begin{equation*} + 2p\log p-2(p-y)\log(p-y)-y\log y-y + \le C_{\mathrm H}y\log\!\left(\frac{\mathrm e}{y}\right). + \tag{7.14a} +\end{equation*} +Indeed, when $y\le p/2$, the mean-value theorem bounds +$p\log p-(p-y)\log(p-y)$ by $Cy$, while $-y\log y$ supplies the only +singular term. When $y\ge p/2$, one has $y\ge c_p/2$, and the assertion follows +by compactness. Finally, +\[ + \sum_i y_i\log\!\left(\frac{\mathrm e}{y_i}\right) + \le + Y\log\!\left(\frac{4\mathrm e}{Y}\right), +\] +by the entropy bound on four coordinates. This is +$O(Y\log(\mathrm e/Y))$ uniformly. + +Since $u_{i+1}=u_i-1$, exact subtraction in (7.15) gives +\begin{equation*} +\begin{aligned} + E_{i+1}-E_i + &=\log n-\log(\alpha-i)-(\log 2)(\alpha-i)+\log 2-1\\ + &=-\frac{\log 2}{2}\alpha+O(1), +\end{aligned} + \tag{7.16} +\end{equation*} +uniformly for $2\le i\le4$. For the second line, use +$(\log 2)\alpha/2=\log n-\log\log n+O(1)$ and +$\log(\alpha-i)=\log\log n+O(1)$. + +Let $\bar E=\sum_i p_iE_i$. Applying Stirling once to the complete signed +first moment gives +\begin{equation*} + -\frac1{k_{\mathrm{co}}} + \log \Exp{Z_{\mathbf k}^{\mathrm{sgn}}} + =\sum_i p_i\log p_i-1+\bar E+o(1). + \tag{7.17} +\end{equation*} +The phase-uniform margin (5.19) implies $\bar E\le C_E$. To expose the affine +structure in (7.16), set +\[ + F_i:=E_i+\frac{(\log 2)\alpha}{2}i. +\] +Then $F_{i+1}-F_i=O(1)$. Because the support has only four consecutive +indices, +\[ + F_i=\sum_jp_jF_j+O(1) + =\bar E+\frac{(\log 2)\alpha}{2}T+O(1). +\] +Consequently +\[ + E_i=\bar E-\frac{(\log 2)\alpha}{2}(i-T)+O(1), +\] +and therefore +\begin{equation*} + \sum_i y_iE_i + \le\frac{(\log 2)\alpha}{2}(TY-I)+O(Y). + \tag{7.18} +\end{equation*} +Only the upper bound on $\bar E$ is used here. + +It remains to replace the true residual fraction $\rho$ by the profile +fraction $R$. Since $2\le i,T\le5$, +\[ + |I-TY|=\left|\sum_i(i-T)y_i\right|\le3Y, +\] +so (7.13) gives +\[ + |\rho-R|\le\frac{3Y}{\alpha-T}=O(Y/\alpha). +\] +If $\rho\ge1/32$, then $Y\le1$ and the preceding bound implies +$R\ge1/64$ for all sufficiently large $n$. Hence $x\mapsto x\log x$ is +uniformly Lipschitz on the interval between $R$ and $\rho$. Moreover, +$-R\log R\le1-R=Y$. Thus +\[ +\begin{aligned} +&\left|n\rho\log\rho + -k_{\mathrm{co}}\alpha R\log R\right|\\ +&\qquad\le + k_{\mathrm{co}}(\alpha-T)C|\rho-R| + +k_{\mathrm{co}}T|R\log R| + \le Ck_{\mathrm{co}}Y, +\end{aligned} +\] +which proves +\begin{equation*} + n\rho\log\rho + =k_{\mathrm{co}}\alpha R\log R+O(k_{\mathrm{co}}Y). + \tag{7.19} +\end{equation*} +Combining (7.14), (7.14a), (7.18), and (7.19) yields one absolute constant +$C$ such that +\begin{equation*} + \log D(\ell) + \le k_{\mathrm{co}}\alpha\Phi_T(z) + +Ck_{\mathrm{co}}Y\log\!\left(\frac{\mathrm e}{Y}\right) + +C\log n, + \tag{7.20} +\end{equation*} +where +\begin{equation*} + \Phi_T(z)=R\log R+\frac{\log 2}{2}(I_r-TR). + \tag{7.21} +\end{equation*} +All constants and eventuality thresholds in this extraction are independent of +the phase. + +\displayheading{Uniform rate negativity} +The four-deficit geometry gives +\begin{equation*} + I_r-TR\le(5-T)R, + \qquad + I_r-TR=\sum_i(T-i)y_i\le(T-2)(1-R). + \tag{7.22} +\end{equation*} +Put $q=\log 2$ and recall that $Y=1-R$. Multiplying the first inequality in +(7.22) by $Y$, the second by $R$, and adding gives +\begin{equation*} + I_r-TR\le3RY. + \tag{7.22a} + \label{eq:partial-diagonal-combined-structural-v3} +\end{equation*} +For $0\eta n, + \qquad + n-m>n/32. + \tag{7.24} +\end{equation*} +Then $\rho>1/32$, and +\[ + \frac mn=\frac{\alpha Y-I}{\alpha-T} + \le\frac{\alpha Y}{\alpha-T} +\] +implies +\[ + Y>\eta\frac{\alpha-T}{\alpha}\ge\frac\eta2 +\] +for all sufficiently large $n$. Define the deterministic error ratio +\begin{equation*} + \varepsilon_n^{\mathrm{diag}} + := + \frac{C\log(2\mathrm e/\eta)}{\alpha} + + + \frac{2C\log n}{k_{\mathrm{co}}\alpha\eta}. + \tag{7.24a} +\end{equation*} +Since +\[ + \alpha=\Theta(\log n), + \qquad + k_{\mathrm{co}}=\Theta(n/\log n), + \qquad + \eta=\Theta(\log\log n/\log n), +\] +one has $\varepsilon_n^{\mathrm{diag}}\to0$, uniformly in the phase. Because +$Y\ge\eta/2$, equations (7.20) and (7.23) give +\[ + \log D(\ell) + \le + -k_{\mathrm{co}}\alpha Y + \left(\frac1{5000}-\varepsilon_n^{\mathrm{diag}}\right). +\] +For all sufficiently large $n$, the parenthesis is at least $1/10000$. +Moreover, $\alpha\eta=\Theta(\log\log n)$. Hence there is a phase-independent +$c>0$ such that +\begin{equation*} + D(\ell) + \le + \exp\{-c k_{\mathrm{co}}\log\log n\}. + \tag{7.25} +\end{equation*} +Define +\[ + \varepsilon_n^{\mathrm{central}} + := + (k_{\mathrm{co}}+1)^4 + \exp\{-c k_{\mathrm{co}}\log\log n\}. +\] +There are at most $(k_{\mathrm{co}}+1)^4$ subprofiles, so the total +central-range contribution is at most +$\varepsilon_n^{\mathrm{central}}$. Since +$k_{\mathrm{co}}\log\log n\gg\log n$, this deterministic sequence tends to +zero, uniformly in the phase and with one eventuality threshold for the +complete phase. diff --git a/625/arxiv/SECTION7_EMPTY_CORNER_V3.tex b/625/arxiv/SECTION7_EMPTY_CORNER_V3.tex new file mode 100644 index 00000000..abad2b3f --- /dev/null +++ b/625/arxiv/SECTION7_EMPTY_CORNER_V3.tex @@ -0,0 +1,101 @@ +% Replacement empty-corner proof for Section 7. +% This file is inserted inside the proof of Lemma 7.1. + +\displayheading{Empty corner} + +Let +\[ + \eta=\frac{\log\log n}{32\log n}, + \qquad + \xi_i=\frac{k_i^2}{2\mu_{u_i}(n)}, + \qquad + \Xi_{\mathrm{empty}}=\sum_i\xi_i. + \tag{7.8} +\] +Equations (2.4), (2.8), and +$k_i=\Theta(n/\log n)$ imply, with one phase-independent constant, +\begin{equation*} + \Xi_{\mathrm{empty}} + =O\!\left((\log n)^{-(2/\log 2-1/2)}\right). + \tag{7.9} +\end{equation*} +We now state explicitly how this activity at ambient size $n$ controls every +intermediate denominator in the selected-mass range. + +Fix a final subprofile $\ell$ with selected mass $m\le\eta n$, and expose its +blocks in any order. At an intermediate selected mass $m'\le m$, the exact +ratio of first moments is +\[ + \frac{\mu_{u_i}(n)}{\mu_{u_i}(n-m')} + = rac{(n)_{u_i}}{(n-m')_{u_i}} + =\prod_{r=0}^{u_i-1} + \frac{n-r}{n-m'-r}. +\] +Uniformly in the phase, $u_i=O(\log n)$ whereas +$\eta n\gg\log n$. Hence, for all sufficiently large $n$, +$m'+r\le2\eta n$ throughout this product, and therefore +\[ + \frac{\mu_{u_i}(n)}{\mu_{u_i}(n-m')} + \le(1-2\eta)^{-u_i}. +\] +The phase expansion and $\log 2>2/3$ give $u_i\le3\log n$ eventually. Since +$\eta\le1/4$ and $-\log(1-2\eta)\le4\eta$, +\begin{equation*} + (1-2\eta)^{-u_i} + \le\exp(4\eta u_i) + \le\exp\!\left(\frac38\log\log n\right) + =(\log n)^{3/8}. + \tag{7.10} +\end{equation*} +Every threshold in this estimate is independent of the phase. + +Suppose the current partial profile is $a$ and the next selected block has type +$i$. The exact recurrence (7.4), the inequality +$(k_i-a_i)^2\le k_i^2$, and (7.10) give +\[ + \frac{D(a+e_i)}{D(a)} + \le + \frac{(\log n)^{3/8}\xi_i}{a_i+1}. +\] +Multiplication along any exposure order gives the order-independent bound +\[ + D(\ell) + \le + \prod_i + \frac{\bigl((\log n)^{3/8}\xi_i\bigr)^{\ell_i}} + {\ell_i!}. +\] +All summands are nonnegative, so enlarging from the selected-mass range to the +whole nonnegative four-dimensional lattice and expanding the exponential +series yields +\begin{equation*} + 1 + \le + \sum_{m\le\eta n}D(\ell) + \le + \exp\!\left((\log n)^{3/8}\Xi_{\mathrm{empty}}\right). + \tag{7.11} +\end{equation*} +The lower bound is the empty marked subprofile. + +For clarity, the exponent tends to zero with a fixed power margin. Indeed, +put $q=\log 2$. By (7.9), +\[ + (\log n)^{3/8}\Xi_{\mathrm{empty}} + =O\!\left((\log n)^{-(2/q-7/8)}\right), +\] +and $q<7/10$ gives +\[ + \frac2q-\frac78 + >\frac{20}{7}-\frac78 + =\frac{111}{56}>0. +\] +Thus, for one deterministic sequence +$\varepsilon_n^{\mathrm{empty}}\to0$ independent of the phase, +\[ + 1 + \le + \sum_{m\le\eta n}D(\ell) + \le e^{\varepsilon_n^{\mathrm{empty}}} + =1+o(1). +\] diff --git a/625/arxiv/SECTION7_FULL_CORNER_V3.tex b/625/arxiv/SECTION7_FULL_CORNER_V3.tex new file mode 100644 index 00000000..7153aa5c --- /dev/null +++ b/625/arxiv/SECTION7_FULL_CORNER_V3.tex @@ -0,0 +1,125 @@ +% Replacement full-corner proof and range assembly for Section 7. +% This file is inserted inside the proof of Lemma 7.1. + +\displayheading{Full corner} + +Put $h=k-\ell$ and write +\[ + v(h):=\sum_i u_i h_i=n-m. +\] +The full corner is the range +\begin{equation*} + v(h)\le\frac n{32}. + \tag{7.26a} +\end{equation*} +We use the exact reverse recurrence (7.6) without replacing any ambient +falling factorial. + +First make the uniform smallness of the residual first moments explicit. For +any $0\le w\le n$ and every one of the four block sizes, +\[ + \frac{\mu_{u_i}(w)}{\mu_{u_i}(n)} + =\frac{(w)_{u_i}}{(n)_{u_i}} + \le\left(\frac wn\right)^{u_i}. +\] +Equations (2.2) and (2.8) give +$\mu_{u_i}(n)\le n^{6+o(1)}$ uniformly in the phase. Moreover, +$u_i=(2/\log 2+o(1))\log n$, and +$\log32=5\log2$. Consequently, uniformly for $w\le n/32$, +\begin{equation*} + \mu_{u_i}(w) + \le + n^{6+o(1)}32^{-u_i} + =n^{-4+o(1)}. + \tag{7.26} +\end{equation*} +In particular, there is one phase-independent threshold after which +\begin{equation*} + \mu_{u_i}(w)\le n^{-3} + \qquad + (w\le n/32,\ 2\le i\le5). + \tag{7.26b} +\end{equation*} +The relaxed exponent $-3$ leaves a fixed margin and is all that the recurrence +requires. + +Fix a final residual profile $h$ satisfying (7.26a), and expose its blocks in +any order. Let $a$ be the current residual profile and +$v(a)=\sum_i u_i a_i$. If the next block has type $i$, then +$a_i\eta n,\ n-m>n/32\},\\ + \mathcal F_n&:=\{\ell:n-m\le n/32\}. +\end{aligned} +\] +Indeed, if $\ell\in\mathcal F_n$, then +$m\ge31n/32>\eta n$, so the full corner cannot meet the empty corner; after +excluding those two cases, the two strict inequalities defining +$\mathcal C_n$ are automatic. Thus no boundary term is counted twice and no +subprofile is omitted. + +The three estimates proved above have the form +\[ +\begin{aligned} + 1&\le\sum_{\ell\in\mathcal E_n}D(\ell) + \le e^{\varepsilon_n^{\mathrm{empty}}},\\ + 0&\le\sum_{\ell\in\mathcal C_n}D(\ell) + \le\varepsilon_n^{\mathrm{central}},\\ + 0&\le\sum_{\ell\in\mathcal F_n}D(\ell) + \le\varepsilon_n^{\mathrm{full}}, +\end{aligned} +\] +where every error sequence is deterministic, phase-independent, and tends to +zero. The lower bound in the first line is the term $D(0)=1$. Adding the three +disjoint sums gives +\[ + 1 + \le + \sum_{0\le\ell_i\le k_i}D(\ell) + \le + e^{\varepsilon_n^{\mathrm{empty}}} + +\varepsilon_n^{\mathrm{central}} + +\varepsilon_n^{\mathrm{full}} + =1+o(1), +\] +which proves (7.7) with one eventuality threshold for the complete phase. diff --git a/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex index 16791e47..b680385c 100644 --- a/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex +++ b/625/arxiv/SECTION8_SELF_CONTAINED_V3.tex @@ -1,33 +1,31 @@ \section{Canonical high cells and endpoint transport} \label{sec:canonical-high-cells-v3} -This section bounds the contribution of all canonical high cells before any -residual local reward or cycle-space factor is charged. The proof has five -logically separate stages: - -\begin{enumerate} -\item sum the complete physical matching fiber for a fixed high-cell demand; -\item compare each actual multiplicity with its full-containment value; -\item pay the ambient falling-factorial loss once, after the fiber sum; -\item sum all admissible positive deficits by a finite product; -\item regroup the full references by endpoint table and transport them to the -partial-diagonal weights of Section~7. -\end{enumerate} - -No individual partial matching is assigned a preferred full completion. - -\subsection{Canonical support and exact aggregate weight} - -Let $U$ be the largest size in the fixed four-size profile and put +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. + +Section~7 has not subtracted or conditioned away overlaps containing common +whole classes. Instead, its weights provide a normalized one-sided reference +measure for the endpoint transport below. Every overlap matrix remains present +and is represented exactly once by its canonical high-cell skeleton. + +\subsection{The complete physical fiber} + +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 +33,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 +551,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 +579,21 @@ \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. All overlap matrices, including those containing whole common +classes, remain part of the exact conditional decomposition there. diff --git a/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex b/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex index c99c27bc..51c248a3 100644 --- a/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex +++ b/625/arxiv/SECTION9_SELF_CONTAINED_V3.tex @@ -1,27 +1,29 @@ \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. Section~7 has not removed any overlap from the exact +sum: its diagonal weights enter Section~8 only as a comparison measure for the +endpoint-table sum. -\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 -$r'_{ab}\le\lfloor U/2\rfloor$ and forbids any further pair in a cell of $M$. -Define +residual degrees; when $m_0=0$, this means the unique empty matching. 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 $\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} \mathcal A(M,j) := @@ -32,34 +34,56 @@ \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. To justify the word \emph{exact}, start with an overlap matrix $r$. +Its cells above $\lfloor U/2\rfloor$ determine one and only one matching $M$ +and multiplicity vector $j$. Removing the exposed pairs leaves one residual +matrix $r'$ satisfying $\mathcal E(M,j)$. Conversely, a feasible skeleton and +a residual matching satisfying $\mathcal E(M,j)$ reconstruct one overlap +matrix. The configuration-model cancellation proved in Section~8 factors its +probability and exposed local reward into $w_{\mathrm{hi}}(M,j)$ times the +residual law in \eqref{eq:residual-attachment-v3}; the remaining sign factor is +exactly $2^{\beta(M\cup H_{\mathrm{res}})}$. Thus no overlap is omitted and no +overlap is assigned to two skeletons. -\subsection{Local threshold activities} +The case $m_0=0$ is complete without introducing cell activities. The residual +matching is empty, every residual local factor is one, and +$H_{\mathrm{res}}=\varnothing$. Since $M$ is a matching, +$\beta(M)=0$, so +\begin{equation} + \mathcal A(M,j)=1 + \qquad(m_0=0). + \label{eq:zero-residual-attachment-v3} +\end{equation} +In all subsequent subsections we assume $m_0>0$. In view of +Proposition~\ref{prop:bare-high-skeleton-v3}, it remains to bound +$\mathcal A(M,j)$ uniformly in the positive-residual case. -For a residual cell $(a,b)$ outside $M$, put +\subsection{Threshold expansion and cell activities} + +For every row--column pair $(a,b)$, put \begin{equation} \theta_{ab}:= \frac{\mathrm e\,d_ad'_b}{m_0}. \label{eq:theta-v3} \end{equation} -Let +The intensity is defined on cells of $M$ as well as outside $M$; only the +activities will be suppressed on $M$. Let \[ \Delta_x:=g(x)-g(x-1), \qquad R:=\left\lfloor\frac U2\right\rfloor, \] -and define +and, for $(a,b)\notin M$, define \begin{equation} \lambda_{ab} := @@ -70,65 +94,109 @@ \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})$ supported outside $M$, 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; no independence between cells is asserted. + +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 +212,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 +255,85 @@ \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 outside $M$. +\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\theta + \le + \log_2\mathrm e+2\log_2U-\frac U3. +\] +For sufficiently large $U$, one has $R\ge3$ and $g(R)=2^{\binom R2-1}$. Hence +\[ +\begin{aligned} + \log_2\!\left(\frac{a_R}{\theta^2}\right) + &= + \binom R2-1+(R-2)\log_2\theta-\log_2(R!)\\ + &\le + \left(\frac{U^2}{8}+O(U)\right) + -\left(\frac{U^2}{6}+O(U)\right) + +O(U\log U)\\ + &= + -\frac{U^2}{24}+O(U\log U). +\end{aligned} +\] +The two quadratic terms come respectively from the local reward $g(R)$ and +from the factor $\theta^{R-2}$; the factorial term only improves the upper +bound. 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} + +Because $\theta_{ab}$ was defined for every pair, the cell intensities satisfy +the exact identity \[ \sum_{a,b}\theta_{ab}^2 = @@ -216,12 +347,13 @@ \subsection{The intrinsic residual regime} \qquad \sum_b(d'_b)^2\le Um_0. \] -Together with \eqref{eq:q-quadratic-v3}, this yields +On $M$ the activities are zero, while outside $M$ the preceding lemma applies. +Therefore \begin{equation} - \sum_{a,b}q_{ab}\le C_1U^2. + \sum_{e\in E_0}q_e\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 +362,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}. + m_0<2^{U/3}\le2^{\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,31 +397,35 @@ \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 \begin{cases} - \exp(CU^2),&2^U\le m_0^3,\\ - 2^{Um_0/2},&2^U>m_0^3. + 1,&m_0=0,\\ + \exp(CU^2),&m_0>0\text{ and }2^U\le m_0^3,\\ + 2^{Um_0/2},&m_0>0\text{ and }2^U>m_0^3. \end{cases} \] \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 +The zero-residual exponent is zero. Thus all three cases 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 +456,17 @@ \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. Adding the two deterministic logarithmic error +sequences gives the required $\Lambda_n$. 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. diff --git a/625/audits/CHROMATIC_LOWER_TAIL_CLOSURE_AUDIT_2026-08-06.md b/625/audits/CHROMATIC_LOWER_TAIL_CLOSURE_AUDIT_2026-08-06.md new file mode 100644 index 00000000..4729e80a --- /dev/null +++ b/625/audits/CHROMATIC_LOWER_TAIL_CLOSURE_AUDIT_2026-08-06.md @@ -0,0 +1,177 @@ +# Erdős 625 chromatic lower-tail closure audit + +**Date:** 2026-08-06 +**Branch:** `agent/625-referee-readable-tier-one-pass` +**Manuscript source:** `625/arxiv/SECTION4_CHROMATIC_LOWER_TAIL_V3.tex` +**Status:** complete candidate paper interface; exact Lean declaration and independent replay still required + +## Purpose + +The final gap theorem uses a deterministic integer threshold `k_chi^-(n)` for which + +```text +P(chi(G_n) > k_chi^-(n)) -> 1 +``` + +and whose distance from the ordinary first-moment root is negligible on the target scale `n/(log n)^3`. The former manuscript stated this conclusion correctly but compressed the decisive uniformity, exact-class-count, and event-direction steps into a short appeal to the profile variational lemma. + +The replacement Section 4 makes every one of those interfaces explicit. + +## Exact deterministic threshold + +The threshold is + +```text +k_chi^-(n) = floor(r_+(n)) - ceil(log n). +``` + +Thus + +```text +log n <= r_+(n)-k_chi^-(n) < log n+2. +``` + +In particular, + +```text +|k_chi^-(n)-r_+(n)| = o(n/(log n)^3). +``` + +No phase-dependent rounding convention or density-one subsequence is introduced. + +## Exact profile enumeration + +For a profile with `k_i` classes of size `alpha-i`, the expected number of unordered proper colorings is + +```text +n! / product_i(((alpha-i)!)^(k_i) k_i!) + * 2^(-sum_i k_i binom(alpha-i,2)). +``` + +The manuscript now explains the symmetry factors: + +- `n!` orders the vertices; +- each block factorial removes its internal ordering; +- `k_i!` removes the ordering of equal-size blocks; +- blocks of different sizes have different profile types, so there is no additional global `k!` factor. + +The profile sum therefore counts each unordered partition once. + +The profile-coordinate box has at most + +```text +(n+1)^(alpha+1) = exp(O((log n)^2)) +``` + +points. The two exact conservation laws only reduce this count. Applying the factorial estimate uniformly, including zero coordinates, gives + +```text +log E_{n,k,alpha+1} + <= L_+(n,k) + O((log n)^2). +``` + +## Uniform derivative corridor + +The key missing line was the verification that the complete interval from `k_chi^-` to `r_+` remains inside the derivative corridor. + +Writing `s(k)=n/k`, one has uniformly on this interval + +```text +k = Theta(n/log n), +s(k) = Theta(log n), +``` + +and hence + +```text +|s(k_chi^-)-s(r_+)| + <= sup n/k^2 * (r_+-k_chi^-) + = O((log n)^3/n) + = o(log log n/log n). +``` + +This is much smaller than the corridor width. Therefore the phase-uniform derivative estimate applies at every intermediate point: + +```text +dL_+(n,k)/dk >= c_* (log n)^2. +``` + +Since `L_+(n,r_+)=0`, the mean-value theorem yields + +```text +L_+(n,k_chi^-) <= -c_* (log n)^3. +``` + +The `O((log n)^2)` profile-enumeration error is absorbed with a fixed margin, producing one deterministic sequence + +```text +epsilon_n^prof = exp(-c_chi (log n)^3) -> 0. +``` + +## Removing the class-size cap + +Let + +```text +A_n = {alpha(G_n) <= alpha+1}. +``` + +The independence-number estimate supplies one deterministic phase-uniform sequence + +```text +P(A_n^c) <= epsilon_n^cap -> 0. +``` + +On `A_n`, every color class has size at most `alpha+1`. + +The first-moment variable counts colorings with exactly `k_chi^-` nonempty classes, whereas the event `chi(G_n)<=k_chi^-` initially gives at most that many classes. The manuscript now includes the exact refinement argument. If a proper coloring has `h 0. +``` + +Equivalently, + +```text +P(chi(G_n) > k_chi^-) -> 1. +``` + +The strict direction is the one used by the final event intersection. + +## What is now closed in the manuscript + +The replacement section contains a complete candidate proof of the theorem-facing chromatic lower-tail interface: + +1. one deterministic integer threshold; +2. the exact unordered profile count; +3. a phase-uniform profile-enumeration error; +4. verification that the full displacement interval lies in the derivative corridor; +5. a uniform `-Theta((log n)^3)` first-moment exponent; +6. the refinement from at most to exactly `k_chi^-` classes; +7. the strict probability event; +8. the required `o(n/(log n)^3)` location precision; +9. one set of eventuality thresholds valid through the complete phase and along the full sequence. + +## What remains open + +This audit does not promote E625-09 to `welded`. The following acceptance steps remain: + +1. freeze the exact Lean declaration using the same `r_+`, `k_chi^-`, class-size cap, and strict event direction; +2. bind the derivative corridor and all error sequences with the required uniform quantifiers; +3. independently check the manuscript proof line by line; +4. replay the declaration under the pinned Lean 4.31 toolchain with warnings fatal; +5. run the placeholder, forbidden-shortcut, and axiom gates; +6. import the result into the theorem-facing root and replay the final adapter on the same integrated commit. + +Until those steps pass, E625-09 remains `needs review` and the manuscript remains fail-closed. diff --git a/625/audits/MATHEMATICAL_CLARITY_AND_CLOSURE_PASS_2026-08-06.md b/625/audits/MATHEMATICAL_CLARITY_AND_CLOSURE_PASS_2026-08-06.md new file mode 100644 index 00000000..02bf7674 --- /dev/null +++ b/625/audits/MATHEMATICAL_CLARITY_AND_CLOSURE_PASS_2026-08-06.md @@ -0,0 +1,312 @@ +# Erdős 625 mathematical clarity and closure pass + +**Date:** 2026-08-06 +**Branch:** `agent/625-referee-readable-tier-one-pass` +**Scope:** Sections 5, 7, 8, 9, final constant ledger, and manuscript validation +**Status:** fail-closed; this audit does not promote the main theorem + +## Executive assessment + +This pass addresses six places where a referee could reasonably object that a correct idea had not yet been expressed at the theorem-facing level: + +1. Section 5 moved from the finite target mean at the unrestricted root to the phase center inside an unexplained `o(1)`; +2. the empty partial-diagonal corner did not display the uniform comparison between the intermediate and ambient first moments; +3. the central partial-diagonal proof compressed the uniform Stirling, entropy, and residual-fraction errors into prose; +4. the full partial-diagonal corner did not state why every reverse-recurrence step remains inside the small residual range, and the three ranges were not assembled as a literal partition; +5. Section 9 defined residual activities by dividing by the residual mass before separating the zero-residual case; +6. the final coefficient relied on a strict phase certificate without exhibiting a fixed margin capable of absorbing the deterministic `o(1)` error. + +All six interfaces are now explicit. Section 7 now contains a complete candidate paper proof of its empty, central, and full ranges and their normalized assembly. This is a material proof-closure improvement, but it is not yet independent verification or a welded Lean theorem. + +## 1. Finite-target transport in the signed root separation + +The root comparison is isolated in +`625/arxiv/SECTION5_ROOT_TRANSPORT_V3.tex`. At the unrestricted root, the manuscript first records the exact finite identity + +```text +Phi_n(r_+) + = r_+ {log 2 - D_{4,n}(T_+(n))}, +T_+(n) = alpha - n/r_+(n). +``` + +No limiting functional is substituted in this equality. The passage to the phase center is decomposed into the uniform convergence of the two finite dual values on `K_*` and the displacement + +```text +T_+(n)-T_0 = O(log log n/log n). +``` + +The limiting dual derivative is `F_S'(T)=-lambda_S(T)`, and the tilts are uniformly bounded on `K_*`. Hence the limiting dual values are uniformly Lipschitz. The manuscript defines one deterministic error sequence + +```text +omega_n^root + = sup |F_{n,S+}-F_{S+}| + + sup |F_{n,S4}-F_{S4}| + + C |T_+(n)-T_0|, +``` + +proves `omega_n^root -> 0` uniformly in the phase, and obtains + +```text +Phi_n(r_+) + = r_+ {log 2 - D_4(delta) + O(omega_n^root)}. +``` + +The positive entropy margin and positive corridor derivative then prove +`r_4^co < r_+`, so the orientation and nonemptiness of the subsequent mean-value interval are explicit. + +## 2. Empty partial-diagonal corner + +The empty corner is isolated in +`625/arxiv/SECTION7_EMPTY_CORNER_V3.tex`. For an intermediate selected mass `m'` and block size `u_i`, the exact comparison is + +```text +mu_{u_i}(n)/mu_{u_i}(n-m') + = (n)_{u_i}/(n-m')_{u_i}. +``` + +In the range `m' <= eta n`, phase-uniform control of `u_i=O(log n)` gives + +```text +mu_{u_i}(n)/mu_{u_i}(n-m') + <= (1-2 eta)^(-u_i) + <= (log n)^(3/8). +``` + +The exact one-block recurrence may therefore be iterated in any order. The resulting product is summed by enlarging to the complete nonnegative four-dimensional lattice. The exponent is + +```text +(log n)^(3/8) Xi_empty + = O((log n)^-(2/log 2-7/8)), +``` + +and the explicit inequality + +```text +2/log 2 - 7/8 > 111/56 > 0 +``` + +leaves a fixed power margin. Thus the range contributes + +```text +1 <= sum_empty D(ell) <= exp(epsilon_n^empty) = 1+o(1) +``` + +for one deterministic phase-independent sequence `epsilon_n^empty -> 0`. + +## 3. Central partial-diagonal range + +The central argument is isolated in +`625/arxiv/SECTION7_CENTRAL_EXTRACTION_V3.tex`. + +### Uniform Stirling and entropy errors + +For every nonnegative factorial argument, + +```text +log(t!) = t log t - t + sigma(t), +|sigma(t)| <= C_S log(t+2). +``` + +Only a fixed number of factorials occurs, so the total error is `O(log n)` uniformly, including zero coordinates. The exact rounded profile has all four proportions uniformly bounded below, and the coordinatewise entropy term is bounded by `C_H y log(e/y)`. The four-coordinate entropy inequality then gives + +```text +sum_i y_i log(e/y_i) <= Y log(4e/Y). +``` + +### Affine phase and residual-fraction transport + +Exact subtraction gives + +```text +E_{i+1}-E_i = -(log 2) alpha/2 + O(1). +``` + +Averaging the affine correction and using only the upper bound supplied by the positive complete first moment yields + +```text +sum_i y_i E_i + <= ((log 2) alpha/2)(T Y-I)+O(Y). +``` + +The proof also displays + +```text +rho-R = (I-TY)/(alpha-T), +|I-TY| <= 3Y, +``` + +and derives the missing bridge + +```text +n rho log rho + = k_co alpha R log R + O(k_co Y). +``` + +### Rate negativity and deterministic sum + +The two four-deficit structural inequalities combine to + +```text +I_r-TR <= 3R(1-R). +``` + +Together with `log R <= 2(R-1)/(R+1)`, this gives the two explicit margins + +```text +1/64 <= R <= 3/4: Phi_T <= -(13/8960)(1-R), +3/4 <= R <= 1: Phi_T <= -(1/20)(1-R). +``` + +The proof defines `epsilon_n^diag -> 0`, obtains + +```text +D(ell) <= exp(-c k_co log log n), +``` + +and names the total deterministic central error + +```text +epsilon_n^central + = (k_co+1)^4 exp(-c k_co log log n) -> 0. +``` + +Every threshold is independent of the phase. + +## 4. Full partial-diagonal corner and exact range assembly + +The full corner and assembly are isolated in +`625/arxiv/SECTION7_FULL_CORNER_V3.tex`. +For residual vertex mass `w <= n/32`, the exact first-moment ratio gives + +```text +mu_{u_i}(w)/mu_{u_i}(n) + <= (w/n)^(u_i), +``` + +and the phase expansion yields the uniform envelope + +```text +mu_{u_i}(w) <= n^(-4+o(1)) <= n^-3. +``` + +If a residual profile `h` is exposed in any order, every next step satisfies + +```text +v(a)+u_i <= v(h) <= n/32. +``` + +The exact reverse recurrence is therefore at most `2n^-2<1` at every step. Consequently `B(h)<=1`, and the positive signed first-moment margin gives + +```text +D(k-h) <= exp(-c_Z k_co). +``` + +After summing the polynomial number of residual profiles, one obtains a deterministic phase-independent sequence `epsilon_n^full -> 0`. + +For all sufficiently large `n`, `eta<31/32`, and the coordinate box is the disjoint union + +```text +E_n = {m <= eta n}, +C_n = {m > eta n and n-m > n/32}, +F_n = {n-m <= n/32}. +``` + +The full and empty ranges cannot meet because the full range has `m>=31n/32`. The remaining profiles satisfy the two strict central inequalities. Hence no subprofile is omitted and no boundary contribution is counted twice. Adding the three deterministic estimates gives + +```text +1 <= sum_ell D(ell) + <= exp(epsilon_n^empty) + + epsilon_n^central + + epsilon_n^full + = 1+o(1), +``` + +with one eventuality threshold for the complete phase. + +### Status consequence + +The manuscript now contains a complete candidate proof of E625-11A--D, conditional on the exact midpoint-profile and positive-first-moment inputs from E625-10. The node remains `needs review`: each standalone source must still receive independent line-by-line mathematical verification, be frozen as an exact theorem interface, and be replayed in Lean against the actual midpoint profile. The finite scalar and reindexing lemmas already welded privately do not by themselves perform this promotion. + +## 5. Section 7--8 accounting interface + +Section 7 does not remove, condition away, or subtract overlaps containing common whole classes. Its partial-diagonal weights form a one-sided normalized reference sum. Section 8 dominates endpoint-table weights by this reference sum through the square-free transport inequality. + +The manuscript states this explicitly at the start and end of Section 8 and defines + +```text +w_hi(P,j) := w(P,j), +``` + +so the bare high-skeleton weight in Section 8 is visibly the same object used in the exact conditional decomposition of Section 9. The one-sided reference vector is restricted to its actual finite coordinate box. + +## 6. Zero residual mass and exact conditional decomposition + +The activity `theta_ab=e d_a d'_b/m_0` is meaningful only for `m_0>0`. Section 9 now handles `m_0=0` first: the residual matching is uniquely empty, all residual local factors are one, and the exposed high cells form a matching with cycle rank zero. Therefore + +```text +A(M,j)=1 when m_0=0. +``` + +The exact overlap decomposition is justified by the two-way reconstruction + +```text +overlap matrix + <-> canonical high-cell matching and multiplicities + + capped residual matching with no return to exposed cells. +``` + +This makes uniqueness and absence of double counting explicit. The prescribed-cell estimate is a joint factorial-moment inequality; no independence between residual cells is asserted. + +## 7. Fixed slack in the final constant + +The exact rational checker now verifies + +```text +L(49q/20) < 2629/10000, +H(29q/10) < 37/2500, +L(29q/10) < 329/2500, +H(83q/20) < 357/2500. +``` + +Both tilt ranges satisfy `L(lambda_4)+H(lambda_4)<2777/10000`, giving + +```text +A_4(delta) > log(20000/12777). +``` + +The fixed slack over the displayed theorem constant is + +```text +log(20000/12777) + = log(1000/639) + log(12780/12777). +``` + +The final proof explicitly takes `n` large enough that the deterministic probability error is smaller than the coefficient corresponding to this positive slack. The theorem coefficient is unchanged. + +## 8. Midpoint and PDF consistency + +The total class count is fixed as + +```text +k_co = ceil((r_4^co+r_+)/2). +``` + +The tangent correction changes only the four type multiplicities and preserves both conservation laws; it does not add another bounded correction to `k_co`. + +Manually tagged displays are placed in unnumbered AMS environments. The PDF workflow fails on duplicate Hyperref destinations in addition to unresolved references, unresolved citations, and material overfull boxes. + +The fail-closed checker and workflow now require and archive the standalone Section 5 source and all three Section 7 range sources, together with the exact numerical ledgers and representative rendered pages. + +## Remaining proof-closure boundary + +This pass does not close the following nodes: + +1. the exact concrete phase center and slope package; +2. the full-sequence chromatic lower tail; +3. the complete signed four-size first-moment assembly; +4. independent mathematical verification and exact Lean replay of the complete candidate E625-11 partial-diagonal package; +5. the complete high-skeleton quotient and endpoint asymptotic theorem; +6. the global residual attachment and normalized-second-moment theorem; +7. the final integrated theorem-facing replay. + +Accordingly, the publication switch must remain disabled and PR #58 must remain a draft. diff --git a/625/audits/PARTIAL_DIAGONAL_CLOSURE_AUDIT_2026-08-05.md b/625/audits/PARTIAL_DIAGONAL_CLOSURE_AUDIT_2026-08-05.md new file mode 100644 index 00000000..099f6a59 --- /dev/null +++ b/625/audits/PARTIAL_DIAGONAL_CLOSURE_AUDIT_2026-08-05.md @@ -0,0 +1,227 @@ +# Erdős 625 partial-diagonal closure audit + +**Date:** 2026-08-05 +**Scope:** E625-11, exact common-subprofile contribution +**Branch:** `agent/625-referee-readable-tier-one-pass` +**Status:** the scalar finite-dimensional rate core is closed; the full asymptotic package is not + +## Verdict + +The principal finite-dimensional obstruction in the central partial-diagonal range is no longer an open proof-design problem. The public Lean root contains both: + +1. the scalar theorem + + ```text + partialDiagonalRate T R Ir <= -(1-R)/5000, + ``` + + under the manuscript structural inequalities; and +2. the four-deficit bridge deriving those inequalities from the actual support `{2,3,4,5}`. + +The manuscript now uses a direct analytic proof of the same margin. It combines the two structural inequalities before splitting the scalar interval, so it no longer depends on the former `47/100` endpoint or on a separate numerical certificate for `log(100/47)`. + +This closes the **scalar geometry** of E625-11. It does not close E625-11 as a whole. The remaining work is the uniform asymptotic transport from exact factorial expressions to that scalar rate, together with the two singular corners and their exhaustive assembly. + +## 1. Exact pieces already present + +### 1.1 Scalar rate theorem + +`PartialDiagonalRateBound.lean` proves the following finite deterministic statement. If + +```text +1/64 <= R <= 1, +T <= 4, +Ir - T R <= (5-T)R, +Ir - T R <= (T-2)(1-R), +``` + +then + +```text +R log R + (log 2)/2 (Ir-TR) <= -(1-R)/5000. +``` + +The endpoint `R=1` is included. No asymptotic notation occurs in this theorem. + +### 1.2 Four-deficit structural bridge + +`PartialDiagonalFourDeficitRateBridge.lean` derives the two structural inequalities from the actual four-coordinate profile, nonnegativity, coordinatewise domination, total mass one, and mean `T`. It therefore rules out a hidden replacement of the four-size geometry by an assumed scalar surrogate. + +### 1.3 Empty-corner finite recurrence + +`PartialDiagonalMidpointActivityBridge.lean` proves an exact cutoff-activity estimate for the empty corner and bounds the finite cutoff sum by + +```text +exp(sum_i muCutoffActivity_i). +``` + +The denominator retains the exact residual first moment `mu(n-massCap,u_i)`. No invalid replacement of `(n)_m` by `n^m` is used. + +### 1.4 Full-corner finite reindexing + +`FullCornerSumReindexing.lean` proves the exact involutive reindexing by complementary residual profiles under the full-mass hypothesis. This isolates the remaining full-corner task as an estimate on the reindexed local ratios divided by the complete signed first moment. + +## 2. Cleaner scalar proof now used in the manuscript + +Put + +```text +Y = 1-R, +q = log 2. +``` + +The two structural inequalities are + +```text +Ir-TR <= (5-T)R, +Ir-TR <= (T-2)Y. +``` + +Multiplying the first by `Y`, the second by `R`, and adding gives the uniform combined bound + +```text +Ir-TR <= 3 R Y. (2.1) +``` + +For `0= 0, +``` + +with `x=(1-R)/R`. + +The positive atanh series gives + +```text +2/3 < q < 7/10. (2.3) +``` + +### Range I: `1/64 <= R <= 3/4` + +Equations (2.1)--(2.3) yield + +```text +Phi_T + <= -2R/(1+R) Y + 21/20 RY + = -[2/(1+R)-21/20] RY. +``` + +Since `2/(1+R) >= 8/7`, + +```text +Phi_T <= -(13/140) RY + <= -(13/8960)Y + <= -Y/5000. +``` + +### Range II: `3/4 <= R <= 1` + +The phase corridor gives `T <= 1+2/q < 4`. Hence the second structural inequality gives `Ir-TR <= 2Y`. Together with `log R <= R-1=-Y`, + +```text +Phi_T <= -RY + qY + = (q-R)Y + <= -Y/20 + <= -Y/5000. +``` + +This proof covers the complete scalar interval without an endpoint grid or a convexity reduction to `R=47/100`. + +## 3. Exact checker and its boundary + +`check_partial_diagonal_rate_v3.py` verifies, with `Fraction` arithmetic only, + +```text +56/81 > 2/3, +25/36 < 7/10, +8/7 - 21/20 = 13/140, +(13/140)(1/64) = 13/8960 > 1/5000, +3/4 - 7/10 = 1/20 > 1/5000. +``` + +The checker is a reproducible ledger for the rational constants. It does **not** prove: + +- the logarithmic inequality (2.2); +- the four-deficit structural reduction (2.1); +- the uniform Stirling extraction; +- the phase-to-midpoint hypotheses; +- the empty/central/full partition of the sum; +- the final asymptotic statement. + +The analytic inequalities are proved in the manuscript and the finite scalar/structural core is mirrored in Lean. The asymptotic bridges below remain separate obligations. + +## 4. Remaining E625-11 interfaces + +### E625-11A — empty-corner asymptotic bridge + +The finite activity theorem is present. What remains is a phase-uniform theorem showing that, for the actual midpoint profile and manuscript cutoff, + +```text +sum_i muCutoffActivity_i = o(1) +``` + +or the exact stronger bound used in the paper. This requires the uniform adjacent-size estimates for `mu_s(n)`, the class-count asymptotics, and control of the cutoff shift in the residual vertex count. + +### E625-11B — uniform central rate extraction + +The scalar theorem is present. What remains is one exact theorem converting the finite factorial expression `A_ell` into + +```text +log A_ell + <= K alpha Phi_T(z) + + C K Y log(e/Y) + + C log n +``` + +with one absolute `C`, uniformly over: + +- the complete phase corridor; +- every admissible integer four-subprofile in the central range; +- coordinates that may vanish; +- sequences approaching either phase endpoint. + +This theorem must also prove the exact relation between the residual vertex fraction and `R`, and the implication from the central residual-mass cutoff to `R>=1/64`. + +### E625-11C — full-corner asymptotic bridge + +The complementary-profile reindexing is present. What remains is a uniform estimate showing that every allowed residual-block increment is at most one in the full-corner range, followed by division by the actual complete signed first moment. The proof must consume the phase-uniform exponential margin supplied by E625-10, not a merely positive first moment. + +### E625-11D — exhaustive assembly + +The final theorem must show that the three ranges are pairwise disjoint and exhaustive under the exact integer cutoffs, and then combine them into the normalized complete partial-diagonal bound with one deterministic error sequence. The boundary cases must be assigned explicitly; no mass vector may be omitted or counted twice. + +## 5. Refined status ledger + +| Component | Finite deterministic core | Uniform asymptotic application | Status | +|---|---:|---:|---| +| Scalar four-deficit geometry | proved in Lean and manuscript | not applicable | **welded** | +| Empty-corner recurrence/activity | proved in Lean | still required | **running / needs review** | +| Central scalar negativity | proved in Lean and manuscript | Stirling/range bridge still required | **running / needs review** | +| Full-corner reindexing | proved in Lean | local-ratio and first-moment bridge still required | **running / needs review** | +| Three-range assembly | finite partition not yet frozen theorem-facing | still required | **blocked** | +| E625-11 as a whole | incomplete | incomplete | **not closed** | + +## 6. Acceptance test for promoting E625-11 + +E625-11 may be marked welded only after one integrated commit contains: + +1. the exact midpoint-profile hypotheses from E625-10; +2. a uniform empty-corner activity asymptotic; +3. the uniform central Stirling/rate extraction; +4. the full-corner local-ratio asymptotic; +5. a disjoint and exhaustive range partition; +6. the final normalized partial-diagonal theorem; +7. Lean 4.31 compilation with warnings fatal, placeholder and shortcut scans, axiom audit, and root replay; +8. an independent mathematical review of every asymptotic implication. + +Until then, the correct statement is: + +> The scalar partial-diagonal rate obstruction is closed. The complete partial-diagonal asymptotic package remains open because its uniform finite-to-asymptotic bridges and global range assembly have not yet been independently welded. diff --git a/625/audits/PROOF_CLOSURE_CONTRACTS_2026-08-05.md b/625/audits/PROOF_CLOSURE_CONTRACTS_2026-08-05.md new file mode 100644 index 00000000..4cf8b5e7 --- /dev/null +++ b/625/audits/PROOF_CLOSURE_CONTRACTS_2026-08-05.md @@ -0,0 +1,255 @@ +# Erdős 625 proof-closure contracts + +**Date:** 2026-08-05 +**Scope:** public manuscript and theorem-facing interface +**Branch:** `agent/625-referee-readable-tier-one-pass` +**Status:** fail-closed planning document; no unresolved node is promoted by this file + +## Purpose + +The project has moved from proof discovery to proof closure, but the remaining work is not merely transcription into Lean. This document fixes the interfaces that must be reviewed before any global theorem can be described as closed. It separates: + +1. finite deterministic identities already supported by exact proofs or checkers; +2. analytic statements that still require uniform asymptotic proofs; +3. global assembly statements that must be replayed on one dependency-consistent commit. + +The contracts below are theorem-facing specifications. An implementation is accepted only if it preserves the manuscript definitions, quantifier order, constants, summation domains, and normalization exactly. + +## Global acceptance conventions + +Every asymptotic contract must satisfy all of the following. + +- **One deterministic error sequence.** A statement uniform in the phase must use one error sequence for the entire phase interval, including integer sequences approaching either endpoint. +- **One eventuality threshold.** Any `eventually` statement must have a threshold independent of the phase and of the admissible profile within the stated corridor. +- **Exact integer profiles.** Conservation of the number of classes and the number of vertices must hold for the actual rounded integer profile. A continuous optimizer is not an acceptable substitute. +- **No hidden support change.** The four-size support, endpoint alphabets, selected cells, and residual families must be the manuscript objects, not enlarged or weakened surrogates. +- **No duplicated charge.** A factor paid in the high-skeleton quotient may not be paid again in the residual attachment sum, and conversely. +- **Normalized outputs.** Second-moment statements must expose the normalization by the square of the first moment rather than absorb it into an unnamed constant. +- **Fail-closed evidence.** Numerical experiments, exact rational checkers, isolated Lean lemmas, and stale branch builds are supporting evidence only. None closes a node without exact-statement review and integrated replay. + +## Dependency spine + +```text +E625-08 concrete phase center and slope + ├── E625-09 chromatic lower tail + └── E625-10 signed four-size first moment + +E625-10 ── E625-11A/B/C/D complete partial-diagonal package +E625-10 ── E625-12 high-skeleton quotient and endpoint transport +E625-12 ── E625-13 global residual attachment and normalized second moment + +E625-09 + E625-10 + E625-11D + E625-13 + ── E625-14 concrete final instantiation +``` + +## E625-08 — concrete phase center and slope package + +### Inputs + +The exact finite-`n` phase parameter, the unrestricted coloring objective, the four-support signed objective, and the root corridor already used in Sections 1–5. + +### Required output + +A single theorem-facing package must provide, uniformly over the complete phase: + +- existence and uniqueness of the ordinary root `r_+(n)` and the signed four-support root `r_4^co(n)` in the stated corridor; +- the concrete center estimates needed to locate both roots; +- the derivative estimate on every point between the two roots, with a uniform remainder of order at most `O((log n)(log log n))` relative to the leading `2(log n)^2/log 2` term; +- the phase-resolved separation + + ```text + r_+(n) - r_4^co(n) + = [((log 2)^2/4) A_4(delta_n) + o(1)] n/(log n)^3, + ``` + + with one deterministic `o(1)` sequence; +- the concrete corridor and feasibility facts consumed by tangent rounding and by the chromatic lower-tail theorem. + +### Rejection conditions + +The node remains open if the proof assumes a fixed interior phase, changes the support at an endpoint, proves only pointwise convergence, or exports a derivative bound that is too weak to retain the `n/(log n)^3` separation. + +## E625-09 — chromatic lower-tail theorem + +### Required output + +There must be a deterministic integer sequence `k_chi^-(n)` such that + +```text +P(chi(G_n) > k_chi^-(n)) -> 1 +``` + +and + +```text +|k_chi^-(n) - r_+(n)| = o(n/(log n)^3) +``` + +uniformly across the phase. The theorem must use the same ordinary root and phase convention as E625-08. + +### Required audit points + +- the lower-tail event is strict in the same direction used by the final union bound; +- all profile truncations are valid uniformly at both phase endpoints; +- integer rounding errors are absorbed at `o(n/(log n)^3)` scale; +- no density-one restriction on the integers remains. + +## E625-10 — signed four-size first-moment assembly + +### Required output + +For the tangent-rounded midpoint profile, one theorem-facing chain must establish: + +- an integer class count + + ```text + k_co(n) = ceil((r_4^co(n) + r_+(n))/2) + b_n, + |b_n| <= C, + ``` + + for an absolute constant `C`; +- nonnegative integer multiplicities on the four prescribed class sizes; +- exact conservation of the class count and the vertex count; +- the uniform finite-support entropy certificate and the resulting root displacement; +- a positive exponential first-moment margin of the form + + ```text + log Z_sgn(k_co) >= c K + ``` + + for one phase-independent `c > 0`, where `K` is the number of classes; +- the retained midpoint gap + + ```text + r_+(n) - k_co(n) + = [((log 2)^2/8) A_4(delta_n) + o(1)] n/(log n)^3. + ``` + +### Rejection conditions + +The node is not closed by the limiting optimizer alone, by an `O(1)` correction whose conservation identities are not checked, or by a positive first moment without a phase-uniform exponential margin. + +## E625-11 — complete partial-diagonal package + +The existing exact identities, the scalar rate lemma, the four-deficit structural bridge, the full-corner reindexing, and the rational endpoint checker are ingredients. They do not by themselves prove the complete partial-diagonal sum. + +### E625-11A — empty corner + +Freeze the exact empty-corner range from Section 7 and prove that its normalized contribution has the manuscript bound, uniformly in the phase. The proof must retain the exact falling factorials in the range where replacing `(n)_m` by `n^m` is not uniform. + +### E625-11B — central Stirling and rate theorem + +For every admissible four-coordinate subprofile in the central range, prove the uniform extraction + +```text +log A_ell + <= K alpha Phi_T(z) + C K Y log(e/Y) + C log n +``` + +with one absolute `C`, followed by the structural reduction to + +```text +Phi_T(z) <= -(1-R)/5000 +``` + +on the complete stated range. The theorem must explicitly include: + +- the relation between the residual vertex fraction and `R`; +- the lower bound that places `R` in the scalar-rate domain; +- the two structural endpoint inequalities; +- the convexity argument on both subintervals; +- uniform control of every Stirling and entropy remainder. + +The exact checker now verifies the rational endpoint arithmetic only. Its success is not evidence for the omitted convexity, range-reduction, or uniform-error steps. + +### E625-11C — full corner + +Use the exact residual reindexing and local ratio bounds to prove the full-corner sum with the same first-moment normalization as the manuscript. The range must meet E625-11B without a gap or overlap ambiguity. + +### E625-11D — partial-diagonal assembly + +Prove that the empty, central, and full ranges are disjoint and exhaustive and combine their estimates into the complete partial-diagonal theorem consumed by the normalized second moment. The final output must be uniform in the phase and must state its deterministic error sequence explicitly. + +## E625-12 — skeleton quotient and endpoint asymptotic assembly + +### Already validated finite core + +The completion-free physical-fiber factorization, exact one-cell deficit ratio, single ambient falling-factorial charge, optional-deficit product, weighted regrouping by realized endpoint table, and realized-table deficit product have substantial exact support. + +### Required remaining output + +A global theorem must combine those finite identities with the concrete phase estimates to bound the complete high-skeleton quotient over the manuscript summation domain. It must include: + +- injective encoding or an exactly quantified multiplicity bound; +- endpoint-table feasibility and realization conditions; +- the phase-uniform common-charge estimate; +- the exact location where the single ambient loss is paid; +- the asymptotic summation over all admissible skeletons; +- an output in the normalization required by E625-13. + +A random replay over feasible endpoint tables is adversarial evidence only; the theorem must cover every feasible table. + +## E625-13 — global attachment and normalized second moment + +### Required output + +The global attachment theorem must combine the high-skeleton quotient with the conditioned residual law and the two residual regimes. It must derive, for the actual midpoint profile, + +```text +E[X_n^2] / E[X_n]^2 <= exp(Lambda_n), +Lambda_n = o(n/(log n)^4), +``` + +with one deterministic error sequence uniform in the phase. + +The proof must expose the chain + +```text +threshold expansion + -> exact restriction-product inequality + -> exp(2 sum q_ab) + -> intrinsic/complementary residual split + -> global summation. +``` + +It must also show explicitly, at the upper endpoint of the quadratic-activity estimate, how the `U^2/8` contribution from the reward and the `-U^2/6` contribution from the activity combine to `-U^2/24`, up to `O(U log U)`. + +### Rejection conditions + +The node remains open if it assumes independence between residual cells, invokes the old cycle/walk route without proving equivalence, hides a skeleton multiplicity in the residual constant, or proves only fixed-phase smallness. + +## E625-14 — concrete final instantiation + +This is an adapter, not a place to introduce new analytic estimates. It may be promoted only after E625-08 through E625-13 are closed on the same commit. + +Its output must instantiate the already-welded rare-seed amplifier and event assembly to prove + +```text +P( + chi(G_n) - zeta(G_n) + >= ((log 2)^2/8) log(1000/639) n/(log n)^3 +) -> 1. +``` + +The final replay must verify: + +- the exact coefficient ledger; +- the strict uniform entropy margin; +- the seed exponent required by amplification; +- the `o(n/(log n)^3)` amplification loss; +- the direction of both final events; +- the union bound without an independence assumption; +- the complement corollary, separately from the main theorem. + +## Promotion rule + +A node may move from `needs-review` to `running` only after its exact theorem statement, constants, uniformity quantifiers, dependencies, and manuscript citation are frozen. It may move from `running` to `welded` only after: + +1. isolated Lean 4.31 compilation with warnings fatal; +2. forbidden-shortcut and placeholder scans; +3. axiom audit; +4. import into the canonical theorem-facing root; +5. root replay on the integrated commit; +6. independent mathematical review of the paper argument corresponding to the declaration. + +Until E625-14 passes this rule, `\ErdosProofClosedfalse` is mandatory and the manuscript remains a conditional verification draft. 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 00000000..be4da202 --- /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. diff --git a/625/experiments/check_constant_ledger_v3.py b/625/experiments/check_constant_ledger_v3.py new file mode 100644 index 00000000..33c2ea32 --- /dev/null +++ b/625/experiments/check_constant_ledger_v3.py @@ -0,0 +1,183 @@ +#!/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 + +# These slightly sharper rational cutoffs leave a visible fixed margin in the +# final theorem rather than relying on an unspecified strict inequality. +L49_MAX = Fraction(2629, 10000) +H58_MAX = Fraction(37, 2500) +L58_MAX = Fraction(329, 2500) +H83_MAX = Fraction(357, 2500) +UNIFORM_OMITTED_MAX = Fraction(2777, 10000) +STRONG_RATIO = Fraction(20000, 12777) +TARGET_RATIO = Fraction(1000, 639) +SLACK_RATIO = Fraction(12780, 12777) + + +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 < L49_MAX, + "L(49 log 2 / 20) sharpened certificate failed", + ) + require( + h58_hi < H58_MAX, + "H(29 log 2 / 10) sharpened certificate failed", + ) + require( + l58_hi < L58_MAX, + "L(29 log 2 / 10) sharpened certificate failed", + ) + require( + h83_hi < H83_MAX, + "H(83 log 2 / 20) sharpened certificate failed", + ) + + first_split = L49_MAX + H58_MAX + second_split = L58_MAX + H83_MAX + require( + first_split == UNIFORM_OMITTED_MAX, + "first split ledger failed", + ) + require( + second_split < UNIFORM_OMITTED_MAX, + "second split ledger failed", + ) + require( + 1 + UNIFORM_OMITTED_MAX == Fraction(12777, 10000), + "partition-ratio ledger failed", + ) + require( + Fraction(2, 1 + UNIFORM_OMITTED_MAX) == STRONG_RATIO, + "strong entropy-ratio ledger failed", + ) + require( + STRONG_RATIO / TARGET_RATIO == SLACK_RATIO > 1, + "fixed final-constant slack 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}") + print(f" uniform omitted-mass cap: {UNIFORM_OMITTED_MAX}") + print(f" strong entropy ratio: {STRONG_RATIO}") + print(f" fixed slack ratio over target: {SLACK_RATIO}") + + +if __name__ == "__main__": + main() diff --git a/625/experiments/check_generator_regexes_v3.py b/625/experiments/check_generator_regexes_v3.py new file mode 100644 index 00000000..5e19f1ff --- /dev/null +++ b/625/experiments/check_generator_regexes_v3.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Statically validate literal regular expressions in the manuscript generator. + +`py_compile` does not compile regex patterns or parse replacement templates. +This checker walks the generator AST, compiles every literal `re.sub` pattern, +and asks the regex engine to parse each literal replacement template. Callable +replacements are deliberately accepted because their return values are literal +text rather than replacement-language programs. +""" + +from __future__ import annotations + +import ast +import re +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[1] +GENERATOR = ROOT / "scripts" / "build_self_contained_ams_v3.py" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def is_re_sub(node: ast.Call) -> bool: + return ( + isinstance(node.func, ast.Attribute) + and isinstance(node.func.value, ast.Name) + and node.func.value.id == "re" + and node.func.attr == "sub" + ) + + +def main() -> None: + require(GENERATOR.is_file(), f"missing generator: {GENERATOR}") + source = GENERATOR.read_text(encoding="utf-8") + tree = ast.parse(source, filename=str(GENERATOR)) + + calls = 0 + literal_patterns = 0 + literal_replacements = 0 + callable_replacements = 0 + + for node in ast.walk(tree): + if not isinstance(node, ast.Call) or not is_re_sub(node): + continue + calls += 1 + require(len(node.args) >= 2, f"line {node.lineno}: re.sub lacks arguments") + + try: + pattern = ast.literal_eval(node.args[0]) + except (ValueError, TypeError, SyntaxError) as exc: + raise RuntimeError( + f"line {node.lineno}: re.sub pattern is not a static literal" + ) from exc + require(isinstance(pattern, str), f"line {node.lineno}: non-string pattern") + try: + compiled = re.compile(pattern) + except re.error as exc: + raise RuntimeError( + f"line {node.lineno}: malformed regex pattern: {exc}" + ) from exc + literal_patterns += 1 + + replacement_node = node.args[1] + try: + replacement = ast.literal_eval(replacement_node) + except (ValueError, TypeError, SyntaxError): + require( + isinstance(replacement_node, (ast.Lambda, ast.Name)), + f"line {node.lineno}: replacement must be literal or callable", + ) + callable_replacements += 1 + continue + + require( + isinstance(replacement, str), + f"line {node.lineno}: literal replacement is not a string", + ) + try: + # The engine parses the replacement template even when the subject + # does not match, so this catches invalid escapes such as `\lambda`. + compiled.sub(replacement, "") + except re.error as exc: + raise RuntimeError( + f"line {node.lineno}: malformed replacement template: {exc}" + ) from exc + literal_replacements += 1 + + require(calls >= 15, f"unexpectedly few re.sub calls: {calls}") + require(calls == literal_patterns, "not every re.sub pattern was checked") + print("ERDOS 625 GENERATOR REGEX CHECK: PASS") + print(f" re.sub calls: {calls}") + print(f" literal replacement templates: {literal_replacements}") + print(f" callable replacements: {callable_replacements}") + + +if __name__ == "__main__": + main() 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 00000000..91d489f1 --- /dev/null +++ b/625/experiments/check_partial_diagonal_rate_v3.py @@ -0,0 +1,70 @@ +#!/usr/bin/env python3 +"""Exact rational ledger for the partial-diagonal scalar rate split. + +This script checks only the finite rational inequalities used after the +analytic logarithmic and four-deficit structural reductions. It does not +prove those reductions, the uniform Stirling estimate, or the final +empty/central/full-corner assembly. +""" + +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). + # The first two positive terms give the lower certificate. Bounding every + # denominator in the tail m >= 1 below by 3 gives the upper certificate. + q_lower = 2 * (Fraction(1, 3) + Fraction(1, 81)) + q_upper = 2 * (Fraction(1, 3) + Fraction(1, 72)) + require(q_lower == Fraction(56, 81), "unexpected lower certificate for log 2") + require(q_upper == Fraction(25, 36), "unexpected upper certificate for log 2") + require(q_lower > Fraction(2, 3), "lower bound log 2 > 2/3 failed") + require(q_upper < Fraction(7, 10), "upper bound log 2 < 7/10 failed") + + # Small-R range: R in [1/64, 3/4]. + # The logarithmic estimate contributes 2/(1+R), whose minimum on this + # range is 8/7. The q-term contributes at most 21/20. + split = Fraction(3, 4) + log_coefficient = Fraction(2, 1) / (1 + split) + reward_coefficient = Fraction(7, 10) * Fraction(3, 2) + coefficient_gap = log_coefficient - reward_coefficient + small_range_margin = coefficient_gap * Fraction(1, 64) + require(log_coefficient == Fraction(8, 7), "small-range log coefficient drifted") + require(reward_coefficient == Fraction(21, 20), "small-range reward coefficient drifted") + require(coefficient_gap == Fraction(13, 140), "small-range coefficient gap drifted") + require(small_range_margin == Fraction(13, 8960), "small-range margin drifted") + require( + small_range_margin > Fraction(1, 5000), + "small-range 1/5000 margin failed", + ) + + # Large-R range: R in [3/4, 1]. The phase corridor gives T < 4, so the + # right structural bound contributes at most q(1-R). Hence q-R is at most + # 7/10 - 3/4 = -1/20. + large_range_margin = split - Fraction(7, 10) + require(large_range_margin == Fraction(1, 20), "large-range margin drifted") + require( + large_range_margin > Fraction(1, 5000), + "large-range 1/5000 margin failed", + ) + + print("ERDOS 625 PARTIAL-DIAGONAL SCALAR LEDGER: PASS") + print(f" log 2 lower: {q_lower}") + print(f" log 2 upper: {q_upper}") + print(f" split point: {split}") + print(f" small-range coefficient gap: {coefficient_gap}") + print(f" small-range uniform margin: {small_range_margin}") + print(f" large-range uniform margin: {large_range_margin}") + print(" scope: rational ledger only; analytic and asymptotic reductions are external") + + +if __name__ == "__main__": + main() diff --git a/625/experiments/check_self_contained_manuscript_v3.py b/625/experiments/check_self_contained_manuscript_v3.py index e5000869..541962a2 100644 --- a/625/experiments/check_self_contained_manuscript_v3.py +++ b/625/experiments/check_self_contained_manuscript_v3.py @@ -12,6 +12,8 @@ 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" +PARTIAL_RATE_CHECKER = ROOT / "experiments" / "check_partial_diagonal_rate_v3.py" GENERATED = ARXIV / "AMS_SELF_CONTAINED_BODY_V3.generated.tex" MASTER = ARXIV / "AMS_SELF_CONTAINED_DRAFT_V3.tex" @@ -19,6 +21,11 @@ ARXIV / "FRONTMATTER_INTRODUCTION_SELF_CONTAINED_V3.tex", ARXIV / "CONVENTIONS_AND_PROOF_OBJECTS_V3.tex", ARXIV / "PROOF_ARCHITECTURE_SELF_CONTAINED_V3.tex", + ARXIV / "SECTION4_CHROMATIC_LOWER_TAIL_V3.tex", + ARXIV / "SECTION5_ROOT_TRANSPORT_V3.tex", + ARXIV / "SECTION7_EMPTY_CORNER_V3.tex", + ARXIV / "SECTION7_CENTRAL_EXTRACTION_V3.tex", + ARXIV / "SECTION7_FULL_CORNER_V3.tex", ARXIV / "SECTION8_SELF_CONTAINED_V3.tex", ARXIV / "SECTION9_SELF_CONTAINED_V3.tex", ARXIV / "FINAL_ASSEMBLY_SELF_CONTAINED_V3.tex", @@ -53,11 +60,28 @@ 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, *SOURCE_FILES]: + for path in [ + MASTER, + GENERATOR, + CONSTANT_CHECKER, + PARTIAL_RATE_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) + subprocess.run(["python", str(PARTIAL_RATE_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 +91,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", @@ -86,6 +109,11 @@ def main() -> None: required_body_markers = ( r"\section{Phase notation and elementary estimates}", + r"\input{SECTION4_CHROMATIC_LOWER_TAIL_V3}", + r"\input{SECTION5_ROOT_TRANSPORT_V3}", + r"\input{SECTION7_EMPTY_CORNER_V3}", + r"\input{SECTION7_CENTRAL_EXTRACTION_V3}", + r"\input{SECTION7_FULL_CORNER_V3}", r"\input{SECTION8_SELF_CONTAINED_V3}", r"\input{SECTION9_SELF_CONTAINED_V3}", r"\section{Rare-event amplification}", @@ -95,18 +123,124 @@ def main() -> None: missing_body = [token for token in required_body_markers if token not in generated] require(not missing_body, f"generated body missing markers: {missing_body}") require( - generated.count(r"\section{") >= 8, - "generated body does not contain the canonical numbered sections", + generated.count(r"\section{") >= 7, + "generated body does not contain the expected numbered sections", ) - # The frozen source contributes 1,915 generated lines after the deliberate - # removal of the old Sections 8, 9, and 11. The replacement sections are - # separate audited inputs, so this gate checks against that exact source - # volume rather than an arbitrary journal-length target. require( - len(generated.splitlines()) >= 1800, + len(generated.splitlines()) >= 1120, f"generated body is unexpectedly short: {len(generated.splitlines())} lines", ) + section4 = sources["SECTION4_CHROMATIC_LOWER_TAIL_V3.tex"] + section4_flat = flatten(section4) + for token in ( + "A uniform lower location", + r"\Delta_n:=r_+(n)-k_\chi^-", + r"\frac{n}{k^2}", + r"c_*(\log n)^2", + r"\varepsilon_n^{\mathrm{prof}}", + r"\varepsilon_n^{\mathrm{cap}}", + "Splitting such a class into two nonempty subsets preserves independence", + "The direction is strict", + r"o\!\left(\frac{n}{(\log n)^3}\right)", + "full sequence of integers", + ): + require(token in section4_flat, f"Section 4 lower tail missing: {token}") + require( + r"\begin{equation}" not in section4, + "Section 4 lower tail uses numbered equations with manual tags", + ) + require( + "By Lemma 3.1 and (1.2)" not in generated, + "compressed chromatic lower-tail proof remains in generated source", + ) + + section5 = sources["SECTION5_ROOT_TRANSPORT_V3.tex"] + section5_flat = flatten(section5) + for token in ( + "finite-$n$ support loss", + r"D_{4,n}(T)", + r"T_+(n)=T_0", + r"\mathcal F_S'(T)=-\lambda_S(T)", + r"\omega_n^{\mathrm{root}}", + "This equality is finite and contains no limiting substitution", + "one deterministic error sequence valid across the complete phase", + "integer sequences approaching either endpoint", + r"r_4^{\mathrm{co}}= 260, + f"Section 7 central extraction is unexpectedly short: {len(central.splitlines())} lines", + ) + require( + r"\begin{equation}" not in central, + "Section 7 central extraction uses numbered equations with manual tags", + ) + + full = sources["SECTION7_FULL_CORNER_V3.tex"] + full_flat = flatten(full) + for token in ( + r"v(a)+u_i\le v(h)", + r"\mu_{u_i}(w)\le n^{-3}", + r"2n^{-2}<1", + r"\varepsilon_n^{\mathrm{full}}", + "Disjoint three-range assembly", + r"\eta<31/32", + "no boundary term is counted twice", + r"\varepsilon_n^{\mathrm{central}}", + "one eventuality threshold for the complete phase", + ): + require(token in full_flat, f"Section 7 full corner missing: {token}") + require( + r"\begin{equation}" not in full, + "Section 7 full corner uses numbered equations with manual tags", + ) + section8 = sources["SECTION8_SELF_CONTAINED_V3.tex"] section8_flat = flatten(section8) for token in ( @@ -115,12 +249,17 @@ 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"w_{\mathrm{hi}}(P,j):=w(P,j)", + "one-sided reference measure", + "not a deletion of common-class overlaps", 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 +267,17 @@ def main() -> None: r"\theta_{ab}", r"\lambda_{ab}", r"q_{ab}", + r"\Phi_F", + r"\label{eq:zero-residual-attachment-v3}", + "the unique empty matching", + "no independence between cells is asserted", + "no overlap is assigned to two skeletons", + r"\frac{U^2}{8}", + r"\frac{U^2}{6}", + "factorial term only improves the upper bound", "Fixed even-set expansion", "Restriction-product bound", + "Quadratic activity bound", "The intrinsic residual regime", "The complementary residual regime", "Normalized signed second moment", @@ -139,12 +287,22 @@ 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", + r"\frac{2777}{10000}", + r"\frac{20000}{12777}", + r"\frac{12780}{12777}", + r"\sigma_4>0", + "there is no additional correction to the total number of classes", + "exact rational certificates", + "1035264923841377", + "check\\_constant\\_ledger\\_v3.py", "Simultaneous complement form", + "no further asymptotic loss is introduced", ): require(token in final_flat, f"final assembly missing: {token}") + require("+b_n" not in final, "final assembly reintroduced a class-count correction") + require("|b_n|" not in final, "final assembly reintroduced an untracked correction") appendix = sources["FORMALIZATION_STATUS_APPENDIX_V3.tex"] appendix_flat = flatten(appendix) @@ -153,6 +311,15 @@ def main() -> None: "Running", "Needs review", "eventually_fourEndpointThreeQuarterRho_le_one", + "SECTION5_ROOT_TRANSPORT_V3.tex", + "SECTION7_EMPTY_CORNER_V3.tex", + "SECTION7_CENTRAL_EXTRACTION_V3.tex", + "SECTION7_FULL_CORNER_V3.tex", + "sum_partialDiagonalWeight_le_exp_sum_muCutoffActivity", + "partialDiagonalRate_uniform_negative", + "partialDiagonalRate_uniform_negative_fourDeficit", + "sum_partialDiagonalWeight_fullCorner_eq", + "complete candidate manuscript proof of E625-11A--D", "Publication gate", "Recommended theorem-facing Lean organization", ): @@ -164,10 +331,15 @@ def main() -> None: "proof omitted", "details are standard", "The endpoint transportation estimate absorbs", + "canonically equivalent to the dependent sum", + "after Section~7 has removed", r"\exp\!left", r"\begin{lemmabox}", r"\begin{propositionbox}", r"\begin{resultbox}", + r"\paragraph{Proof", + r"\(\square\)", + r"\log2", r"\ln", ) offenders = [token for token in forbidden if token in combined] @@ -175,34 +347,33 @@ 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(): + check_control_characters(text, name) check_balanced_environments(text, name) require(text.count("{") == text.count("}"), f"{name}: unbalanced braces") words = re.findall(r"[A-Za-z][A-Za-z'-]+", strip_tex(combined)) + # The generated body delegates theorem-facing passages to checked source + # files, so this threshold measures the assembled source set rather than + # the length of one monolithic generated file. require( - len(words) >= 5000, + len(words) >= 5700, f"manuscript prose extraction is unexpectedly short: {len(words)} words", ) print("ERDOS 625 SELF-CONTAINED MANUSCRIPT CHECK: PASS") print(f" generated body lines: {len(generated.splitlines())}") + print(f" Section 4 lower-tail source lines: {len(section4.splitlines())}") + print(f" Section 5 root-transport source lines: {len(section5.splitlines())}") + print(f" Section 7 empty source lines: {len(empty.splitlines())}") + print(f" Section 7 central source lines: {len(central.splitlines())}") + print(f" Section 7 full source lines: {len(full.splitlines())}") print(f" approximate prose words: {len(words)}") print(f" unique semantic labels: {len(label_counts)}") + print(" exact certificates: four-support slack and partial-diagonal scalar ledger") print(" publication switch: disabled") diff --git a/625/scripts/build_self_contained_ams_v3.py b/625/scripts/build_self_contained_ams_v3.py index 9a2f944c..324e7766 100644 --- a/625/scripts/build_self_contained_ams_v3.py +++ b/625/scripts/build_self_contained_ams_v3.py @@ -2,10 +2,11 @@ """Generate the complete AMS Version 3 manuscript body. The canonical TeX remains frozen while the proof is incomplete. This script -extracts the complete Sections 1--7 and 10 from that source, normalizes their -legacy statement environments, and inserts the audited replacement Sections 8, -9, and 11. The exact canonical Git-blob SHA is checked before line-independent -section markers are used. +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 theorem-facing replacement +sources for the arguments under active proof closure. The canonical Git-blob +SHA is checked before line-independent section markers are used. """ from __future__ import annotations @@ -43,9 +44,24 @@ def slice_between(text: str, start: str, end: str) -> str: return text[begin:finish] +def replace_between(text: str, start: str, end: str, replacement: str) -> str: + """Replace one marker-delimited block, retaining the end marker.""" + begin = text.find(start) + finish = text.find(end, begin + 1) + require(begin >= 0, f"missing replacement start marker: {start}") + require(finish >= 0, f"missing replacement end marker: {end}") + require(begin < finish, f"reversed replacement markers: {start!r}, {end!r}") + return text[:begin] + replacement + text[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 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?", @@ -73,11 +89,43 @@ 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, + ) - # 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}") + 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. replacements = { r"\ln": r"\log", + r"\log2": r"\log 2", "colouring": "coloring", "colourings": "colorings", "coloured": "colored", @@ -98,6 +146,208 @@ 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 = { + ( + "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." + ), + ( + "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." + ), + ( + "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." + ): ( + "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." + ), + } + for old, new in prose_replacements.items(): + text = text.replace(old, new) + + text = text.replace( + "The recurrence (7.4) controls the empty corner, the\n" + "continuous rate function controls the central range, and the reverse\n" + "recurrence (7.6) controls the full corner. The ranges overlap only at their\n" + "boundaries and together exhaust every common subprofile.", + ( + "The recurrence (7.4) controls the empty corner, the continuous rate\n" + "function controls the central range, and the reverse recurrence (7.6)\n" + "controls the full corner. For all sufficiently large \\(n\\), when\n" + "\\(\\eta<31/32\\), the three ranges are the disjoint sets\n" + "\\(m\\le\\eta n\\); \\(m>\\eta n\\) and \\(n-m>n/32\\); and\n" + "\\(n-m\\le n/32\\). They are exhaustive, so no inclusion--exclusion or\n" + "boundary convention is hidden in the assembly." + ), + ) + + text = re.sub( + r"We (?:first|begin by) bracket this tilt\..*?Substituting\s+\\\(i=j\+2\\\) in the weight gives", + lambda _: ( + "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( + "\\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." + ), + ) + + # Replace the complete chromatic lower-tail section by a standalone source. + text = replace_between( + text, + r"\section{\texorpdfstring{A valid unrestricted lower location for", + r"\section{The four-size signed first-moment advantage}", + r"\input{SECTION4_CHROMATIC_LOWER_TAIL_V3}" + "\n\n", + ) + + root_transport_old = r"""Put +\[ + \Phi_n(k):=L_{S_4}(n,k)+{\log 2}k. +\] +Then \(\Phi_n(r_4^{\mathrm{co}})=0\) by definition, while at +\(k=r_+\), Lemma 3.1 and (5.2) give + +\[ + L_{S_4}(n,r_+)+{\log 2}r_+ + =r_+\{{\log 2}-D_4(\delta)+o(1)\}. \tag{5.10} +\] +""" + require( + root_transport_old in text, + "missing canonical Section 5 root-transport block", + ) + text = text.replace( + root_transport_old, + r"\input{SECTION5_ROOT_TRANSPORT_V3}" + "\n", + 1, + ) + + # Replace all three Section 7 ranges by standalone sources. The exact + # counting identities and lemma statement remain in the generated body; + # each asymptotic range can now be audited without a generator-sized diff. + text = re.sub( + r"\\displayheading\{Empty corner\}.*?(?=\\displayheading\{Central range\})", + lambda _: "\\input{SECTION7_EMPTY_CORNER_V3}\n\n", + text, + count=1, + flags=re.S, + ) + text = re.sub( + r"\\displayheading\{Central range\}.*?(?=\\displayheading\{Full corner\})", + lambda _: "\\input{SECTION7_CENTRAL_EXTRACTION_V3}\n\n", + text, + count=1, + flags=re.S, + ) + text = re.sub( + r"\\displayheading\{Full corner\}.*?(?=\\end\{proof\})", + lambda _: "\\input{SECTION7_FULL_CORNER_V3}\n", + 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\.", + lambda _: ( + "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\.", + lambda _: ( + "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" + "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.