From 1686d90808a65ca8ef5f10b6d7b6f7abd659028b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:26:28 +0300 Subject: [PATCH 1/8] =?UTF-8?q?Add=20the=20detailed=20Erd=C5=91s=20625=20v?= =?UTF-8?q?alue-upgrade=20research=20program?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...DOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md | 1122 +++++++++++++++++ 1 file changed, 1122 insertions(+) create mode 100644 625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md diff --git a/625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md b/625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md new file mode 100644 index 00000000..9428ad56 --- /dev/null +++ b/625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md @@ -0,0 +1,1122 @@ +# Erdős Problem 625 after the 12 July candidate proof + +## A theorem-level program for a stronger main paper and substantive follow-up results + +**Date:** 26 July 2026 +**Repository:** `SamPetkov/Erdos` +**Stack base:** PR #41, `agent/625-section8-decorated-reference-quotient` +**Scope:** chronology, current proof frontier, stronger consequences of the existing architecture, and mathematically precise next-result programs + +--- + +## 0. Status convention + +This note deliberately separates four statuses. + +- **Kernel-checked finite theorem:** accepted by Lean in the public repository without `sorry`, `admit`, or a project-defined axiom. +- **Conditional corollary:** follows from the candidate proof once the remaining normalized-second-moment bridge is closed. +- **New theorem target:** a precise statement with a proposed proof route, but not yet established. +- **Exploratory program:** a plausible separate-paper direction whose final theorem is not yet fixed. + +No item labelled conditional or new is presented as already proved. + +--- + +## 1. Public chronology and claim scope + +### 1.1 Public timestamp of the candidate proof + +The candidate proof was publicly recorded on GitHub on **12 July 2026**. +PR #1, + +> `Add verification report and publication bundle for Problem 625`, + +was created at `2026-07-12 19:08:31 UTC` and merged at +`2026-07-12 19:29:28 UTC`. Its public head commit was + +```text +945ed733af198fe8698e14079ddc079f2bc554d7 +``` + +and its merge commit was + +```text +7d0cba893b7cdc707102380c52e22359b867eb5e. +``` + +The PR explicitly described the verdict as + +```text +Provisional internal verification: PASS +``` + +and explicitly did **not** describe it as external verification, peer review, +formal verification, publication, or community acceptance. + +Accordingly, the accurate chronology is: + +1. candidate proof publicly deposited on 12 July 2026; +2. no official solution claim made on the Erdős Problems page while awaiting external assessment; +3. later PRs devoted to adversarial audit, simplification, formalization, + coefficient strengthening, and new consequences. + +The July 12 public record establishes a public chronology. It does not rule out +unpublished independent work by other researchers. + +### 1.2 Current external status + +As of 26 July 2026, the Erdős Problems page still marks Problem 625 as open and +lists no claimed complete or partial solution in its comments: + +- +- + +The closest published/public results remain: + +- A. Heckel, *On a question of Erdős and Gimbel on the cochromatic number*, + Electron. J. Combin. 31 (2024), P4.72, arXiv:2408.13839; +- A. Heckel, *The difference between the chromatic and the cochromatic number + of a random graph*, arXiv:2409.17614, proving a positive answer for roughly + 95% of integers `n`; +- R. Steiner, *On the Difference Between the Chromatic and Cochromatic Number*, + SIAM J. Discrete Math. 39 (2025), 2268--2274. + +A targeted search through 26 July 2026 did not find an indexed paper claiming +the same full-sequence high-probability lower bound of order +`n/(log n)^3`. This is a literature-search statement, not a guarantee about +unpublished or unindexed work. + +### 1.3 Recommended attribution language + +Until an external expert has checked the proof, the repository and any message +to Thomas Bloom should use language of the following form: + +> A candidate full-sequence proof was publicly deposited on GitHub on 12 July +> 2026. The proof has since undergone extensive computational, formal, and +> theorem-by-theorem internal auditing. External verification is still being +> sought, and no claim of community acceptance is made. + +This preserves both priority chronology and mathematical caution. + +--- + +## 2. Notation and the candidate theorem + +Let + +```text +q = ln 2, +N = ln n, +H_n = n/N^3. +``` + +For `G_n ~ G(n,1/2)`, let `chi(G_n)` be the chromatic number and +`zeta(G_n)` the cochromatic number. + +The canonical candidate manuscript proves, conditional on the remaining +Section VIII--IX closure, + +\[ + \Pr\!\left( + \chi(G_n)-\zeta(G_n) + \ge + \frac{q^2}{32}\log\!\left(\frac{200}{153}\right)H_n + \right)\longrightarrow1. +\] + +The displayed coefficient is + +\[ + c_{\mathrm{canonical}} + =\frac{q^2}{32}\log\!\left(\frac{200}{153}\right) + =0.004021983962242\ldots. +\] + +The proof architecture is: + +1. phase-resolved first moment for ordinary independent-set partitions; +2. signed four-size first moment for cocolorings; +3. exact signed overlap/cycle-space identity; +4. partial-diagonal control; +5. canonical high-skeleton endpoint and residual analysis; +6. normalized second moment and Paley--Zygmund rare seed; +7. rare-seed-to-typical-completion amplification; +8. intersection with the chromatic lower event. + +--- + +## 3. Current proof frontier + +### 3.1 Parts that are no longer the bottleneck + +The public stack now contains rigorous finite or focused-CI-checked versions of: + +- the phase expansion and independent-set first moment; +- the four-size signed variational problem; +- the exact signed overlap identity; +- all partial diagonals; +- the endpoint transport inequality; +- the all-high one-cell deficit estimate; +- the matching-restriction product theorem; +- the q-only literal residual attachment estimate; +- the exact reduction of the normalized second moment to the Section VIII bare + skeleton estimate; +- the rare-seed amplifier and graph-law concentration infrastructure. + +PR #41 additionally proves the exact full-endpoint reference normalization: +for each endpoint table `L`, summing over all selected block pairings and all +full-cell physical stub matchings gives exactly the manuscript weight +`fourEndpointW(L)`, with no missing or duplicated factorial. + +It also proves that the map + +```text +fourEndpointDecoratedBlockPairingToPhysicalFibre +``` + +is injective. + +### 3.2 Exact remaining closure theorem + +The decisive remaining proof obligation is a global Section VIII reindexing +and comparison theorem. + +It has two finite subproblems. + +#### Endpoint physical-fibre equivalence + +Complete the reverse construction + +```text +FourEndpointPhysicalFibre + -> FourEndpointDecoratedBlockPairing +``` + +and prove the two round trips. The source branch already contains a candidate +reverse-data construction, but it must receive a direct focused build and a +line-by-line audit before it is counted as proved. + +#### Aggregate deficit reindexing + +Every attained canonical high physical skeleton must be represented by: + +1. a block-level matching support `P`; +2. one full endpoint size `m_e` per selected cell; +3. one admissible deficit `h_e`, so the actual multiplicity is + `j_e=m_e-h_e`; +4. one partial physical stub matching in each selected cell. + +After summing the local physical fibres, the aggregate weight 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!} + \prod_{e\in P}g(j_e), + \qquad J=\sum_{e\in P}j_e. +\] + +For `d_e=|s_e-t_e|` and `h_e=m_e-j_e`, the exact local aggregate ratio is + +\[ + R_{m,d}(h) + = + \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)} + 2^{-hm+h(h+1)/2}. +\] + +The single nonlocal denominator changes by + +\[ + \frac{(n)_{J+H}}{(n)_J}=(n-J)_H\le n^H, + \qquad H=\sum_eh_e. +\] + +Hence + +\[ + \boxed{ + \frac{w(P,m-h)}{w_{\mathrm{full}}(P)} + \le + \prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e).} +\] + +The high-cell condition gives `2h\log\!\left(\frac{1000}{639}\right) +\] + +uniformly in the full limiting phase interval. Therefore the midpoint theorem +supports + +\[ + \boxed{ + c_*=\frac{q^2}{8}\log\!\left(\frac{1000}{639}\right) + =0.026896409808379\ldots.} +\] + +This is approximately + +\[ + 6.68734884596 +\] + +times the constant printed in the canonical candidate manuscript. + +### 4.3 Complement-symmetric consequence + +Since + +\[ + \zeta(\overline G)=\zeta(G) +\] + +and `G(n,1/2)` is complement invariant, applying the completed theorem to both +`G_n` and `\overline G_n` gives + +\[ + \boxed{ + \min\{\chi(G_n),\chi(\overline G_n)\}-\zeta(G_n) + \ge c_*H_n + } +\] + +with high probability. + +This says the mixed partition beats both pure orientations simultaneously. + +### 4.4 Tunable upper tail for the cochromatic location + +The rare-seed amplifier gives more than one high-probability specialization. +If a `k_n`-cocoloring seed has probability at least `exp(-Lambda_n)`, then for +every deterministic `r>0`, + +\[ + \Pr\!\left( + \zeta(G_n)>k_n+C\left[ + \frac{\sqrt{n\Lambda_n}+\sqrt{nr}}{N} + +n^{1/3}+1 + \right]\right) + \le e^{-r}+o(1). +\] + +This should be stated as a named theorem or proposition, since it is reusable +outside the single final choice of `r`. + +### 4.5 Balanced-sign rare seed + +Let `Z_sgn` count signed witnesses with arbitrary clique/independent labels and +let `Z_bal` restrict to exactly `floor(k/2)` clique labels. Then + +\[ + \mathbb EZ_{\mathrm{bal}} + =\frac{\binom{k}{\lfloor k/2\rfloor}}{2^k} + \mathbb EZ_{\mathrm{sgn}}, +\] + +and + +\[ + \binom{k}{\lfloor k/2\rfloor}\ge\frac{2^k}{k+1}. +\] + +Since `Z_bal<=Z_sgn`, + +\[ + \frac{\mathbb EZ_{\mathrm{bal}}^2} + {(\mathbb EZ_{\mathrm{bal}})^2} + \le + (k+1)^2 + \frac{\mathbb EZ_{\mathrm{sgn}}^2} + {(\mathbb EZ_{\mathrm{sgn}})^2}. +\] + +Thus the normalized second moment supplies a balanced rare seed at the same +exponential scale, up to `O(log k)`. + +The high-probability preservation of balance requires a labelled-slot +amplifier and is a separate theorem target below. + +--- + +## 5. New theorem target I: remove the midpoint loss + +### 5.1 General placement + +For `00`, but the seed remains a factor `sqrt N` above the +`n/N^4` error scale. + +### 5.3 Target theorem + +> **Near-root placement theorem.** Assume the four-support profile +> construction and Proposition 9.2 hold uniformly for placements +> `theta_n` satisfying `theta_n N -> infinity`. Then, for +> `theta_n=N^{-1/2}`, +> \[ +> \chi(G_n)-\zeta(G_n) +> \ge +> \left(\frac{q^2}{4}A_4(\delta_n)-o(1)\right)H_n +> \] +> with high probability. + +The certified uniform consequence would be + +\[ + \boxed{ + \chi(G_n)-\zeta(G_n) + \ge + \frac{q^2}{4}\log\!\left(\frac{1000}{639}\right)H_n + } +\] + +with coefficient + +\[ + 0.053792819616758\ldots, +\] + +approximately `13.3746976919` times the canonical displayed coefficient. + +### 5.4 Required proof audit + +The proof should expose all dependence on the signed-root buffer in: + +1. integer profile feasibility; +2. finite-to-limiting entropy approximation; +3. partial-diagonal estimates; +4. canonical high-skeleton estimates; +5. the q-only residual estimate; +6. Paley--Zygmund seed probability; +7. the amplifier loss. + +The critical question is not whether `theta` is fixed. It is whether every +error is uniform on a window whose width above the signed root is +`omega(n/N^4)`. + +**Priority:** highest-return theorem that reuses the existing architecture. + +--- + +## 6. New theorem target II: exact minimum of the four-support advantage + +Numerical scans suggest + +\[ + \min_{\delta\in[0,1]}A_4(\delta) + \approx0.520701335491, +\] + +apparently near the endpoint `delta=1`. This value is diagnostic only. + +Let `F_S(T)` be the constrained entropy value for support `S`, and let +`lambda_S(T)` be its selected Lagrange multiplier. The envelope identity is + +\[ + \frac{d}{dT}F_S(T)=-\lambda_S(T). +\] + +For the full support and `S_4={2,3,4,5}`, + +\[ + D_4(T)=F_\infty(T)-F_4(T), +\] + +so + +\[ + \frac{d}{dT}D_4(T) + =\lambda_4(T)-\lambda_\infty(T). +\] + +If `T=T_0(delta)`, then + +\[ + A_4'(\delta) + =T_0'(\delta) + \bigl(\lambda_\infty(T_0(\delta)) + -\lambda_4(T_0(\delta))\bigr). +\] + +A rigorous endpoint-minimum theorem can therefore be obtained by: + +1. proving monotonicity of `T_0`; +2. interval-enclosing both selected tilts on a finite partition of the phase + interval; +3. certifying the sign of `lambda_infinity-lambda_4`; +4. evaluating `A_4(1)` with rational interval bounds. + +If the diagnostic minimum is certified, the midpoint coefficient becomes + +\[ + 0.031271565748\ldots, +\] + +and the near-root coefficient becomes + +\[ + 0.062543131497\ldots. +\] + +This would be the sharp constant for the existing four-size support, not the +sharp constant for the full cochromatic problem. + +--- + +## 7. New theorem target III: balance is necessary near the optimum + +### 7.1 Sign entropy + +Suppose a signed partition has `k` nonempty classes, of which a proportion +`rho` are labelled clique classes. The number of sign assignments with this +proportion is + +\[ + \binom{k}{\rho k} + =\exp\{kH(\rho)+O(\log k)\}, +\] + +where + +\[ + H(\rho)=-\rho\log\rho-(1-\rho)\log(1-\rho). +\] + +The unrestricted sign entropy is `k log 2`. Thus an imbalance costs + +\[ + k\bigl(\log2-H(\rho)\bigr). +\] + +Near `rho=1/2+x`, + +\[ + \log2-H(1/2+x)=2x^2+O(x^4). +\] + +Since the local derivative of the coloring first-moment logarithm with respect +to the number of classes is of order `N^2`, an entropy loss of order +`k=Theta(n/N)` produces a root displacement of order + +\[ + \frac{n/N}{N^2}=\frac n{N^3}=H_n. +\] + +### 7.2 Target structural theorem + +> **Balance stability theorem.** For every fixed `epsilon>0`, there exists +> `c(epsilon)>0` such that, with high probability, every cocoloring whose +> clique-class proportion lies outside +> `[1/2-epsilon,1/2+epsilon]` uses at least +> \[ +> r_4^{\mathrm{co}}(n)+c(\epsilon)H_n +> \] +> nonempty classes. + +A quantitative local version should give + +\[ + c(\epsilon) + =\frac{q^2}{4}\bigl(\log2-H(1/2+\epsilon)\bigr) + +o_\epsilon(1) +\] + +up to the support loss and root normalization. + +Consequently, any sequence of cocolorings with class count + +\[ + r_4^{\mathrm{co}}(n)+o(H_n) +\] + +must satisfy + +\[ + \rho_n=\frac12+o(1). +\] + +This is more conceptually valuable than merely constructing one balanced seed: +it identifies a structural feature forced by near-optimality. + +### 7.3 Proof route + +1. refine the first-moment sum by the number of clique labels; +2. replace the sign factor `2^k` by `binom(k,rho k)`; +3. rerun the finite-support root calculation with `log 2` replaced by + `H(rho)`; +4. take a union bound over imbalanced `rho` values; +5. combine with the balanced existence result. + +A labelled-slot amplifier can then produce, with high probability, a +near-optimal cocoloring having + +\[ + \#\{\text{clique parts}\}=(1/2+o(1))k, + \qquad + \#\{\text{independent parts}\}=(1/2+o(1))k. +\] + +--- + +## 8. High-upside extension: slowly growing support + +### 8.1 Motivation + +For a fixed finite support `S`, the signed-root advantage is + +\[ + \frac{q^2}{4}\bigl(\log2-D_S(\delta_n)\bigr)H_n. +\] + +The four-size support has a strictly positive but nonzero truncation loss. +A five-size support improves the scanned minimum by only about `1.017%` while +raising the endpoint table dimension from `4x4` to `5x5`. Therefore a single +fixed extra size is not a compelling redesign. + +The meaningful target is a support `S_n` whose width tends slowly to infinity. + +### 8.2 Limiting coefficient + +If + +\[ + \sup_{\delta\in[0,1]}D_{S_n}(\delta)\longrightarrow0, +\] + +then the signed-root displacement tends to + +\[ + \frac{q^3}{4}H_n. +\] + +Midpoint placement would retain + +\[ + \frac{q^3}{8}=0.041628081498616\ldots, +\] + +whereas near-root placement would retain + +\[ + \boxed{ + \frac{q^3}{4}=0.083256162997232\ldots.} +\] + +### 8.3 Why uniform truncation is plausible + +The selected full-support deficit law has Gaussian-type tails in the existing +analytic infrastructure. A support containing all deficits up to a cutoff +`m` should therefore satisfy an omitted-mass estimate of the form + +\[ + \sup_\delta D_m(\delta) + \le C\exp(-cm^2) +\] + +or another uniform tail tending to zero. + +The first-moment side is therefore plausible. The principal difficulty is a +second moment uniform in the number of endpoint types. + +### 8.4 Dimension-uniform second-moment program + +The fixed-support proof must be reorganized so that constants depend on the +support width through an explicit complexity envelope `K(m)`. + +Required ingredients: + +1. endpoint transportation controlled by norms or generating functions rather + than `m^2` unrelated cell estimates; +2. a block-matching description whose sparsity is independent of the ambient + type-table dimension; +3. all-high deficit bounds uniform in the endpoint type; +4. q-only residual bounds with explicit polynomial or subexponential dependence + on `m`; +5. an explicit choice `m=m_n` such that + \[ + K(m_n)=o(N). + \] + +If `K(m)` is polynomial, `m_n=floor(log log n)` is more than sufficient. If +`K(m)` is exponential in a fixed power of `m`, a slower cutoff such as +`floor(log log log n)` may be appropriate. + +### 8.5 Target theorem + +> **Slow-support theorem.** There exists an explicit sequence `m_n->infinity` +> and a signed profile supported on `m_n` consecutive deficit sizes such that +> \[ +> \chi(G_n)-\zeta(G_n) +> \ge +> \left(\frac{q^3}{4}-o(1)\right)H_n +> \] +> with high probability. + +This would be the strongest result naturally suggested by the present signed +entropy mechanism. It is a plausible separate paper or a major Version 3, +not a prerequisite for validating the July 12 theorem. + +--- + +## 9. Largest follow-up target: prove the matching upper bound + +Heckel conjectures + +\[ + \chi(G_n)-\zeta(G_n) + \asymp\frac n{(\log n)^3} +\] + +with high probability. The candidate theorem supplies the full-sequence lower +bound side. + +The most important possible follow-up is + +\[ + \boxed{ + \chi(G_n)-\zeta(G_n) + =O(H_n) + } +\] + +with high probability. + +### 9.1 Required location bounds + +A two-sided proof can be decomposed into: + +\[ + \zeta(G_n) + \ge r_{\mathrm{signed,full}}(n)-O(H_n) +\] + +and + +\[ + \chi(G_n) + \le r_+(n)+O(H_n). +\] + +The first inequality is a lower bound on the cochromatic number and should come +from a first-moment union bound over **all** signed profiles, not only the +selected four-size witness family. + +The second inequality requires a third-order ordinary-coloring construction. +Existing first-order or `o(n/N^2)` localization is not automatically precise +enough at the `H_n=n/N^3` scale. + +### 9.2 Intermediate publishable theorem + +Before the full upper bound, establish a phase-resolved corridor + +\[ + r_{\mathrm{signed,full}}(n)-o(H_n) + \le\zeta(G_n) + \le r_4^{\mathrm{co}}(n)+o(H_n). +\] + +This would be the first explicit third-order location result for the +cochromatic number itself and would isolate the remaining ordinary-coloring +input needed for the complete `Theta(H_n)` theorem. + +### 9.3 Why this should be a separate project + +The lower-gap proof is based on constructing one signed witness and amplifying +a rare seed. A matching upper bound requires excluding all better signed +partitions and constructing ordinary colorings to matching precision. It is a +different global optimization problem and should not delay external review of +the current proof. + +--- + +## 10. General edge density `p != 1/2` + +For `G(n,p)`, a class of size `s` is independent with probability + +\[ + (1-p)^{\binom s2} +\] + +and a clique with probability + +\[ + p^{\binom s2}. +\] + +Summing the two declarations gives the one-class reward + +\[ + g_p(s)=p^{\binom s2}+(1-p)^{\binom s2}. +\] + +At `p=1/2`, + +\[ + g_{1/2}(s)=2^{1-\binom s2}, +\] + +which is the exact symmetric sign gain used in the present proof. + +For `p!=1/2`, the optimal declaration depends on class size and the two-partition +overlap factor acquires an external field. The binary compatibility sum becomes +an inhomogeneous Ising-type partition function on the overlap support graph. + +A separate project should determine: + +1. whether a polynomial chromatic--cochromatic gap persists for every fixed + `p in (0,1)`; +2. the optimal phase-dependent clique proportion; +3. the analogue of the finite-support entropy advantage; +4. whether `p=1/2` is merely a symmetry point or a transition point in the + structure of optimal mixed partitions. + +This direction connects naturally with generalized hereditary chromatic numbers: + +- E. Scheinerman, *Generalized Chromatic Numbers of Random Graphs*, SIAM J. + Discrete Math. 5 (1992), 74--80; +- B. Bollobás and A. Thomason, *Generalized chromatic numbers of random graphs*, + Random Structures & Algorithms 6 (1995), 353--356. + +--- + +## 11. Two-independent-graph model + +The Erdős Problems discussion records the following model, attributed there to +Zach Hunter with Micha Christoph, Annika Heckel, and Raphael Steiner. + +Let `G_1,G_2` be independent copies of `G(n,1/2)`. Define `X(G_1,G_2)` as the +minimum number of parts in a partition in which each part is independent in at +least one of the two graphs. + +For a fixed partition into `k` classes and a fixed assignment of every class to +one of the two layers, + +\[ + \Pr\{\text{all assigned independence constraints hold}\} + =2^{-\sum_i\binom{|C_i|}{2}}. +\] + +Summing over the `2^k` layer assignments gives **exactly the same first moment** +as the signed clique/independent witness at `p=1/2`. + +The second moment is different. A class labelled clique in one witness and +independent in another creates a compatibility obstruction in the one-graph +model. In the two-layer model, constraints in different graph layers are +independent rather than contradictory. This may replace the cycle-space +compatibility factor by a simpler two-layer overlap calculation. + +The forum comment reports a McDiarmid coupling under which + +\[ + X(G_1,G_2)\ge\zeta(G) +\] + +for a coupled `G~G(n,1/2)`. The comments are explicitly unverified. Before +using this model in a paper: + +1. obtain the exact coupling proof from the people named in the discussion; +2. agree on attribution; +3. calculate the two-layer normalized second moment; +4. compare its phase constant with the one-graph signed model. + +This is a credible alternative proof or follow-up paper, not an input that +should be silently folded into the current manuscript. + +--- + +## 12. Reusable method results + +### 12.1 Restriction-product theorem + +If a finite family `C` of subsets of a finite ground set `E` is determined +injectively by deletion of a coordinate set `I`, then for nonnegative +activities `q_e`, + +\[ + \sum_{A\in\mathcal C}\prod_{e\in A\setminus I}q_e + \le\prod_{e\in E\setminus I}(1+q_e). +\] + +For graph cycle spaces, deletion of a forest is injective. For binary matroid +cycle spaces, deletion of an independent set is injective. + +The theorem is useful inside the main paper. It is too short for a standalone +paper unless combined with several applications or a stability/sharpness +theory. + +### 12.2 Exact cycle-space factor + +For two signed partitions, the support graph of overlap cells of size at least +two carries the exact factor + +\[ + 2^{W+c(H)-|V(H)|} + =\left(\prod_eg(r_e)\right)2^{\beta(H)}. +\] + +The topological correction is the binary cycle-space dimension. A `q`-template +generalization should lead to Potts/Tutte-type factors. + +### 12.3 Rare-seed amplifier + +The amplification argument depends only on: + +1. independent block exposure; +2. a Lipschitz maximum feasible induced-subobject score; +3. a rare full-coverage seed; +4. a deterministic or high-probability leftover completion rule. + +An abstract methods theorem would apply to other hereditary covering and +partition parameters. It becomes a viable standalone methods paper only after +at least one further nontrivial application is supplied. + +--- + +## 13. Recommended publication architecture + +### Main Erdős 625 paper, Version 2 + +Include: + +1. the full-sequence candidate theorem after external verification; +2. the phase-resolved coefficient; +3. the certified uniform coefficient + `q^2 log(1000/639)/8`; +4. the simultaneous complement corollary; +5. the tunable cochromatic upper-tail theorem; +6. the matching-restriction simplification; +7. the exact endpoint normalization and aggregate deficit proof; +8. the rare-seed amplifier as a named method proposition; +9. a precise public chronology and verification-status paragraph. + +Include the balanced rare seed. Include high-probability balance only if the +labelled-slot amplifier is completed. + +### Follow-up paper A: structure and sharp coefficient + +Best moderate-risk package: + +1. near-root placement and removal of the midpoint loss; +2. exact phase minimum for the four-support advantage; +3. existence and necessity of balanced near-optimal cocolorings. + +This package would improve both the constant and the conceptual content. + +### Follow-up paper B: growing support + +Develop dimension-uniform endpoint and residual estimates and approach the +coefficient `q^3/4`. + +### Follow-up paper C: matching upper bound + +Prove the `O(n/(log n)^3)` upper bound and hence the full order conjecture. +This is the most important but highest-risk project. + +### Alternative follow-up + +Develop the two-independent-graph model after direct communication and explicit +attribution. + +--- + +## 14. Concrete PR sequence + +### Closure PRs + +1. validate the physical-fibre reverse-data module; +2. prove decorated/physical round trips; +3. prove the aggregate high-deficit reindexing; +4. instantiate the bare-skeleton asymptotic; +5. derive Proposition 9.2 and the final event intersection on one branch. + +### Value-upgrade PRs + +6. integrate the phase-resolved `/8` theorem and stronger entropy certificate; +7. add complement and tunable-tail corollaries; +8. expose a uniform error envelope in the placement parameter; +9. prove the `theta_n=N^{-1/2}` near-root theorem; +10. prove the balanced-sign first-moment stability theorem; +11. certify the exact four-support phase minimum. + +### Separate-paper branches + +12. dimension-uniform slowly growing support; +13. all-profile first moment for the lower location of `zeta`; +14. third-order ordinary-coloring upper construction; +15. combine 13--14 into the matching upper bound. + +--- + +## 15. Decision table + +| Direction | Mathematical value | Reuses current proof | Risk | Recommended destination | +|---|---:|---:|---:|---| +| Close physical fibre and deficits | essential | very high | medium | current main paper | +| Phase-resolved `/8` theorem | high | complete | low | current main paper | +| Stronger uniform certificate | high | complete | low | current main paper | +| Complement/tail corollaries | medium | complete | low | current main paper | +| Near-root placement | very high | high | medium | first follow-up or strong V2 | +| Exact phase minimum | medium-high | high | medium | first follow-up | +| Balance necessity | high conceptual value | high | medium | first follow-up | +| Fixed five-size support | small gain | medium | medium | do not prioritize | +| Slowly growing support | very high | medium | high | separate paper | +| Matching upper bound | maximal | low-medium | very high | major separate paper | +| General `p` | high | medium | high | separate paper | +| Two-graph coupling | potentially high | partial | high/attribution-sensitive | separate collaboration | + +--- + +## 16. Immediate recommendation + +The next mathematical work should proceed in this order: + +1. **Finish the current proof closure.** This is still necessary for any theorem + upgrade to be meaningful. +2. **Promote the phase-resolved theorem and the coefficient + `0.0268964098...` into the main paper.** These are already latent in the + current architecture. +3. **Attack near-root placement with `theta_n=N^{-1/2}`.** This is the best + ratio of new value to new machinery. +4. **Prove balance stability.** This gives a structural theorem, not merely a + larger decimal constant. +5. **Choose one major follow-up:** slowly growing support for the best lower + constant, or the matching upper bound for the full conjectured order. + +Further isolated constant tweaks or fixed-support grid scans should not take +priority over these steps. From 1e341d95d4b1191a703d85631e2808b1a83e69ab Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:27:49 +0300 Subject: [PATCH 2/8] Add copy-ready theorem statements and proof blueprints --- .../ERDOS625_VALUE_UPGRADE_THEOREMS.tex | 533 ++++++++++++++++++ 1 file changed, 533 insertions(+) create mode 100644 625/research/ERDOS625_VALUE_UPGRADE_THEOREMS.tex diff --git a/625/research/ERDOS625_VALUE_UPGRADE_THEOREMS.tex b/625/research/ERDOS625_VALUE_UPGRADE_THEOREMS.tex new file mode 100644 index 00000000..96e5c37b --- /dev/null +++ b/625/research/ERDOS625_VALUE_UPGRADE_THEOREMS.tex @@ -0,0 +1,533 @@ +\documentclass[11pt]{article} + +\usepackage[a4paper,margin=1in]{geometry} +\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage{enumitem} +\usepackage[hidelinks]{hyperref} + +\newtheorem{theorem}{Theorem}[section] +\newtheorem{proposition}[theorem]{Proposition} +\newtheorem{lemma}[theorem]{Lemma} +\newtheorem{corollary}[theorem]{Corollary} +\newtheorem{conjecture}[theorem]{Conjecture} +\newtheorem{program}[theorem]{Proof program} +\theoremstyle{definition} +\newtheorem{definition}[theorem]{Definition} +\newtheorem{remark}[theorem]{Remark} + +\newcommand{\whp}{\text{with high probability}} +\newcommand{\E}{\mathbb E} +\newcommand{\Pp}{\mathbb P} +\newcommand{\Nn}{\log n} +\newcommand{\gapscale}{\dfrac{n}{(\log n)^3}} +\newcommand{\smallscale}{\dfrac{n}{(\log n)^4}} +\newcommand{\Afour}{A_4} +\newcommand{\Dfour}{D_4} +\newcommand{\rplus}{r_+} +\newcommand{\rco}{r_4^{\mathrm{co}}} + +\title{Erd\H{o}s Problem 625: theorem upgrades and follow-up programs} +\author{Research planning note} +\date{26 July 2026} + +\begin{document} +\maketitle + +\begin{abstract} +This note isolates the strongest theorem statements currently latent in the +candidate proof of Erd\H{o}s Problem 625 and formulates the next substantive +research targets. Statements are classified as conditional consequences of +the existing proof architecture or as new targets requiring additional work. +No conditional or target statement is represented as already externally +verified. +\end{abstract} + +\section{Notation and the root displacement} + +Let +\[ + q=\log 2,\qquad N=\log n,\qquad H_n=\frac{n}{N^3}. +\] +For $G_n\sim G(n,1/2)$, write $\chi(G_n)$ for the chromatic number and +$\zeta(G_n)$ for the cochromatic number. + +Let $\delta_n\in[0,1)$ be the independence-number phase parameter. For the +four-size signed support, define +\[ + \Afour(\delta)=\log 2-\Dfour(\delta), +\] +where $\Dfour$ is the limiting entropy loss caused by restricting the deficit +support to four consecutive sizes. + +The root calculation used by the candidate proof has the form +\begin{equation} + \rplus(n)-\rco(n) + =\left(\frac{q^2}{4}\Afour(\delta_n)+o(1)\right)H_n. + \label{eq:root-gap} +\end{equation} +Here $\rplus$ is the ordinary-coloring root and $\rco$ is the signed +four-support root. + +\section{Conditional main-paper theorems} + +\begin{theorem}[Phase-resolved full-sequence gap] +\label{thm:phase-gap} +Assume the normalized signed four-support second moment and the +rare-seed-to-typical-completion step in the candidate proof. Then +\[ + \chi(G_n)-\zeta(G_n) + \ge + \left(\frac{q^2}{8}\Afour(\delta_n)-o(1)\right)H_n +\] +with high probability along the full sequence of integers $n$. +\end{theorem} + +\begin{proof}[Proof blueprint] +Place the signed witness at +\[ + k_{1/2}=\left\lceil\frac{\rco+\rplus}{2}\right\rceil. +\] +Equation~\eqref{eq:root-gap} gives +\[ + \rplus-k_{1/2} + =\frac12(\rplus-\rco)+O(1) + =\left(\frac{q^2}{8}\Afour(\delta_n)+o(1)\right)H_n. +\] +The normalized second moment gives a rare signed cocoloring seed. The +amplifier adds $o(H_n)$ classes, while integer rounding also contributes +$o(H_n)$. Intersect with the ordinary chromatic lower event. +\end{proof} + +\begin{corollary}[Certified uniform coefficient] +\label{cor:uniform} +Assume Theorem~\ref{thm:phase-gap} and the certified entropy inequality +\[ + \Afour(\delta)>\log\!\left(\frac{1000}{639}\right) + \qquad(0\le\delta\le1). +\] +Then +\[ + \chi(G_n)-\zeta(G_n) + \ge + \frac{q^2}{8}\log\!\left(\frac{1000}{639}\right)H_n +\] +with high probability. The coefficient equals +\[ + 0.026896409808379\ldots. +\] +\end{corollary} + +\begin{corollary}[Simultaneous comparison with the complement] +\label{cor:complement} +Under the hypotheses of Corollary~\ref{cor:uniform}, +\[ + \min\{\chi(G_n),\chi(\overline G_n)\}-\zeta(G_n) + \ge + \frac{q^2}{8}\log\!\left(\frac{1000}{639}\right)H_n +\] +with high probability. +\end{corollary} + +\begin{proof} +Use $\zeta(\overline G)=\zeta(G)$ and the distributional identity +$\overline G_n\stackrel d=G_n$. Apply Corollary~\ref{cor:uniform} to $G_n$ +and $\overline G_n$ and take a union bound. +\end{proof} + +\begin{proposition}[Tunable cochromatic upper tail] +\label{prop:tunable-tail} +Suppose a $k_n$-cocoloring seed has probability at least +$\exp(-\Lambda_n)$. Then there is an absolute constant $C$ such that, for +every deterministic $r>0$, +\[ + \Pp\!\left( + \zeta(G_n)>k_n+C\left[ + \frac{\sqrt{n\Lambda_n}+\sqrt{nr}}{\log n}+n^{1/3}+1 + \right]\right) + \le e^{-r}+o(1). +\] +\end{proposition} + +\begin{remark} +The proposition should be stated independently of the one value of $r$ used +in the final proof. It is a general output of the rare-seed amplifier. +\end{remark} + +\section{Exact endpoint normalization and the remaining closure} + +Fix a full endpoint table $L$. Let $P$ denote a selected block-level matching +and let every selected cell carry a literal full physical stub matching. +The finite endpoint formalization proves that the aggregate sum over these +decorated objects is exactly the manuscript reference weight $W(L)$. + +\begin{proposition}[Decorated endpoint normalization] +\label{prop:endpoint-normalization} +For every feasible four-type endpoint table $L$, +\[ + \sum_{D\in\mathcal D(L)}w_{\mathrm{atom}}(D)=W(L), +\] +where $\mathcal D(L)$ is the family of block pairings decorated by full-cell +stub matchings and $w_{\mathrm{atom}}$ is the common signed reward divided by +the ambient falling factorial. +\end{proposition} + +The proof proceeds through the exact cardinality identity +\[ + |\mathcal D(L)|\, + \Bigl(\prod_{i,j}\ell_{ij}!\Bigr) + \Bigl(\prod_{i,j}m_{ij}!^{\ell_{ij}}\Bigr) + = + R(L)C(L)S(L), +\] +where $R(L),C(L)$ are the row and column block-selection products and $S(L)$ +is the product of full-cell stub selections. All cancellation in +$\mathbb R_{\ge0}\cup\{\infty\}$ is performed only after positivity and +finiteness of the factorial factors are established. + +The remaining closure is an exact reindexing of every attained high physical +skeleton by a block support, a deficit vector, and local partial stub +matchings. + +For a cell with endpoint sizes $m$ and $m+d$ and deficit $h$, define +\begin{equation} + R_{m,d}(h) + =\frac{\binom mh}{(d+1)(d+2)\cdots(d+h)} + 2^{-hm+h(h+1)/2}. + \label{eq:local-ratio} +\end{equation} +If $J$ is the actual total multiplicity and $H$ the total deficit, then +\begin{equation} + \frac{(n)_{J+H}}{(n)_J}=(n-J)_H\le n^H. + \label{eq:global-denominator} +\end{equation} +Consequently the aggregate decorated-to-full comparison is +\begin{equation} + \frac{w(P,m-h)}{w_{\mathrm{full}}(P)} + \le\prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e). + \label{eq:aggregate-comparison} +\end{equation} + +\begin{program}[Global Section VIII closure] +Prove the following in one theorem chain. +\begin{enumerate}[label=(\roman*)] +\item Construct an equivalence between attained high physical skeletons and +triples consisting of a block matching, an admissible deficit vector, and +local partial stub matchings. +\item Sum the local physical fibres to recover the aggregate weight used in +\eqref{eq:aggregate-comparison}. +\item Use the high condition $2h0$, there exists $c(\varepsilon)>0$ such that, +with high probability, every cocoloring whose clique-class proportion lies +outside $[1/2-\varepsilon,1/2+\varepsilon]$ uses at least +\[ + \rco(n)+c(\varepsilon)H_n +\] +nonempty classes. Consequently every cocoloring using +$\rco(n)+o(H_n)$ classes has clique proportion $1/2+o(1)$. +\end{conjecture} + +\begin{program}[First-moment proof of Conjecture~\ref{conj:balance}] +Refine the signed first moment by the number of clique labels. Replace the +factor $2^k$ by $\binom{k}{\rho k}$ and repeat the root-displacement analysis +with $\log2$ replaced by $H(\rho)$. The entropy deficit shifts the root by +order $H_n$. A union bound excludes all fixed imbalances. A labelled-slot +amplifier then preserves balance with high probability. +\end{program} + +\section{Slowly growing support} + +Let $S_m$ be a consecutive deficit support whose size tends to infinity, and +let $D_m(\delta)$ be its support loss. + +\begin{conjecture}[Uniform truncation] +There exist constants $c,C>0$ such that +\[ + \sup_{\delta\in[0,1]}D_m(\delta)\le Ce^{-cm^2}. +\] +\end{conjecture} + +This is suggested by the Gaussian tail structure of the selected full-support +deficit distribution. + +\begin{conjecture}[Slow-support gap] +\label{conj:slow-support} +There exists an explicit sequence $m_n\to\infty$ and admissible signed profiles +supported on $m_n$ consecutive sizes such that +\[ + \chi(G_n)-\zeta(G_n) + \ge + \left(\frac{q^3}{4}-o(1)\right)H_n +\] +with high probability. +\end{conjecture} + +The limiting coefficient is +\[ + \frac{q^3}{4}=0.083256162997232\ldots. +\] +Midpoint placement alone would give $q^3/8$. + +\begin{program}[Dimension-uniform second moment] +Derive an explicit complexity envelope $K(m)$ for the endpoint and residual +estimates. Prove the bare-skeleton and q-only errors in the form +\[ + \exp\left\{O\left(K(m)\frac n{N^4}\right)\right\}. +\] +Choose $m=m_n$ so that $K(m_n)=o(N)$. If $K$ is polynomial, one may take +$m_n=\lfloor\log\log n\rfloor$; if $K$ is moderately exponential, a slower +sequence such as $\lfloor\log\log\log n\rfloor$ may be required. +\end{program} + +\section{Matching upper bound and the full order conjecture} + +\begin{conjecture}[Heckel order conjecture] +\[ + \chi(G_n)-\zeta(G_n) + =\Theta\left(\frac n{(\log n)^3}\right) +\] +with high probability. +\end{conjecture} + +The candidate proof addresses the lower-bound direction. A matching upper +bound should be decomposed into a lower location theorem for $\zeta$ and a +third-order upper construction for $\chi$. + +\begin{conjecture}[Cochromatic location corridor] +There is a full signed-profile root $r_{\mathrm{sgn}}(n)$ such that +\[ + r_{\mathrm{sgn}}(n)-o(H_n) + \le\zeta(G_n) + \le\rco(n)+o(H_n) +\] +with high probability. +\end{conjecture} + +The lower inequality should follow from a first-moment union bound over all +signed profiles. The upper inequality is the present constructive result. + +\begin{program}[Full upper bound] +\begin{enumerate}[label=(\roman*)] +\item Determine the variational optimum over all signed profiles and prove a +uniform first-moment exclusion below it. +\item Construct ordinary colorings at $\rplus+O(H_n)$ rather than only at +first-order or $o(n/N^2)$ precision. +\item Compare the two phase-resolved roots to obtain +$\chi-\zeta=O(H_n)$. +\end{enumerate} +\end{program} + +\section{General density and the two-layer model} + +For $G(n,p)$, the one-class signed reward is +\[ + g_p(s)=p^{\binom s2}+(1-p)^{\binom s2}. +\] +At $p=1/2$, this reduces to $2^{1-\binom s2}$. For $p\ne1/2$, the sign +variable has a size-dependent external field, and the overlap compatibility +sum becomes an inhomogeneous Ising-type partition function. + +\begin{program}[Fixed $p\ne1/2$] +Determine the optimal clique proportion, phase-resolved signed root, and +whether a polynomial chromatic--cochromatic gap persists for every fixed +$p\in(0,1)$. +\end{program} + +For the two-layer model, sample independent $G_1,G_2\sim G(n,1/2)$ and let +$X(G_1,G_2)$ be the minimum number of classes, each independent in at least one +layer. For a fixed partition and layer assignment, +\[ + \Pp\{\text{all constraints hold}\} + =2^{-\sum_i\binom{|C_i|}{2}}, +\] +so its first moment is exactly the same as the signed one-graph witness after +summing the $2^k$ assignments. + +\begin{program}[Two-layer comparison] +Obtain and verify the McDiarmid coupling reported in the Erd\H{o}s Problems +discussion, with explicit attribution. Then calculate the two-layer second +moment and compare its constant and complexity with the one-graph cycle-space +formula. +\end{program} + +\section{Recommended order of attack} + +\begin{enumerate}[label=\arabic*.] +\item Close the endpoint physical equivalence and global deficit reindexing. +\item Promote Theorem~\ref{thm:phase-gap}, Corollary~\ref{cor:uniform}, and +Corollary~\ref{cor:complement} into the main paper. +\item Prove the near-root placement theorem, beginning with the explicit choice +$\theta_n=N^{-1/2}$. +\item Prove balance stability. +\item Certify the exact four-support phase minimum. +\item Choose between the slowly growing support program and the matching upper +bound as the main separate-paper project. +\end{enumerate} + +\end{document} From 39966b8ca484f98a0d74ceb1e857226a80824879 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:28:34 +0300 Subject: [PATCH 3/8] Add the exact coefficient and placement regression ledger --- .../erdos625_value_upgrade_constants.py | 212 ++++++++++++++++++ 1 file changed, 212 insertions(+) create mode 100644 625/research/erdos625_value_upgrade_constants.py diff --git a/625/research/erdos625_value_upgrade_constants.py b/625/research/erdos625_value_upgrade_constants.py new file mode 100644 index 00000000..9b55f22e --- /dev/null +++ b/625/research/erdos625_value_upgrade_constants.py @@ -0,0 +1,212 @@ +#!/usr/bin/env python3 +"""Numerical regression ledger for the Erdős 625 value-upgrade program. + +The script uses only Python's standard library. It verifies the deterministic +coefficient propagation formulas recorded in the research note and prints +quantitative diagnostics for near-root placement and sign-balance penalties. + +It does not prove the four-support entropy certificate, the phase minimum, the +normalized second moment, or any random-graph theorem. Those are mathematical +inputs or explicitly labelled research targets. +""" + +from __future__ import annotations + +from decimal import Decimal, getcontext + + +getcontext().prec = 90 + + +D = Decimal + + +def require(condition: bool, message: str) -> None: + """Raise an explicit error; unlike assert, this remains active under -O.""" + + if not condition: + raise RuntimeError(message) + + +def binary_entropy(rho: Decimal) -> Decimal: + """Natural-log binary entropy on the open unit interval.""" + + require(D(0) < rho < D(1), f"rho must lie in (0,1), got {rho}") + return -(rho * rho.ln() + (D(1) - rho) * (D(1) - rho).ln()) + + +def coefficient_ledger() -> dict[str, Decimal]: + q = D(2).ln() + + canonical = q * q * (D(200) / D(153)).ln() / D(32) + factor_four_old_entropy = q * q * (D(200) / D(153)).ln() / D(8) + stronger_entropy_old_propagation = q * q * (D(1000) / D(639)).ln() / D(32) + certified_midpoint = q * q * (D(1000) / D(639)).ln() / D(8) + certified_near_root = q * q * (D(1000) / D(639)).ln() / D(4) + + full_support_midpoint = q**3 / D(8) + full_support_near_root = q**3 / D(4) + + diagnostic_advantage = D("0.520701335491") + diagnostic_midpoint = q * q * diagnostic_advantage / D(8) + diagnostic_near_root = q * q * diagnostic_advantage / D(4) + + require( + factor_four_old_entropy == canonical * D(4), + "factor-four propagation identity failed", + ) + require( + certified_midpoint == stronger_entropy_old_propagation * D(4), + "stronger-entropy factor-four identity failed", + ) + require( + certified_near_root == certified_midpoint * D(2), + "near-root/midpoint factor-two identity failed", + ) + require( + full_support_near_root == full_support_midpoint * D(2), + "full-support near-root/midpoint identity failed", + ) + require( + full_support_near_root + > diagnostic_near_root + > certified_near_root + > full_support_midpoint + > diagnostic_midpoint + > certified_midpoint + > factor_four_old_entropy + > stronger_entropy_old_propagation + > canonical + > 0, + "coefficient ordering failed", + ) + + return { + "q=ln(2)": q, + "canonical": canonical, + "PR31 only (old entropy, /8)": factor_four_old_entropy, + "PR32 only (strong entropy, /32)": stronger_entropy_old_propagation, + "certified midpoint (/8)": certified_midpoint, + "certified near-root (/4)": certified_near_root, + "diagnostic four-support midpoint": diagnostic_midpoint, + "diagnostic four-support near-root": diagnostic_near_root, + "full-support midpoint limit": full_support_midpoint, + "full-support near-root limit": full_support_near_root, + "certified midpoint / canonical": certified_midpoint / canonical, + "certified near-root / canonical": certified_near_root / canonical, + } + + +def placement_diagnostics() -> list[tuple[int, Decimal, Decimal, Decimal]]: + """Check the explicit theta_N=N^{-1/2} buffer criterion. + + If the root-scale buffer is theta_N*n/N^3 and the error scale is n/N^4, + their ratio is theta_N*N=sqrt(N). The returned rows record N, theta_N, + theta_N*N, and the retained deterministic fraction 1-theta_N. + """ + + rows: list[tuple[int, Decimal, Decimal, Decimal]] = [] + previous_ratio: Decimal | None = None + previous_theta: Decimal | None = None + + for nlog in (16, 64, 256, 1024, 4096, 16384): + N = D(nlog) + theta = D(1) / N.sqrt() + ratio = theta * N + retained = D(1) - theta + + require(D(0) < theta < D(1), f"invalid theta at N={N}") + require(ratio > D(1), f"buffer does not dominate error at N={N}") + require(D(0) < retained < D(1), f"invalid retained fraction at N={N}") + + if previous_ratio is not None: + require(ratio > previous_ratio, "theta_N*N is not increasing") + require(theta < previous_theta, "theta_N is not decreasing") + + previous_ratio = ratio + previous_theta = theta + rows.append((nlog, theta, ratio, retained)) + + require(rows[-1][2] >= D(100), "buffer ratio is not strongly divergent") + return rows + + +def balance_penalties() -> list[tuple[Decimal, Decimal, Decimal]]: + """Compute entropy losses and their formal root-scale coefficients. + + The coefficient q^2/4*(log 2-H(rho)) is a deterministic diagnostic for the + proposed first-moment balance-stability theorem. It is not a proved random + graph bound until the refined profile union bound is written. + """ + + q = D(2).ln() + rows: list[tuple[Decimal, Decimal, Decimal]] = [] + + for epsilon_text in ("0.01", "0.025", "0.05", "0.10", "0.20", "0.30"): + epsilon = D(epsilon_text) + rho = D("0.5") + epsilon + loss = q - binary_entropy(rho) + coefficient = q * q * loss / D(4) + require(loss > 0, f"entropy loss not positive at epsilon={epsilon}") + require(coefficient > 0, f"root penalty not positive at epsilon={epsilon}") + rows.append((epsilon, loss, coefficient)) + + for previous, current in zip(rows, rows[1:]): + require(current[1] > previous[1], "entropy loss is not increasing") + require(current[2] > previous[2], "root penalty is not increasing") + + return rows + + +def theta_coefficient(theta: Decimal, advantage: Decimal) -> Decimal: + """Formal retained coefficient (1-theta) q^2 advantage / 4.""" + + require(D(0) <= theta <= D(1), f"theta outside [0,1]: {theta}") + require(advantage >= 0, f"negative advantage: {advantage}") + q = D(2).ln() + return (D(1) - theta) * q * q * advantage / D(4) + + +def placement_coefficient_table() -> list[tuple[str, Decimal]]: + advantage = (D(1000) / D(639)).ln() + rows = [ + ("midpoint theta=1/2", theta_coefficient(D("0.5"), advantage)), + ("quarter placement theta=1/4", theta_coefficient(D("0.25"), advantage)), + ("theta=1/10", theta_coefficient(D("0.1"), advantage)), + ("formal theta->0 limit", theta_coefficient(D(0), advantage)), + ] + require(rows[0][1] < rows[1][1] < rows[2][1] < rows[3][1], + "placement coefficients are not ordered") + return rows + + +def main() -> None: + coefficients = coefficient_ledger() + placements = placement_diagnostics() + balance = balance_penalties() + placement_coefficients = placement_coefficient_table() + + print("ERDOS 625 VALUE-UPGRADE CONSTANT LEDGER: PASS") + print("\nCoefficient ledger") + for name, value in coefficients.items(): + print(f" {name}: {value}") + + print("\nCertified placement coefficients") + for name, value in placement_coefficients: + print(f" {name}: {value}") + + print("\nNear-root buffer diagnostics") + print(" N | theta=N^(-1/2) | theta*N | retained fraction") + for nlog, theta, ratio, retained in placements: + print(f" {nlog} | {theta} | {ratio} | {retained}") + + print("\nSign-balance entropy diagnostics") + print(" epsilon | log(2)-H(1/2+epsilon) | formal q^2/4 penalty") + for epsilon, loss, coefficient in balance: + print(f" {epsilon} | {loss} | {coefficient}") + + print("\nScope: deterministic coefficient arithmetic and diagnostics only") + + +if __name__ == "__main__": + main() From 36b26b330b5ef9c69f7395724b6d8b8cc2271758 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:29:05 +0300 Subject: [PATCH 4/8] =?UTF-8?q?Index=20the=20Erd=C5=91s=20625=20post-proof?= =?UTF-8?q?=20research=20program?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- 625/research/README.md | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 625/research/README.md diff --git a/625/research/README.md b/625/research/README.md new file mode 100644 index 00000000..64a2b737 --- /dev/null +++ b/625/research/README.md @@ -0,0 +1,38 @@ +# Erdős 625 research program + +This directory separates the validation of the 12 July 2026 candidate proof +from theorem-strengthening and follow-up-paper research. + +## Files + +- [`ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md`](ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md) + is the comprehensive chronology, proof-frontier, theorem-upgrade, and + publication-strategy document. +- [`ERDOS625_VALUE_UPGRADE_THEOREMS.tex`](ERDOS625_VALUE_UPGRADE_THEOREMS.tex) + contains copy-ready theorem statements and proof blueprints. Conditional + results and new targets are explicitly distinguished. +- [`erdos625_value_upgrade_constants.py`](erdos625_value_upgrade_constants.py) + checks the deterministic coefficient ledger, near-root buffer criterion, and + sign-balance entropy diagnostics under ordinary and optimized Python. + +## Status discipline + +The research program uses four labels: + +1. kernel-checked finite theorem; +2. conditional corollary of the candidate proof; +3. new theorem target; +4. exploratory separate-paper program. + +The directory does not alter `Erdos625Statement`, the canonical manuscript, or +the public status of Problem 625. + +## Recommended order + +1. finish the endpoint physical equivalence and aggregate deficit reindexing; +2. close the normalized second moment and external verification; +3. promote the phase-resolved `/8` theorem and stronger entropy constant; +4. prove near-root placement with `theta_n=(log n)^(-1/2)`; +5. prove balance stability; +6. pursue either slowly growing support or the matching upper bound as the + major follow-up project. From 2c217e41e12f42a9db78b1431def2eaf977671d1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:29:25 +0300 Subject: [PATCH 5/8] =?UTF-8?q?Add=20CI=20for=20the=20Erd=C5=91s=20625=20v?= =?UTF-8?q?alue-upgrade=20dossier?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../erdos625-value-upgrade-program.yml | 100 ++++++++++++++++++ 1 file changed, 100 insertions(+) create mode 100644 .github/workflows/erdos625-value-upgrade-program.yml diff --git a/.github/workflows/erdos625-value-upgrade-program.yml b/.github/workflows/erdos625-value-upgrade-program.yml new file mode 100644 index 00000000..1d44c5cc --- /dev/null +++ b/.github/workflows/erdos625-value-upgrade-program.yml @@ -0,0 +1,100 @@ +name: Erdős 625 value-upgrade research program + +on: + pull_request: + paths: + - "625/research/**" + - ".github/workflows/erdos625-value-upgrade-program.yml" + workflow_dispatch: + +concurrency: + group: erdos625-value-upgrade-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + research-dossier-check: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + + - name: Compile the coefficient ledger + run: python -m py_compile 625/research/erdos625_value_upgrade_constants.py + + - name: Run the coefficient ledger + run: python 625/research/erdos625_value_upgrade_constants.py + + - name: Run the coefficient ledger with optimization + run: python -O 625/research/erdos625_value_upgrade_constants.py + + - name: Check theorem-dossier structure and status markers + run: | + python - <<'PY' + from pathlib import Path + + md = Path("625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md") + tex = Path("625/research/ERDOS625_VALUE_UPGRADE_THEOREMS.tex") + readme = Path("625/research/README.md") + + for path in (md, tex, readme): + if not path.is_file(): + raise SystemExit(f"missing required research file: {path}") + + md_text = md.read_text(encoding="utf-8") + tex_text = tex.read_text(encoding="utf-8") + + md_markers = ( + "Public chronology and claim scope", + "Current proof frontier", + "New theorem target I: remove the midpoint loss", + "High-upside extension: slowly growing support", + "Largest follow-up target: prove the matching upper bound", + "Recommended publication architecture", + ) + tex_markers = ( + r"\begin{theorem}[Phase-resolved full-sequence gap]", + r"\begin{conjecture}[Near-root placement theorem]", + r"\begin{conjecture}[Balance stability]", + r"\begin{conjecture}[Slow-support gap]", + r"\begin{program}[Full upper bound]", + ) + + missing_md = [marker for marker in md_markers if marker not in md_text] + missing_tex = [marker for marker in tex_markers if marker not in tex_text] + if missing_md: + raise SystemExit(f"missing Markdown markers: {missing_md}") + if missing_tex: + raise SystemExit(f"missing TeX markers: {missing_tex}") + + forbidden_typos = (r"o\!left", r"\log2") + for typo in forbidden_typos: + if typo in md_text or typo in tex_text: + raise SystemExit(f"known TeX typo remains: {typo}") + + if tex_text.count(r"\begin{document}") != 1: + raise SystemExit("TeX file must have exactly one begin{document}") + if tex_text.count(r"\end{document}") != 1: + raise SystemExit("TeX file must have exactly one end{document}") + + # Lightweight brace check that ignores escaped braces. + depth = 0 + index = 0 + while index < len(tex_text): + char = tex_text[index] + if char == "\\": + index += 2 + continue + if char == "{": + depth += 1 + elif char == "}": + depth -= 1 + if depth < 0: + raise SystemExit("TeX has a premature closing brace") + index += 1 + if depth != 0: + raise SystemExit(f"TeX brace depth is {depth}, expected zero") + + print("research dossier structure: PASS") + PY From 9b024fb4c4a094d5148674c2fe777aa5e313861e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:30:15 +0300 Subject: [PATCH 6/8] Allow standard TeX command adjacency in the dossier check --- .github/workflows/erdos625-value-upgrade-program.yml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/.github/workflows/erdos625-value-upgrade-program.yml b/.github/workflows/erdos625-value-upgrade-program.yml index 1d44c5cc..ce03f4c1 100644 --- a/.github/workflows/erdos625-value-upgrade-program.yml +++ b/.github/workflows/erdos625-value-upgrade-program.yml @@ -68,10 +68,8 @@ jobs: if missing_tex: raise SystemExit(f"missing TeX markers: {missing_tex}") - forbidden_typos = (r"o\!left", r"\log2") - for typo in forbidden_typos: - if typo in md_text or typo in tex_text: - raise SystemExit(f"known TeX typo remains: {typo}") + if r"o\!left" in md_text or r"o\!left" in tex_text: + raise SystemExit(r"known TeX typo remains: o\!left") if tex_text.count(r"\begin{document}") != 1: raise SystemExit("TeX file must have exactly one begin{document}") From 99d7250237e60318a34317f242d3a8a428634f8b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:32:09 +0300 Subject: [PATCH 7/8] Correct and polish the value-upgrade mathematical dossier --- .../ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md b/625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md index 9428ad56..44bc3fd2 100644 --- a/625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md +++ b/625/research/ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md @@ -230,7 +230,7 @@ The single nonlocal denominator changes by \[ \frac{(n)_{J+H}}{(n)_J}=(n-J)_H\le n^H, - \qquad H=\sum_eh_e. + \qquad H=\sum_e h_e. \] Hence @@ -273,7 +273,7 @@ The repaired Section IX theorem then yields \[ \frac{\mathbb E Z_n^2}{(\mathbb E Z_n)^2} \le - \exp\!\left\{o\!left(\frac n{N^4}\right)\right\}. + \exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}. \] This is the exact closure route. Further cycle/polymer decompositions do not @@ -288,7 +288,7 @@ address the remaining seam. Let \[ - A_4(\delta)=\log2-D_4(\delta), + A_4(\delta)=\log 2-D_4(\delta), \] where `D_4` is the four-support entropy loss at phase `delta`. @@ -621,13 +621,13 @@ where The unrestricted sign entropy is `k log 2`. Thus an imbalance costs \[ - k\bigl(\log2-H(\rho)\bigr). + k\bigl(\log 2-H(\rho)\bigr). \] Near `rho=1/2+x`, \[ - \log2-H(1/2+x)=2x^2+O(x^4). + \log 2-H(1/2+x)=2x^2+O(x^4). \] Since the local derivative of the coloring first-moment logarithm with respect @@ -653,7 +653,7 @@ A quantitative local version should give \[ c(\epsilon) - =\frac{q^2}{4}\bigl(\log2-H(1/2+\epsilon)\bigr) + =\frac{q^2}{4}\bigl(\log 2-H(1/2+\epsilon)\bigr) +o_\epsilon(1) \] @@ -701,7 +701,7 @@ near-optimal cocoloring having For a fixed finite support `S`, the signed-root advantage is \[ - \frac{q^2}{4}\bigl(\log2-D_S(\delta_n)\bigr)H_n. + \frac{q^2}{4}\bigl(\log 2-D_S(\delta_n)\bigr)H_n. \] The four-size support has a strictly positive but nonzero truncation loss. @@ -987,7 +987,7 @@ two carries the exact factor \[ 2^{W+c(H)-|V(H)|} - =\left(\prod_eg(r_e)\right)2^{\beta(H)}. + =\left(\prod_e g(r_e)\right)2^{\beta(H)}. \] The topological correction is the binary cycle-space dimension. A `q`-template From 4d1b12206fefad3e65e6c32818fd4a0dbd2d82b6 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 08:33:13 +0300 Subject: [PATCH 8/8] =?UTF-8?q?Map=20the=20public=20Erd=C5=91s=20625=20PR?= =?UTF-8?q?=20stack=20by=20mathematical=20role?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../PUBLIC_PR_RESULT_MAP_2026-07-26.md | 334 ++++++++++++++++++ 1 file changed, 334 insertions(+) create mode 100644 625/research/PUBLIC_PR_RESULT_MAP_2026-07-26.md diff --git a/625/research/PUBLIC_PR_RESULT_MAP_2026-07-26.md b/625/research/PUBLIC_PR_RESULT_MAP_2026-07-26.md new file mode 100644 index 00000000..4a5ac975 --- /dev/null +++ b/625/research/PUBLIC_PR_RESULT_MAP_2026-07-26.md @@ -0,0 +1,334 @@ +# Public Erdős 625 PR result map + +**Cutoff:** 26 July 2026 +**Purpose:** distinguish the original public proof record, merged formalization bricks, later audit/simplification branches, and theorem-upgrade research + +This map is descriptive. An open PR is not treated as merged into `main`, and a +successful finite or focused check is not treated as a proof of +`Erdos625Statement`. + +--- + +## 1. Public proof chronology + +| PR | Date | Role | Status interpretation | +|---:|---|---|---| +| #1 | 12 Jul | Public verification bundle containing the candidate proof | Earliest explicit public PR timestamp for the candidate proof; provisional internal verification only | +| #2 | 12 Jul | Source audit, styled proof, release archive | Historical/source validation; no external proof verification | +| #3 | 12 Jul | Manuscript citations and current verification record | Bibliographic and presentation work | +| #4 | 12 Jul | Adversarial leap audit and written-proof repair | Substantive internal repair; theorem still candidate | +| #5 | 12 Jul | Exact finite illustrative animation | Expository only | +| #6 | 13 Jul | Synchronize proof components and traceability | Consolidation; no new theorem claim | + +Public chronology anchor: + +```text +PR #1 created: 2026-07-12 19:08:31 UTC +PR #1 head: 945ed733af198fe8698e14079ddc079f2bc554d7 +PR #1 merged: 2026-07-12 19:29:28 UTC +``` + +--- + +## 2. Merged Lean/formalization progression + +### Model, probability, phase, and first moment + +| PR | Main mathematical content | +|---:|---| +| #7 | Exact finite graph/cocoloring model, `zeta<=chi`, random graph law, definition of `Erdos625Statement` | +| #8 | Phase/floor arithmetic, independent-set first moment, Markov/Paley--Zygmund, Boolean-cube bounded differences | +| #9 | Vertex-block concentration, cochromatic induced capacity, rare-seed inversion and amplification infrastructure | +| #10 | Exact bounded-profile enumeration and first-moment formula | +| #11 | Finite profile duality, variational calculus, chromatic reduction | +| #12 | Growing-support analytic bricks, overlap foundations, first Section VIII atoms | + +### Exact overlap/configuration-model counting + +| PR | Main mathematical content | +|---:|---| +| #13 | Citation refresh and first stub-allocation atom | +| #14 | Stub allocations, prescribed-demand numerator, matching-extension counts | +| #15 | Embedding matching extensions | +| #16 | Global row/column stubs and configuration-model witnesses | +| #17 | Large self-contained partial checkpoint; closed unmerged, later work continued elsewhere | +| #18--#21 | Successive integrated formalization checkpoints, including Section VIII/IX and amplification bricks | + +### Manuscript and accepted arithmetic leaves + +| PR | Main mathematical content | +|---:|---| +| #22 | Rewritten and synchronized Problem 625 manuscript | +| #23 | Public artifact synchronization and updated Steiner citation | +| #24 | Checked Section IX finite arithmetic leaves | +| #25 | Small/large residual asymptotic scale adapters | +| #28 | Phase-root and midpoint formalization checkpoint | +| #29 | Derivative affine-core error bound | + +PR #26 concerns Problem 593 and does not affect Problem 625. + +--- + +## 3. Broad review and theorem-upgrade line + +### PR #27: research notebook + +PR #27 is a broad draft notebook containing corrected Section VII--IX notes, +experiments, and several possible theorem extensions. It is useful as a source +of ideas but should not be merged wholesale into the canonical proof without +splitting and rechecking its claims. + +Surviving ideas were extracted into narrower PRs. + +### PR #30: verified Section VII and IX simplifications + +Main results: + +1. stronger central partial-diagonal rate on the same domain; +2. direct injection + \[ + F\mapsto F\setminus M + \] + on even edge sets after exposing a matching; +3. replacement of the large-residual cycle/walk enumeration by + \[ + \sum_F\prod_{e\in F\setminus M}q_e + \le\prod_{e\notin M}(1+q_e). + \] + +This was later formalized and integrated through PRs #34--#37. + +### PR #31: root-gap constant propagation + +Conditional deterministic result: + +\[ + r_+-r_4^{\mathrm{co}} + =\left(\frac{q^2}{4}A_4(\delta_n)+o(1)\right) + \frac n{(\log n)^3} +\] + +and midpoint placement retains one half, giving `/8`, not `/32`, in the final +coefficient. The PR verifies rounding and propagation, not the full second +moment. + +### PR #32: stronger four-support entropy certificate + +Exact certificate: + +\[ + D_4(\delta)<\log(639/500), + \qquad + A_4(\delta)>\log(1000/639) +\] + +uniformly in the limiting phase interval. + +Combined with PR #31, the conditional uniform coefficient is + +\[ + \frac{q^2}{8}\log(1000/639) + =0.026896409808379\ldots. +\] + +### PR #33: support-frontier diagnostic + +The finite grid scan reports approximately + +```text +{2,3,4,5,6}: 0.525994631053 +{2,3,4,5}: 0.520701335491 +``` + +so the fifth size gains only about `1.017%` while increasing the endpoint +transport dimension. This is numerical evidence, not a certified support +optimality theorem. + +--- + +## 4. Focused Section IX closure line + +### PR #34: finite matching-restriction product + +Kernel-checked finite statements: + +- deletion of an exposed matching is injective on even bipartite edge sets; +- weighted even-family sum is bounded by the full residual subset product; +- the fixed-family residual sum is bounded by the local-increment product times + the residual-q product. + +The cumulative audit later extracts the generic theorem: + +\[ + \sum_{A\in\mathcal C}\prod_{e\in A\setminus I}q_e + \le\prod_{e\notin I}(1+q_e) +\] + +whenever deletion of `I` is injective on the finite family `C`. + +### PR #35: direct actual-attachment envelope + +Carries PR #34 through the literal capped attachment numerator and proves a +profile-level large-residual envelope of order + +\[ + \exp\{O((\log n)^2)\}. +\] + +### PR #37: q-only two-regime attachment theorem + +Uses + +\[ + \lambda_{ab}\le q_{ab} +\] + +so both products are controlled by one total-q sum. It proves, over the literal +attained attachment sum, + +\[ + \operatorname{AttachmentSum}_n + \le + \operatorname{BareSkeletonSum}_n + \exp\left\{\varepsilon_n\frac n{(\log n)^4}\right\}, + \qquad\varepsilon_n\to0. +\] + +The focused source branch was repaired and built successfully. PR #40 merged +this Section IX stack into the cumulative audit branch. + +--- + +## 5. Focused Section VIII closure line + +### PR #36: endpoint transport core + +Kernel-checks the square-free, denominator-free form of the endpoint +transportation inequality. This is the exact finite algebra behind manuscript +Lemma 8.1. + +### PR #38: AM--GM and all-high-deficit simplification + +Replaces the Cauchy/table-family route by square-free AM--GM and one-sided +multinomial sums. It also replaces near/middle high-cell ranges by one +all-deficit geometric expansion using + +\[ + h\left\lfloor\frac{2m}{3}\right\rfloor + \le hm-\frac{h(h+1)}2. +\] + +The paper-level resulting exponent is + +\[ + O\bigl(n^{2/3}(\log n)^{4/3}\bigr) + +O\bigl(\sqrt{n\log n}\bigr) + =o\left(\frac n{(\log n)^4}\right). +\] + +### PR #39: cumulative theorem/lemma audit + +PR #39 integrates the Section VIII and Section IX simplification lines and +records the authoritative theorem frontier: + +- Sections II--VII and X are structurally coherent; +- Section IX is reduced to the Section VIII bare-skeleton estimate; +- one global Section VIII physical-fibre/deficit theorem remains decisive; +- `Erdos625Statement` remains unproved. + +It also contains the phase-resolved theorem, stronger coefficient, complement +corollary, balanced seed, reusable restriction-product theorem, and exact +regression ledger. + +### PR #40: mechanical branch integration + +Merged PRs #34, #35, and #37 into the head of PR #39. It makes no new +mathematical claim. + +### PR #41: exact endpoint reference normalization + +PR #41 proves: + +1. the combined block-pairing and full-stub factorial quotient; +2. the common signed endpoint atom weight; +3. exact identification of the decorated sum with `fourEndpointW(L)`; +4. injectivity of the decorated-to-physical endpoint map. + +It also contains a candidate reverse-data construction. That newest reverse +module must be directly built and audited before it is treated as proved. + +The remaining endpoint task is surjectivity/two round trips. The remaining +global task is the aggregate all-deficit reindexing. + +--- + +## 6. Current integration graph + +The focused proof stack is + +```text +#34 -> #35 -> #37 + \ + #40 -> #39 -> #41 -> current value-upgrade PR + / +#36 -> #38 ---- +``` + +The theorem-upgrade PRs #31 and #32 were created independently from `main`. +Their mathematics is summarized and regression-checked in the cumulative audit, +but they should be cherry-picked or restated deliberately rather than merged +blindly with unrelated branch history. + +PR #33 is diagnostic and need not be part of the canonical proof history. + +--- + +## 7. Result classification + +### Already finite/kernel checked + +- exact graph and cochromatic definitions; +- many first-moment and phase-expansion bricks; +- exact signed overlap/cycle-space algebra; +- prescribed-demand and configuration-model finite counts; +- endpoint transport core; +- matching-restriction product; +- q-only literal attachment theorem; +- endpoint decorated reference normalization; +- decorated-to-physical endpoint injectivity; +- rare-seed concentration and deterministic completion infrastructure. + +### Conditional on the remaining global Section VIII theorem + +- Proposition 9.2; +- full-sequence `Omega(n/(log n)^3)` gap; +- phase-resolved `/8` coefficient; +- uniform coefficient `0.026896409808379...`; +- simultaneous complement corollary; +- balanced rare seed at the same exponential scale. + +### New research targets + +- near-root placement and `/4` coefficient; +- exact phase minimum of `A_4`; +- balance necessity for near-optimal cocolorings; +- slowly growing support and limiting coefficient `(ln 2)^3/4`; +- matching `O(n/(log n)^3)` upper bound; +- fixed-`p` extension; +- two-independent-graph alternative model. + +--- + +## 8. Review policy + +For every future PR, the description should state separately: + +1. what theorem is proved in the PR itself; +2. which manuscript statements it assumes; +3. whether the result is finite, asymptotic, computational, or diagnostic; +4. whether the exact focused target is compiled by CI; +5. whether the PR changes the canonical theorem statement; +6. whether it changes the external claim status. + +No green root build should be used to certify a newly added isolated Lean module +unless that module lies in the root import closure or has its own focused build.