From 34e902ebbec1cf21cc403e32915be249f6f5b2b3 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 17:38:12 +0300 Subject: [PATCH 1/6] =?UTF-8?q?Add=20the=20full=20mathematical=20re-audit?= =?UTF-8?q?=20of=20the=20Erd=C5=91s=20625=20TeX?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...ULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md | 699 ++++++++++++++++++ 1 file changed, 699 insertions(+) create mode 100644 625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md diff --git a/625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md b/625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md new file mode 100644 index 00000000..6534247f --- /dev/null +++ b/625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md @@ -0,0 +1,699 @@ +# Full mathematical re-audit of the Erdős 625 TeX + +**Date:** 26 July 2026 +**Audited source:** `625/arxiv/main.tex` on `agent/625-value-upgrade-program` +**Source blob:** `c4d090b73cd5efcdb98cc30f79bb5f53c6c9bc97` +**Scope:** every section from the phase expansion through the final event intersection, together with the theorem upgrades proposed in PR #43 + +## 0. Status vocabulary + +This audit uses five labels. + +- **GREEN:** no new mathematical defect was found in the stated argument, subject to its declared inputs. +- **AMBER:** the idea is plausible or correct at fixed parameters, but a quantitative uniformity statement is still missing for the proposed extension. +- **RED:** the canonical TeX currently relies on a global identification or estimate that has not been supplied by the checked public/private proof stack. +- **BLUE:** a theorem-strength or proof-simplification improvement that should be incorporated after closure. +- **TYPO:** a source-level mathematical notation error that should be corrected even though the intended formula is clear. + +A GREEN label is not external peer review and is not a claim that the corresponding section has been completely formalized in Lean. + +--- + +## 1. Executive verdict + +### 1.1 The unique submission-blocking proof seam remains Section VIII + +The decisive unresolved theorem is the **weight-preserving physical-fibre and all-deficit reindexing** behind Lemma 8.3. The canonical TeX moves from a partial high physical matching to a full-containment reference table as though the relevant objects were obtained by independently decorating distinguished full cells. A partial physical stub matching generally has many full completions, and some of its unused stubs may participate in residual cells. Therefore the required argument is not an objectwise completion bijection. + +The correct statement is aggregate. For a fixed block-level matching support `P`, endpoint multiplicities `m_e`, deficits `h_e`, and actual multiplicities `j_e=m_e-h_e`, one must first sum the partial physical stub-matching fibre. Its 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. +\] + +The exact one-cell aggregate ratio is + +\[ + R_{m,d}(h)= + \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)} + 2^{-hm+h(h+1)/2}, +\] + +and the single global denominator ratio is + +\[ + \frac{(n)_{J+H}}{(n)_J}=(n-J)_H\le n^H, + \qquad H=\sum_eh_e. +\] + +Only after establishing the exact finite reindexing may one conclude + +\[ + \frac{w(P,m-h)}{w_{\rm full}(P)} + \le\prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e). +\] + +PR #41 closes the full-endpoint reference normalization and proves injectivity of the decorated-to-physical map. A candidate reverse-data construction exists, but the reverse map, its round trips, and the global partial-deficit fibre identity are not yet accepted. The private DAG independently identifies this same seam and rejects a generic subexponential-sum wrapper as insufficient. + +**Verdict:** Lemma 8.3, Proposition 9.2, and the main theorem remain conditional until this finite global theorem is checked. + +### 1.2 No second independent fatal gap was found outside that seam + +Sections 2--7 and 10--11 form a coherent dependency chain when Proposition 9.2 is supplied. The exact signed-overlap identity, partial-diagonal recurrence architecture, chromatic lower reduction, and rare-seed amplifier remain mathematically compatible with the newer Section VIII--IX route. + +This does not mean that the existing Section VIII--IX prose should be retained. The canonical TeX still presents the older near/middle and cycle-kernel proofs. The newer aggregate all-deficit and matching-restriction route is shorter, more exact, and better aligned with the checked finite modules. + +### 1.3 Three proposed upgrades in PR #43 need narrower statements + +1. **Near-root placement:** `theta_n log n -> infinity` is presently only a proposed sufficient criterion. The exact placement dependence of every use of the positive first-moment margin has not yet been collected in one theorem. The candidate `theta_n=(log n)^(-1/2)` remains plausible, but the roadmap must not present the criterion as established before the replay is done. +2. **Balance necessity:** replacing `2^k` by `binom(k,rho k)` proves a stability statement inside the selected four-size signed witness family. It does not exclude arbitrary imbalanced cocolorings using different class-size profiles. Global necessity requires a first-moment union bound over all signed profiles. +3. **Slow-support complexity:** if a dimension-dependent second-moment exponent is written as `K(m)n/(log n)^4`, then `K(m_n)=o(log n)` is not enough. The required condition is directly `Lambda(n,m_n)=o(n/(log n)^4)`. A complexity envelope must be compared with the actual smaller fixed-support error scale, not multiplied by the target scale itself. + +### 1.4 The canonical theorem constant is unnecessarily weakened + +The source loses fixed factors after the phase-resolved root displacement. The correct midpoint propagation is + +\[ + \chi(G_n)-\zeta(G_n) + \ge + \left[ + \frac{(\ln2)^2}{8}\bigl(\ln2-D_4(\delta_n)\bigr)-o(1) + \right]\frac{n}{(\ln n)^3}. +\] + +Combining this with the stronger exact entropy certificate gives + +\[ + \frac{(\ln2)^2}{8}\ln\!\left(\frac{1000}{639}\right) + =0.026896409808379\ldots, +\] + +about `6.68735` times the displayed coefficient in the canonical TeX. + +--- + +## 2. Section-by-section audit table + +| TeX layer | Verdict | Mathematical conclusion | Required action | +|---|---:|---|---| +| Abstract and Theorem 1 | RED/BLUE | The statement depends on the unresolved Section VIII global theorem; its coefficient is also weaker than necessary. | Keep candidate status until closure; then replace by the phase-resolved theorem and stronger corollary. | +| Section 1, elementary tools | GREEN | The stated Stirling, bounded-differences, Paley--Zygmund, binomial-tail, and Markov forms are compatible with later uses. | No mathematical rewrite required. | +| Section 2, complete phase | GREEN | The phase expansion and adjacent-size consequences are internally consistent and uniform on the attained phase interval. | Clarify that `delta=1` is used only as a continuous endpoint extension. | +| Section 3, continuous roots | GREEN for fixed placement; AMBER for shrinking placement | Root corridor, derivative, and support comparison are coherent. | For `theta_n->0`, collect a quantitative placement-uniform theorem rather than relying on a generic error slogan. | +| Section 4, chromatic lower location | GREEN | The bounded-profile first moment plus the independence-number cap removes the apparent profile restriction. | No structural change. | +| Section 5, signed first moment | GREEN/BLUE | The root displacement is the main phase-sensitive theorem. The later constant propagation is over-conservative. | Insert the stronger entropy certificate and retain the full `/8` midpoint coefficient. | +| Section 6, exact signed overlap | GREEN | The compatible-sign count and prescribed-cell bound are exact finite statements. | Promote the cycle-space identity as a named reusable proposition. | +| Section 7, partial diagonals | GREEN with one TYPO and one BLUE improvement | The empty/central/full corner architecture is coherent for the fixed midpoint profile. | Fix `2^ell_bullet`; replace decimal central-rate checks by the exact stronger rational certificate; expose placement dependence for `theta_n`. | +| Section 8, endpoint/high skeletons | RED | Full endpoint normalization is now checked, but the attained partial physical-fibre/all-deficit reindexing is missing. | Replace the old near/middle proof by the aggregate all-deficit theorem. | +| Section 9, residual attachments | GREEN on the newer q-only route; obsolete canonical route | The public q-only matching-restriction chain controls the literal attained attachment sum. | Replace cycle/walk enumeration by the direct restriction-product theorem and two-regime assembly. | +| Section 10, amplification | GREEN/BLUE | The one-Lipschitz capacity argument and simultaneous leftover coloring give the claimed tunable tail. | State the tunable tail as a named proposition. | +| Section 11, event intersection | GREEN conditional on Proposition 9.2; BLUE coefficient | The union-bound intersection is valid. | Use the phase-resolved coefficient and add the complement-symmetric corollary. | +| PR #43 near-root target | AMBER | Plausible; `theta=N^{-1/2}` is a strong candidate. | Replace the asserted criterion by an explicit list of quantities that must be `o(theta n/log n)` or uniform at `k_theta`. | +| PR #43 balance necessity | AMBER/overstated | Valid for the selected four-size witness family; not yet for arbitrary cocolorings. | Restrict the theorem or first prove an all-signed-profile lower location. | +| PR #43 slow support | AMBER/correction required | The limiting coefficient is plausible, but the complexity criterion is dimensionally wrong as written. | Require `Lambda(n,m_n)=o(n/(log n)^4)` directly. | +| PR #43 cochromatic corridor | AMBER/correction required | The present midpoint construction gives an upper location near the midpoint, not `r_4^co+o(H_n)`. | Make the latter conditional on the near-root theorem. | + +--- + +## 3. Abstract, introduction, and theorem statement + +### 3.1 Claim boundary + +The abstract says “We prove” the final full-sequence theorem. That wording becomes appropriate only after the Section VIII reindexing theorem has been supplied and the integrated proof has been independently reviewed. Until then, the repository should retain candidate-proof language outside the frozen manuscript. + +### 3.2 The theorem should be phase-resolved + +Let + +\[ + A_4(\delta)=\ln2-D_4(\delta), + \qquad H_n=\frac{n}{(\ln n)^3}. +\] + +The strongest theorem already latent in the fixed-midpoint architecture is + +\[ + \Pr\!\left( + \chi(G_n)-\zeta(G_n) + \ge\left[\frac{(\ln2)^2}{8}A_4(\delta_n)-o(1)\right]H_n + \right)\to1. +\] + +This statement preserves the genuine phase information. The uniform numerical constant should be a corollary, not the main theorem. + +### 3.3 Background additions + +The historical paragraph should eventually include the origin and generalized-coloring framework already identified in PR #41: + +- Lesniak--Straight for the cochromatic number; +- Erdős--Gimbel--Straight and Erdős--Gimbel--Kratsch for early extremal/comparison theory; +- Scheinerman and Bollobás--Thomason for generalized chromatic numbers of dense random graphs; +- Gimbel--Kündgen--Molloy only as adjacent fractional work. + +These are background improvements, not proof dependencies. + +### 3.4 Roadmap must match the new proof + +The introduction currently says that Section 8 treats near/middle high cells and Section 9 pays for cycle attachments by a separate cycle-kernel argument. A Version 2 roadmap should instead say: + +1. Section 8 identifies the exact physical high-skeleton fibres, compares every deficit to the full endpoint reference, and sums one all-high geometric product; +2. Section 9 uses injective restriction outside the exposed matching and one q-only two-regime estimate for the literal attained attachment sum. + +--- + +## 4. Sections 1--2: elementary estimates and the complete phase + +### 4.1 Elementary inequalities + +No incompatibility was found between the displayed forms and their uses. In particular: + +- Lemma 10.2 uses `n-1` independent vertex blocks, which is consistent with the general parameter `r` in the bounded-differences statement; +- the one-sided bounded-differences exponent used in (10.7)--(10.8) has the correct factor `2/(n-1)`; +- the lower-quarter binomial estimate is more than sufficient for Lemma 10.1. + +### 4.2 Phase endpoint convention + +The actual phase satisfies `0<=delta<1`. Lemma 5.1 and the research upgrades use the compact closure `[0,1]`. The paper should state once that all limiting phase functions extend continuously to `delta=1`; no integer `n` is asserted to attain that endpoint. + +### 4.3 Adjacent-size consequences + +The ratios + +\[ + \frac{\mu_{s+1}}{\mu_s}=\frac{n-s}{s+1}2^{-s}, + \qquad + \frac{\mu_{s-1}}{\mu_s}=\frac{s}{n-s+1}2^{s-1} +\] + +correctly give the upper independence-number cap and the lower first-moment scale needed in Section 7. No new gap was found here. + +--- + +## 5. Section 3: continuous roots + +### 5.1 Fixed-corridor argument + +The affine-plus-curved decomposition, Gaussian domination, bounded selected tilts, positive variance floor, and envelope derivative form a coherent proof of the root corridor and slope for fixed `c in [0,ln 2]`. + +### 5.2 Uniform support comparison + +For the four-size support, compact-uniform convergence of the optimizer and its positive coordinate floor is exactly what is needed for the finite integer correction in Section 5. For the unrestricted support, the Gaussian majorant controls the moving finite cutoff. + +### 5.3 New quantitative lemma needed for shrinking placement + +The proposed near-root theorem should not be reduced to the single sentence “all errors are `O(n/N^4)`.” Define the exact placement + +\[ + k_{\theta_n}=\left\lceil + r_4^{\rm co}+\theta_n(r_+-r_4^{\rm co}) + \right\rceil. +\] + +A complete uniformity theorem should list separately: + +1. the signed first-moment margin at `k_theta`, expected to be of order + \[ + \theta_n\frac nN; + \] +2. the finite profile/Stirling error, currently logarithmic; +3. the full-corner denominator `1/EZ`, which requires the preceding margin to dominate the polynomial number of residual profiles; +4. the normalized-second-moment error, which must remain `o(n/N^4)` uniformly in the moving profile; +5. the amplifier loss, which need only be `o(H_n)` for the final near-root coefficient. + +The candidate `theta_n=N^{-1/2}` leaves a very large first-moment margin `n/N^{3/2}` and is therefore plausible. What remains missing is the theorem that every Section 7--9 constant is uniform over that moving placement. + +--- + +## 6. Section 4: unrestricted chromatic lower location + +The logic is valid: + +1. profiles with exactly `k` nonempty parts and maximum size `alpha+1` are counted; +2. the number of bounded profiles contributes only `exp(O(N^2))`; +3. moving `ceil(N)` classes below the continuous root decreases the logarithmic first moment by order `N^3`; +4. on the event `alpha(G)<=alpha+1`, any coloring with at most `k` parts can be split to exactly `k` bounded nonempty parts. + +This is a genuine unrestricted lower bound, not merely a lower bound inside the chosen four-size profile family. + +--- + +## 7. Section 5: signed first moment and constants + +### 7.1 Stronger entropy certificate + +The old certificate + +\[ + D_4(\delta)<\ln(153/100) +\] + +should be replaced by the stronger exact certificate + +\[ + D_4(\delta)<\ln(639/500), + \qquad + A_4(\delta)>\ln(1000/639). +\] + +The newer proof uses rational interval bounds and should replace the longer decimal-tail calculation in the canonical TeX once reviewed. + +### 7.2 Correct coefficient ledger + +Equation (5.11) gives + +\[ + r_+-r_4^{\rm co} + =\left[\frac{(\ln2)^2}{4}A_4(\delta_n)+o(1)\right]H_n. +\] + +At the rounded midpoint, + +\[ + r_+-k_{\rm co} + =\left[\frac{(\ln2)^2}{8}A_4(\delta_n)+o(1)\right]H_n. +\] + +Subtracting `ceil(ln n)` and the amplifier's `o(H_n)` loss causes no further fixed halving. Therefore the fixed certified coefficient is + +\[ + \frac{(\ln2)^2}{8}\ln(1000/639), +\] + +not the `/32` coefficient currently displayed. + +### 7.3 Integer correction + +The corrections + +\[ + \Delta k_2=e_1-3e_0, + \qquad + \Delta k_3=2e_0-e_1 +\] + +solve both conservation equations exactly. Since every limiting coordinate is bounded away from zero, bounded corrections preserve nonnegativity. The tangent Hessian loss is `O(1/k)` and is negligible. + +### 7.4 Balanced seed is valid + +Restricting to exactly `floor(k/2)` clique labels costs at most a factor `k+1` in the first moment and `(k+1)^2` in the normalized second moment. This gives a balanced **rare seed** at the same exponential scale. Preservation under amplification is a separate theorem. + +--- + +## 8. Section 6: exact overlap representation + +### 8.1 Exact sign sum + +The support graph on cells of multiplicity at least two correctly encodes sign compatibility. The identity + +\[ + 2^{W+c(H)-|V(H)|} + =\left(\prod_{a,b}g(r_{ab})\right)2^{\beta(H)} +\] + +is exact, and the even-subgraph interpretation of `2^beta` is the binary cycle-space cardinality. + +### 8.2 Prescribed-cell estimate + +The row-stub choices, column-stub choices, local bijections, and one global falling factorial in (6.8) are correctly normalized. The later product majorant (6.9) is an upper bound and does not replace the exact denominator when exact cancellation is needed. + +### 8.3 Expository improvement + +The cycle-space identity and the generic restriction-product inequality should be stated as separate named finite propositions. This makes it transparent which parts are model-independent. + +--- + +## 9. Section 7: partial diagonals + +### 9.1 Source-level mathematical typo + +Equation (7.2) contains + +```tex +2^\ell_\bullet +``` + +but the intended factor is + +```tex +2^{\ell_\bullet}. +``` + +Without braces the TeX expression places `ell` in the superscript and the bullet in a subscript. This is a notation error even though the subsequent recurrence uses the intended quantity. + +### 9.2 Empty and full corners + +The forward recurrence is controlled by the large value of `mu_{alpha-2}` and its neighboring sizes. The reverse recurrence is controlled by the small first moment on at most `n/32` residual vertices. The polynomial number of four-coordinate residual profiles is absorbed by the positive signed first-moment margin. + +### 9.3 Central rate + +The entropy/Stirling reduction and the two linear bounds on `Phi_T` are coherent. The paper currently uses decimal endpoint checks and constants `1/5000` and `1/200`. PR #30 supplies an exact rational strengthening to `1/100` on the relevant central domain. The stronger exact certificate should replace the decimal prose. + +### 9.4 Placement dependence + +For a moving placement `theta_n`, the full-corner estimate no longer has a fixed `c_Z k` exponent. It has an exponent of expected order + +\[ + \theta_n\frac nN. +\] + +A near-root theorem must prove that this still dominates the polynomial profile count and every error used in the central estimate. For `theta_n=N^{-1/2}` it does, but this comparison has not yet been written as a theorem. + +--- + +## 10. Section 8: exact diagnosis and replacement + +### 10.1 What is already closed + +The checked stack now supplies: + +- the endpoint block-pairing factorial identity; +- the full-cell stub-matching cardinality; +- their combined quotient; +- the exact equality between the decorated endpoint reference sum and `W(L)`; +- injectivity of the decorated-to-physical endpoint map; +- the square-free endpoint transport inequality; +- the one-cell all-high deficit arithmetic; +- the generic optional-deficit product bound. + +Thus the endpoint factorial bookkeeping is no longer the issue. + +### 10.2 What is not closed + +The missing theorem must identify the actual attained physical high-skeleton family with the aggregate block-support/deficit/partial-stub parameterization and preserve its weight. Specifically, it must prove that summing the local partial physical fibres gives the aggregate formula `w(P,j)` and that the collection of all such fibres is a disjoint reindexing of the canonical high-skeleton sum. + +The reverse endpoint construction alone is not enough: nonendpoint deficits use partial local matchings, not the full local matchings of the endpoint fibre. + +### 10.3 Why the old near/middle prose should be removed + +The canonical proof says that one may distinguish full endpoint cells and independently assign deficits, with “no additional multiplicity.” That conclusion is true only after proving the aggregate fibre formula. It does not follow from an objectwise unique completion. + +The old proof also contains finite summation ranges of the form + +```text +j <= 3a/4 + O(1), +``` + +which are not exact finite statements. They must be replaced by typewise integer cutoffs, or eliminated by the single all-high route. + +Finally, Step IV bounds residual local and cycle factors inside a lemma whose contract says those factors are deferred to Section 9. Because those factors are at least one, the resulting inequality may still be an upper bound, but the stated division of labour is no longer literally true and the same residual structure is then charged again in Proposition 9.2. + +### 10.4 Recommended all-deficit replacement + +For every positive deficit with `2hk_n+C\left[ + \frac{\sqrt{n\Lambda_n}+\sqrt{nr}}{N}+n^{1/3}+1 + \right]\right) + \le e^{-r}+o(1) +\] + +should be promoted to a named proposition. It is a reusable output and not merely an intermediate estimate. + +--- + +## 13. Section 11: final theorem and corollaries + +### 13.1 Event intersection + +The intersection of the chromatic lower event and cochromatic upper event uses only a union bound; no independence is needed. This part is correct once Proposition 9.2 is available. + +### 13.2 Remove the two unnecessary fixed halvings + +The canonical route obtains a phase-resolved root gap, then replaces it by a half-sized uniform gap, takes a midpoint, and finally halves the resulting coefficient once more to absorb an `o(1)`. The final two conservative steps are unnecessary once uniform continuity and the exact entropy slack are stated. + +The Version 2 final theorem should retain + +\[ + \frac{(\ln2)^2}{8}A_4(\delta_n) +\] + +up to `o(1)`. + +### 13.3 Complement corollary + +Since `zeta(complement G)=zeta(G)` and `G(n,1/2)` is complement invariant, + +\[ + \min\{\chi(G_n),\chi(\overline G_n)\}-\zeta(G_n) + \ge c\frac n{N^3} +\] + +holds with high probability for every certified main-theorem coefficient `c`. + +--- + +## 14. Audit of the proposed new theorem programs + +### 14.1 Near-root placement: retain as AMBER + +The deterministic placement formula is exact and the final retained gap approaches the full root displacement when `theta_n->0`. The candidate `theta_n=N^{-1/2}` is conservative. The missing work is not a new entropy calculation; it is a uniform replay of the fixed positive first-moment margin through Sections 7--9. + +The roadmap should define an explicit margin + +\[ + M_n(\theta)= + L_{S_4}(n,k_\theta)+(\ln2)k_\theta + \asymp\theta\frac nN +\] + +and list every proof error that must be `o(M_n(theta))` or uniform at the moving profile. Until this is done, `theta_nN->infinity` is a proposed sufficient criterion, not a proved lemma. + +### 14.2 Balance stability: restrict the current theorem + +The calculation with `binom(k,rho k)` proves: + +> Among the chosen four-size signed profiles, a fixed imbalance in the sign labels shifts the signed first-moment root by a positive multiple of `H_n`. + +It does not prove: + +> Every arbitrary cocoloring within `o(H_n)` of the global optimum is balanced. + +The latter requires excluding all alternative class-size profiles. That is an all-signed-profile first-moment theorem and belongs with the lower-location half of the matching-upper-bound project. + +The immediate rigorous structural program is therefore: + +1. balanced rare seed; +2. labelled-slot amplifier producing one near-optimal balanced cocoloring; +3. four-size witness-family stability; +4. global balance necessity only after all-profile exclusion. + +### 14.3 Slowly growing support: correct the complexity condition + +The target condition is + +\[ + \Lambda(n,m_n)=o(n/N^4), +\] + +where `Lambda(n,m)` is the logarithm of the normalized second-moment bound for support width `m`. + +If one proves + +\[ + \Lambda(n,m)\le K(m)B_n +\] + +for a fixed-support error scale `B_n=o(n/N^4)`, then choose `m_n` so that + +\[ + K(m_n)B_n=o(n/N^4). +\] + +Writing `Lambda=O(K(m)n/N^4)` and imposing only `K(m_n)=o(N)` is insufficient; it would generally be larger than the required target scale. + +The support itself must also be specified. A natural first choice is + +\[ + S_m=\{-1,0,1,\ldots,m\}, +\] + +with `m=o(alpha)`, rather than the ambiguous phrase “m consecutive sizes.” + +### 14.4 Cochomatic location corridor: make the upper side conditional + +The present midpoint construction gives + +\[ + \zeta(G_n) + \le + \frac{r_4^{\rm co}(n)+r_+(n)}2+o(H_n), +\] + +not + +\[ + \zeta(G_n)\le r_4^{\rm co}(n)+o(H_n). +\] + +The latter follows only after a near-root placement theorem. The proposed corridor must therefore be split: + +- current midpoint upper location, conditional on proof closure; +- near-root upper location, conditional on the new placement theorem; +- all-profile lower location, a separate new theorem. + +### 14.5 Exact phase minimum + +The envelope derivative formula is correct. Since + +\[ + T_0'(\delta)=-1, +\] + +the sign of `A_4'` is the sign of `lambda_4-lambda_infinity`. Directed interval arithmetic over finitely many target intervals is a credible rigorous route. The numerical value remains diagnostic. + +### 14.6 General density and two-layer model + +The one-class first-moment reward for `G(n,p)` is correct, but it should use notation different from the current local overlap factor `g(x)`. The overlap calculation becomes a component partition function with a size-dependent external field. + +The two-independent-graph model has the same witness first moment but a different second moment. It must remain explicitly attributed and separate until the coupling and normalized moment are obtained from a primary source or proved in the paper. + +--- + +## 15. Recommended Version 2 architecture + +1. **Theorem statement:** phase-resolved `/8` theorem, stronger fixed constant as corollary, complement corollary. +2. **Sections 2--4:** retain, with only minor uniformity clarifications. +3. **Section 5:** replace the old entropy certificate; correct constant propagation; optionally add the balanced seed. +4. **Section 6:** retain exact sign and prescribed-cell identities; isolate reusable finite propositions. +5. **Section 7:** fix the TeX exponent, use the exact stronger central-rate certificate, and state placement dependence explicitly. +6. **Section 8:** replace all near/middle prose by the exact physical-fibre equivalence, aggregate local ratio, all-deficit geometric product, and endpoint AM--GM transport. +7. **Section 9:** replace cycle/walk enumeration by the matching-restriction q-only two-regime theorem. +8. **Section 10:** retain and promote the tunable tail. +9. **Section 11:** retain the union-bound intersection, insert the phase-resolved coefficient and corollaries. + +This would shorten the technically most vulnerable part of the paper while strengthening its theorem. + +--- + +## 16. Acceptance checklist before canonical rewrite + +The canonical TeX should not be rewritten around the stronger theorem until the following are green on one integrated branch: + +1. reverse endpoint physical-fibre map and both round trips; +2. exact partial-cell physical fibre and its cardinality/weight identity; +3. disjoint global reindexing of every attained canonical high skeleton; +4. aggregate deficit comparison with the single global denominator; +5. all-deficit product at the actual midpoint profile; +6. endpoint AM--GM summation at the actual table/margin types; +7. direct literal q-only attachment theorem; +8. exact normalized-second-moment composition; +9. line-by-line constant propagation from the phase root to the final event; +10. manuscript compilation, bibliography, equation-reference, and source-sync checks. + +The stronger fixed coefficient, complement corollary, and tunable tail require no new random-graph mechanism after these gates are closed. From 9b225be382dcc250d13745538816955eb26e1737 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 17:39:53 +0300 Subject: [PATCH 2/6] Add the canonical Version 2 mathematical rewrite specification --- .../CANONICAL_V2_REWRITE_SPEC_2026-07-26.md | 433 ++++++++++++++++++ 1 file changed, 433 insertions(+) create mode 100644 625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md diff --git a/625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md b/625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md new file mode 100644 index 00000000..7ad90c6c --- /dev/null +++ b/625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md @@ -0,0 +1,433 @@ +# Canonical Version 2 mathematical rewrite specification + +**Purpose:** a section-by-section replacement plan for `625/arxiv/main.tex` after the remaining Section VIII theorem is proved +**Authority:** the exact theorem statements must be rechecked against the integrated Lean/public proof branch before manuscript substitution + +## 1. Main theorem package + +Let + +\[ + q=\ln2, + \qquad + H_n=\frac{n}{(\ln n)^3}, + \qquad + A_4(\delta)=\ln2-D_4(\delta). +\] + +### Proposed main theorem + +> **Theorem (phase-resolved chromatic--cochromatic gap).** Let +> `G_n~G(n,1/2)` and let `delta_n` be the complete independence-number phase. +> Then +> \[ +> \chi(G_n)-\zeta(G_n) +> \ge +> \left[ +> \frac{q^2}{8}A_4(\delta_n)-o(1) +> \right]H_n +> \] +> with high probability, uniformly along the full sequence of integers `n`. + +The `o(1)` is deterministic and uniform in the phase. + +### Proposed certified corollary + +Use the exact entropy certificate + +\[ + A_4(\delta)>\ln(1000/639) + \qquad(0\le\delta\le1) +\] + +to state + +\[ + \chi(G_n)-\zeta(G_n) + \ge + \frac{q^2}{8}\ln(1000/639)H_n +\] + +with high probability. The coefficient is + +\[ + 0.0268964098083791186\ldots. +\] + +### Proposed complement corollary + +\[ + \min\{\chi(G_n),\chi(\overline G_n)\}-\zeta(G_n) + \ge + \frac{q^2}{8}\ln(1000/639)H_n +\] + +with high probability. + +## 2. Constant derivation to insert after the root calculation + +Retain the exact phase-resolved root displacement + +\[ + r_+(n)-r_4^{\rm co}(n) + =\left[ + \frac{q^2}{4}A_4(\delta_n)+o(1) + \right]H_n. +\] + +For + +\[ + k_{\rm co}=\left\lceil\frac{r_4^{\rm co}+r_+}{2}\right\rceil, + \qquad + k_\chi^- =\lfloor r_+\rfloor-\lceil\ln n\rceil, +\] + +write directly + +\[ +\begin{aligned} + k_\chi^- - k_{\rm co} + &=\frac12(r_+-r_4^{\rm co})-O(\ln n)\\ + &=\left[ + \frac{q^2}{8}A_4(\delta_n)+o(1) + \right]H_n. +\end{aligned} +\] + +Since the amplifier adds `o(H_n)` parts, the same leading coefficient survives in the final gap. Do not introduce the intermediate fixed halvings currently appearing in (5.12), (5.20), and (11.2). + +## 3. Section 5 entropy certificate replacement + +Replace the old omitted-mass bounds by the exact rational certificate from PR #32. The replacement lemma should state only what is used downstream: + +> **Lemma (uniform four-support entropy advantage).** For every +> `delta in [0,1]`, +> \[ +> D_4(\delta)<\ln(639/500), +> \qquad +> A_4(\delta)>\ln(1000/639). +> \] + +The proof may be placed in a compact appendix if the exact rational interval calculations make the main narrative too long. Its required ingredients are: + +1. the certified tilt interval + \[ + \frac{49}{20}q<\lambda_4<\frac{83}{20}q; + \] +2. a split at `29q/10`; +3. the four exact omitted-ratio inequalities; +4. monotonicity of the low and high omitted masses; +5. evaluation of the full-support dual function at the four-support optimizer. + +## 4. Section 7 corrections and strengthening + +### 4.1 Correct signed partial moment + +Change + +```tex +2^\ell_\bullet +``` + +to + +```tex +2^{\ell_\bullet}. +``` + +### 4.2 Replace decimal central-rate verification + +Use the exact strengthened central rate from PR #30. State it as a finite analytic lemma with rational logarithm bounds rather than decimal evaluations embedded in the proof. The target form is + +\[ + \Phi_T(z)\le-c_0(1-R) +\] + +on the complete central domain, with one explicit rational `c_0` no smaller than `1/100` if the final audited domain matches the PR #30 certificate. + +### 4.3 Record margin dependence + +For later non-midpoint work, parameterize the positive signed first-moment margin by + +\[ + M_n(k)=L_{S_4}(n,k)+qk. +\] + +At the midpoint, `M_n(k_co)>=c n/ln n`. The fixed-midpoint paper may keep this simpler bound. A separate proposition should record the exact dependence for moving placements rather than hiding it in `c_Z`. + +## 5. New Section VIII finite parameterization + +### 5.1 Block support and partial physical fibres + +For each attained canonical high physical skeleton, define: + +- a block-level bipartite matching `P` between row and column blocks; +- endpoint sizes `s_e,t_e` and `m_e=min(s_e,t_e)`; +- actual multiplicity `j_e` with `R_0 If deletion of `I` is injective on a finite family `C` of subsets of `E`, 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 the even-subgraph family, deletion of the exposed matching is injective. + +### 6.2 Q-only local absorption + +Outside the matching, use + +\[ + q_{ab}=\frac{\theta_{ab}^2}{2}+\lambda_{ab}^{\rm loc}, + \qquad + \lambda_{ab}^{\rm loc}\le q_{ab}. +\] + +Therefore the local product and even-subgraph product are bounded together by + +\[ + \exp\left\{2\sum_{a,b}q_{ab}\right\}. +\] + +Under the degree caps and `2^U<=m^3`, the checked total-q estimate gives + +\[ + \sum_{a,b}q_{ab}\le CU^2. +\] + +### 6.3 Intrinsic complementary regime + +If `2^U>m^3`, use the exact finite implication + +\[ + m<2^{\lceil U/3\rceil} +\] + +and the deterministic capped attachment bound. Assemble both regimes over the literal attained attachment sum. + +### 6.4 Aggregate statement + +The authoritative Section IX endpoint should be + +\[ + \operatorname{AttachmentSum}_n + \le + \operatorname{BareSkeletonSum}_n + \exp\left\{\varepsilon_n\frac n{(\ln n)^4}\right\}, + \qquad + \varepsilon_n\to0. +\] + +This statement composes directly with the exact normalized-second-moment identity. Do not reintroduce a polymer surrogate or independent demand law. + +## 7. Proposition 9.2 replacement proof + +Write the normalized signed second moment exactly as the attained attachment sum. Apply the aggregate Section IX theorem, then the Section VIII bare-skeleton estimate: + +\[ +\begin{aligned} + \frac{\mathbb EZ^2}{(\mathbb EZ)^2} + &\le + \operatorname{BareSkeletonSum}_n + \exp\left\{\varepsilon_n\frac n{N^4}\right\}\\ + &\le + \exp\left\{o\left(\frac n{N^4}\right)\right\}. +\end{aligned} +\] + +There is no need to take a supremum over skeletons or to enumerate simple cycles. + +## 8. Section 10 named amplifier theorem + +Retain Lemmas 10.1 and 10.2, but promote the following statement: + +> **Proposition (rare-seed completion tail).** If +> \[ +> \Pr\{\zeta(G_n)\le k_n\}\ge e^{-\Lambda_n}, +> \] +> then, uniformly for deterministic `r>0`, +> \[ +> \Pr\!\left( +> \zeta(G_n)>k_n+C\left[ +> \frac{\sqrt{n\Lambda_n}+\sqrt{nr}}{\ln n}+n^{1/3}+1 +> \right]\right) +> \le e^{-r}+o(1). +> \] + +This theorem should be phrased independently of the midpoint profile. + +## 9. Version 2 conclusion + +Intersect the unrestricted chromatic lower event with the amplified cocoloring upper event. Use + +\[ + k_\chi^- - k_{\rm co} + =\left[\frac{q^2}{8}A_4(\delta_n)+o(1)\right]H_n +\] + +and the `o(H_n)` amplifier loss to obtain the phase-resolved theorem. Then state the fixed certificate and complement corollary. + +## 10. Material to move out of the main proof + +The following should be retained as historical/repository alternatives but removed from the canonical Version 2 proof: + +- the Section VIII near/middle split; +- `E_mid`, `Xi_4`, and the Section VIII residual-mass dichotomy; +- simple-cycle decomposition of the residual even family; +- the residual walk kernel `S`; +- the mixed matching-cycle encoding; +- the parameters `tau` and `h tau`; +- the old conservative `/32` coefficient ledger. + +## 11. Material for a separate “Further directions” section + +Do not state the following as proved consequences of Version 2: + +- shrinking near-root placement; +- exact phase minimum; +- global balance necessity for arbitrary cocolorings; +- slowly growing support; +- a two-sided `Theta(n/(log n)^3)` gap; +- fixed `p!=1/2`; +- the two-independent-graph coupling. + +The balanced rare seed, finite restriction-product theorem, cycle-space factor, and tunable amplifier are rigorous enough to mention as proved method-level results, with their exact scopes. From 929ae4d6e790e6d43ec4cc3ef3049d13eb60c1fe Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 17:41:17 +0300 Subject: [PATCH 3/6] Add exact regression checks for the full TeX re-audit --- .../full_tex_mathematical_reaudit.py | 288 ++++++++++++++++++ 1 file changed, 288 insertions(+) create mode 100644 625/experiments/full_tex_mathematical_reaudit.py diff --git a/625/experiments/full_tex_mathematical_reaudit.py b/625/experiments/full_tex_mathematical_reaudit.py new file mode 100644 index 00000000..36fd3f05 --- /dev/null +++ b/625/experiments/full_tex_mathematical_reaudit.py @@ -0,0 +1,288 @@ +#!/usr/bin/env python3 +"""Exact and high-precision checks for the full Erdős 625 TeX re-audit. + +The script checks deterministic arithmetic used by the audit. It does not +prove the random-graph theorem, the Section VIII physical-fibre equivalence, +or any conjectural theorem upgrade. +""" + +from __future__ import annotations + +from decimal import Decimal, getcontext +from fractions import Fraction +from math import comb, factorial +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def falling(n: int, k: int) -> int: + require(0 <= k <= n, f"invalid falling factorial ({n})_{k}") + value = 1 + for offset in range(k): + value *= n - offset + return value + + +def floor_fraction(value: Fraction) -> int: + return value.numerator // value.denominator + + +def ceil_fraction(value: Fraction) -> int: + return -((-value.numerator) // value.denominator) + + +def signed_local_reward(j: int) -> int: + if j <= 2: + return 1 + return 2 ** (comb(j, 2) - 1) + + +def aggregate_local_weight(m: int, d: int, j: int) -> Fraction: + return Fraction( + falling(m, j) * falling(m + d, j) * signed_local_reward(j), + factorial(j), + ) + + +def aggregate_ratio_formula(m: int, d: int, h: int) -> Fraction: + denominator = 1 + for offset in range(1, h + 1): + denominator *= d + offset + exponent = h * m - h * (h + 1) // 2 + return Fraction(comb(m, h), denominator * 2**exponent) + + +def check_coefficient_ledger() -> dict[str, Decimal]: + getcontext().prec = 80 + q = Decimal(2).ln() + + canonical = q * q * (Decimal(200) / Decimal(153)).ln() / Decimal(32) + old_certificate_midpoint = ( + q * q * (Decimal(200) / Decimal(153)).ln() / Decimal(8) + ) + strong_midpoint = q * q * (Decimal(1000) / Decimal(639)).ln() / Decimal(8) + strong_near_root = q * q * (Decimal(1000) / Decimal(639)).ln() / Decimal(4) + full_support_near_root = q**3 / Decimal(4) + + require(old_certificate_midpoint == 4 * canonical, "factor-four ledger failed") + require(strong_near_root == 2 * strong_midpoint, "near-root factor-two failed") + require( + full_support_near_root > strong_near_root > strong_midpoint > canonical > 0, + "coefficient ordering failed", + ) + + diagnostic_advantage = Decimal("0.520701335491") + diagnostic_midpoint = q * q * diagnostic_advantage / Decimal(8) + diagnostic_near_root = q * q * diagnostic_advantage / Decimal(4) + require(diagnostic_near_root == 2 * diagnostic_midpoint, "diagnostic ratio failed") + + return { + "canonical": canonical, + "old_certificate_midpoint": old_certificate_midpoint, + "strong_midpoint": strong_midpoint, + "strong_near_root": strong_near_root, + "full_support_near_root": full_support_near_root, + "strong_midpoint_over_canonical": strong_midpoint / canonical, + "diagnostic_midpoint": diagnostic_midpoint, + "diagnostic_near_root": diagnostic_near_root, + } + + +def check_midpoint_rounding() -> int: + checked = 0 + values = [Fraction(i, 12) for i in range(-24, 73)] + losses = [Fraction(i, 12) for i in range(0, 49)] + for x in values: + for y in values: + if x <= y: + continue + for loss in losses: + lhs = ( + floor_fraction(x) + - ceil_fraction(loss) + - ceil_fraction((x + y) / 2) + ) + rhs = (x - y) / 2 - loss - 3 + require(Fraction(lhs) > rhs, "midpoint rounding inequality failed") + checked += 1 + return checked + + +def check_aggregate_local_ratio(max_m: int = 90) -> int: + checked = 0 + for m in range(5, max_m + 1): + for d in range(4): + for h in range(0, m): + if 2 * h >= m: + continue + j = m - h + require(j >= 3, "tested high multiplicity fell below reward range") + actual = aggregate_local_weight(m, d, j) / aggregate_local_weight(m, d, m) + formula = aggregate_ratio_formula(m, d, h) + require(actual == formula, f"aggregate local ratio failed: m={m}, d={d}, h={h}") + checked += 1 + return checked + + +def check_global_denominator(max_n: int = 120) -> int: + checked = 0 + for n in range(max_n + 1): + for j in range(n + 1): + for h in range(n - j + 1): + ratio = Fraction(falling(n, j + h), falling(n, j)) + require(ratio == falling(n - j, h), "global denominator identity failed") + require(ratio <= n**h, "global denominator upper bound failed") + checked += 1 + return checked + + +def check_two_thirds_budget(max_m: int = 1200) -> int: + checked = 0 + for m in range(1, max_m + 1): + for h in range(1, m + 1): + if 2 * h >= m: + continue + lhs = h * ((2 * m) // 3) + rhs = h * m - h * (h + 1) // 2 + require(lhs <= rhs, f"two-thirds budget failed: m={m}, h={h}") + checked += 1 + return checked + + +def check_geometric_fibre() -> int: + checked = 0 + for denominator in range(2, 101): + for numerator in range(1, denominator // 2 + 1): + rho = Fraction(numerator, denominator) + for cutoff in range(1, 50): + finite_sum = sum((rho**h for h in range(1, cutoff + 1)), Fraction()) + require(finite_sum <= rho / (1 - rho), "geometric majorant failed") + require(finite_sum <= 2 * rho, "two-rho majorant failed") + checked += 1 + return checked + + +def check_binary_entropy_penalty() -> list[tuple[Decimal, Decimal]]: + getcontext().prec = 80 + q = Decimal(2).ln() + rows: list[tuple[Decimal, Decimal]] = [] + previous: Decimal | None = None + for integer in range(1, 10): + x = Decimal(integer) / Decimal(20) + rho = Decimal("0.5") + x + entropy = -(rho * rho.ln() + (1 - rho) * (1 - rho).ln()) + penalty = q - entropy + require(penalty > 0, "binary entropy penalty is not positive") + if previous is not None: + require(penalty > previous, "binary entropy penalty is not increasing") + previous = penalty + rows.append((x, penalty)) + return rows + + +def check_asymptotic_scales() -> list[tuple[int, Decimal, Decimal, Decimal]]: + """Check logarithms of the relevant ratios to n/(log n)^4.""" + + getcontext().prec = 80 + rows: list[tuple[int, Decimal, Decimal, Decimal]] = [] + previous_all_high: Decimal | None = None + previous_transport: Decimal | None = None + previous_theta_margin: Decimal | None = None + + for nlog in (120, 240, 480, 960, 1920): + N = Decimal(nlog) + # n^(2/3) N^(4/3) divided by n/N^4. + log_all_high = -N / 3 + (Decimal(16) / 3) * N.ln() + # sqrt(nN) divided by n/N^4. + log_transport = -N / 2 + (Decimal(9) / 2) * N.ln() + # theta=nlog^(-1/2): (theta*n/N) / N, comparing the seed log-margin + # with a conservative O(N) logarithmic error. + log_theta_margin = N - (Decimal(5) / 2) * N.ln() + + if previous_all_high is not None: + require(log_all_high < previous_all_high, "all-high ratio is not decreasing") + require(log_transport < previous_transport, "transport ratio is not decreasing") + require( + log_theta_margin > previous_theta_margin, + "candidate near-root seed margin is not increasing", + ) + previous_all_high = log_all_high + previous_transport = log_transport + previous_theta_margin = log_theta_margin + rows.append((nlog, log_all_high, log_transport, log_theta_margin)) + + require(rows[-1][1] < -100, "all-high error is not strongly subcritical") + require(rows[-1][2] < -100, "endpoint transport error is not strongly subcritical") + require(rows[-1][3] > 100, "candidate near-root margin is not strongly supercritical") + return rows + + +def check_slow_support_warning() -> tuple[Decimal, Decimal]: + """Demonstrate why K=o(N) is insufficient if Lambda=K*n/N^4.""" + + getcontext().prec = 80 + N = Decimal(10_000) + K = N.sqrt() + require(K / N < Decimal("0.02"), "chosen K is not visibly o(N) at the test point") + target_ratio = K # (K*n/N^4)/(n/N^4) + require(target_ratio > 1, "counterexample to the proposed complexity criterion failed") + return K / N, target_ratio + + +def scan_canonical_tex() -> dict[str, bool]: + path = Path(__file__).resolve().parents[1] / "arxiv" / "main.tex" + if not path.is_file(): + return {"available": False} + text = path.read_text(encoding="utf-8") + return { + "available": True, + "old_coefficient": r"\frac{(\ln 2)^2}{32}" in text, + "old_entropy_certificate": r"\ln\frac{200}{153}" in text, + "near_middle_split": "canonical near--middle split" in text, + "cycle_kernel": "Cycle-kernel estimate" in text, + "partial_diagonal_exponent_typo": r"2^\ell_\bullet" in text, + } + + +def main() -> None: + coefficients = check_coefficient_ledger() + rounding_cases = check_midpoint_rounding() + local_ratio_cases = check_aggregate_local_ratio() + denominator_cases = check_global_denominator() + budget_cases = check_two_thirds_budget() + geometric_cases = check_geometric_fibre() + entropy_rows = check_binary_entropy_penalty() + scale_rows = check_asymptotic_scales() + slow_support_ratio, slow_support_target = check_slow_support_warning() + tex_scan = scan_canonical_tex() + + print("ERDOS 625 FULL TEX MATHEMATICAL RE-AUDIT: PASS") + print(" coefficient ledger:") + for name, value in coefficients.items(): + print(f" {name}: {value}") + print(f" midpoint rounding cases: {rounding_cases}") + print(f" exact aggregate local-ratio cases: {local_ratio_cases}") + print(f" global falling-factorial cases: {denominator_cases}") + print(f" two-thirds exponent cases: {budget_cases}") + print(f" geometric-fibre cases: {geometric_cases}") + print(" binary-entropy penalties (x, log2-H(1/2+x)):") + for x, penalty in entropy_rows: + print(f" {x}: {penalty}") + print(" asymptotic log-ratios (N, all-high/target, transport/target, theta seed/O(N)):") + for row in scale_rows: + print(f" {row[0]}: {row[1]}, {row[2]}, {row[3]}") + print(" slow-support criterion diagnostic:") + print(f" K/N at N=10000: {slow_support_ratio}") + print(f" (K*n/N^4)/(n/N^4): {slow_support_target}") + print(" canonical TeX audit markers:") + for name, value in tex_scan.items(): + print(f" {name}: {value}") + print(" scope: deterministic arithmetic and source-marker audit only") + + +if __name__ == "__main__": + main() From 65199a6638a45b43c61b039147572db270b1b69c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 17:42:18 +0300 Subject: [PATCH 4/6] Add focused CI for the full TeX mathematical re-audit --- ...erdos625-full-tex-mathematical-reaudit.yml | 90 +++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 .github/workflows/erdos625-full-tex-mathematical-reaudit.yml diff --git a/.github/workflows/erdos625-full-tex-mathematical-reaudit.yml b/.github/workflows/erdos625-full-tex-mathematical-reaudit.yml new file mode 100644 index 00000000..cacb48a2 --- /dev/null +++ b/.github/workflows/erdos625-full-tex-mathematical-reaudit.yml @@ -0,0 +1,90 @@ +name: Erdős 625 full TeX mathematical re-audit + +on: + pull_request: + paths: + - "625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md" + - "625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md" + - "625/experiments/full_tex_mathematical_reaudit.py" + - "625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md" + - ".github/workflows/erdos625-full-tex-mathematical-reaudit.yml" + workflow_dispatch: + +concurrency: + group: erdos625-full-tex-reaudit-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + mathematical-reaudit: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + + - name: Compile deterministic audit checker + run: python -m py_compile 625/experiments/full_tex_mathematical_reaudit.py + + - name: Run deterministic audit checker + run: python 625/experiments/full_tex_mathematical_reaudit.py + + - name: Run deterministic audit checker with optimization + run: python -O 625/experiments/full_tex_mathematical_reaudit.py + + - name: Check audit coverage and corrected research classifications + run: | + python - <<'PY' + from pathlib import Path + + audit = Path("625/audits/FULL_TEX_MATHEMATICAL_REAUDIT_2026-07-26.md") + rewrite = Path("625/proofs/CANONICAL_V2_REWRITE_SPEC_2026-07-26.md") + corrections = Path("625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md") + + for path in (audit, rewrite, corrections): + if not path.is_file(): + raise SystemExit(f"missing required file: {path}") + + audit_text = audit.read_text(encoding="utf-8") + rewrite_text = rewrite.read_text(encoding="utf-8") + correction_text = corrections.read_text(encoding="utf-8") + + audit_markers = ( + "The unique submission-blocking proof seam remains Section VIII", + "Section 7: partial diagonals", + "Section 8: exact diagnosis and replacement", + "Section 9: direct q-only replacement", + "Balance stability: restrict the current theorem", + "Slowly growing support: correct the complexity condition", + "Cochomatic location corridor: make the upper side conditional", + ) + rewrite_markers = ( + "Proposed main theorem", + "New Section VIII finite parameterization", + "New Section IX direct attachment theorem", + "Version 2 conclusion", + ) + correction_markers = ( + "Near-root placement correction", + "Balance-stability correction", + "Slow-support complexity correction", + "Cochromatic-corridor correction", + ) + + for marker in audit_markers: + if marker not in audit_text: + raise SystemExit(f"missing audit marker: {marker}") + for marker in rewrite_markers: + if marker not in rewrite_text: + raise SystemExit(f"missing rewrite marker: {marker}") + for marker in correction_markers: + if marker not in correction_text: + raise SystemExit(f"missing correction marker: {marker}") + + forbidden = (r"2^\ell_\bullet", "K(m_n)=o(N) is sufficient") + for token in forbidden: + if token in correction_text: + raise SystemExit(f"superseded assertion remains in correction note: {token}") + + print("full TeX re-audit coverage: PASS") + PY From c86213434695f1ff05654d352c36cc87ca661d93 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 17:43:18 +0300 Subject: [PATCH 5/6] Correct the theorem-upgrade classifications after the full TeX audit --- ..._UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md | 231 ++++++++++++++++++ 1 file changed, 231 insertions(+) create mode 100644 625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md diff --git a/625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md b/625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md new file mode 100644 index 00000000..5188a677 --- /dev/null +++ b/625/research/ERDOS625_VALUE_UPGRADE_REAUDIT_CORRECTIONS_2026-07-26.md @@ -0,0 +1,231 @@ +# Corrections to the Erdős 625 theorem-upgrade program after the full TeX re-audit + +**Date:** 26 July 2026 +**Applies to:** `ERDOS625_VALUE_UPGRADE_PROGRAM_2026-07-26.md` and `ERDOS625_VALUE_UPGRADE_THEOREMS.tex` in PR #43 +**Purpose:** narrow four proposed extensions whose first formulations were stronger than the mathematics presently supports + +The main phase-resolved `/8` theorem, stronger certified fixed coefficient, complement corollary, tunable amplifier tail, and balanced rare seed are unchanged. The corrections below concern only new theorem programs. + +## 1. Near-root placement correction + +### Earlier formulation + +The initial roadmap treated + +\[ + \theta_n\ln n\to\infty +\] + +as though it were already a proved sufficient condition for moving the signed witness from the midpoint to + +\[ + k_{\theta_n} + =\left\lceil + r_4^{\rm co}+\theta_n(r_+-r_4^{\rm co}) + \right\rceil. +\] + +### Correct classification + +This condition is a **candidate sufficient criterion**, not an established lemma. The exact deterministic placement formula is valid, but the proof must collect the dependence on the positive signed first-moment margin in Sections 7--9. + +Define + +\[ + M_n(\theta) + =L_{S_4}(n,k_\theta)+(\ln2)k_\theta. +\] + +The expected scale is + +\[ + M_n(\theta)\asymp \theta\frac n{\ln n}. +\] + +A complete theorem must prove that: + +1. integer profile construction and Stirling errors are `o(M_n(theta_n))`; +2. the full-corner term `1/EZ` still beats the polynomial number of residual profiles; +3. Lemma 7.1 is uniform at the moving profile; +4. the Section VIII bare-skeleton theorem is uniform at the moving profile; +5. the q-only attachment theorem is uniform at the moving profile; +6. the amplifier adds `o(n/(ln n)^3)` classes, which is sufficient for the final coefficient. + +The explicit candidate + +\[ + \theta_n=(\ln n)^{-1/2} +\] + +still leaves a first-moment log margin of order `n/(ln n)^(3/2)` and is therefore a strong conservative target. It should be retained as a conjectural theorem until the uniform replay is complete. + +### Correct theorem label + +> **Near-root placement program.** Prove uniformity of the four-support second-moment architecture for `theta_n=(ln n)^(-1/2)`. Conditional on that uniformity, +> \[ +> \chi(G_n)-\zeta(G_n) +> \ge +> \left[ +> \frac{(\ln2)^2}{4}A_4(\delta_n)-o(1) +> \right]\frac n{(\ln n)^3} +> \] +> with high probability. + +## 2. Balance-stability correction + +### Earlier formulation + +The initial roadmap proposed that every near-optimal cocoloring must use asymptotically equal numbers of clique and independent parts, based on replacing `2^k` by `binom(k,rho k)`. + +### Correct classification + +That calculation controls the selected **four-size signed witness family**. It does not exclude an arbitrary cocoloring with a different class-size profile. The immediate theorem target must therefore be restricted. + +### Valid current targets + +1. **Balanced rare seed:** already follows from the unrestricted normalized second moment up to a polynomial loss. +2. **Balanced constructed cocoloring:** a labelled-slot amplifier should preserve asymptotic balance while adding `o(H_n)` parts. +3. **Four-size witness-family stability:** among signed witnesses with the chosen four-size profile, a fixed sign imbalance loses + \[ + k\bigl(\ln2-H(\rho)\bigr) + \] + in first-moment entropy and shifts the root by a positive multiple of `H_n`. + +### Global theorem requires a new input + +To prove that **every arbitrary near-optimal cocoloring** is balanced, one must first perform a first-moment union bound over all signed class-size profiles. This is the same all-profile lower-location problem required for a matching upper bound on `chi-zeta`. + +The global balance theorem must therefore be moved under the all-signed-profile location program. + +## 3. Slow-support complexity correction + +### Earlier formulation + +The initial program proposed an estimate of the form + +\[ + \Lambda(n,m) + \le O\!\left(K(m)\frac n{(\ln n)^4}\right) +\] + +and suggested choosing `K(m_n)=o(ln n)`. + +### Why this is insufficient + +The target required by the amplifier is + +\[ + \Lambda(n,m_n)=o\!\left(\frac n{(\ln n)^4}\right). +\] + +If the bound is literally `K(m)n/(ln n)^4`, then any growing `K(m_n)` violates the target scale. The condition `K(m_n)=o(ln n)` does not repair this. + +### Correct formulation + +First prove a dimension-dependent bound + +\[ + \Lambda(n,m)\le K(m)B_n, +\] + +where the fixed-support base scale satisfies + +\[ + B_n=o\!\left(\frac n{(\ln n)^4}\right). +\] + +Then choose `m_n` so that + +\[ + K(m_n)B_n=o\!\left(\frac n{(\ln n)^4}\right). +\] + +For example, the present fixed four-size bare-skeleton exponent has the much smaller scale + +\[ + B_n= + O\!\left(n^{2/3}(\ln n)^{4/3}+\sqrt{n\ln n}\right). +\] + +A polynomial or moderately exponential `K(m)` may then permit a slowly growing support, but the admissible growth must be calculated from this exact comparison. + +### Support definition + +Replace the ambiguous phrase “`m` consecutive sizes” by an explicit deficit support, for example + +\[ + S_m=\{-1,0,1,\ldots,m\}, +\] + +with `m=o(alpha)`. Other asymmetric truncations may be better, but their endpoints and feasibility interval must be stated. + +## 4. Cochromatic-corridor correction + +### Earlier formulation + +The initial roadmap wrote the prospective upper location + +\[ + \zeta(G_n)\le r_4^{\rm co}(n)+o(H_n) +\] + +as though it were already the output of the current constructive proof. + +### Correct present upper location + +The current midpoint construction gives + +\[ + \zeta(G_n) + \le + \frac{r_4^{\rm co}(n)+r_+(n)}2+o(H_n) +\] + +with high probability, conditional on closure of the normalized second moment. + +### Near-root upper location + +The sharper bound + +\[ + \zeta(G_n)\le r_4^{\rm co}(n)+o(H_n) +\] + +requires the near-root placement theorem above. + +### Correct corridor program + +The location project has three logically separate stages: + +1. **midpoint upper location:** supplied by the current candidate proof after Section VIII closure; +2. **near-root upper location:** conditional on the shrinking-placement uniformity theorem; +3. **all-profile lower location:** a new first-moment exclusion theorem over every signed profile. + +Only after stages 2 and 3 can one state a two-sided `O(H_n)` cochromatic corridor centered at the full signed root. + +## 5. Revised priority order + +1. close the physical-fibre and global all-deficit Section VIII theorem; +2. insert the phase-resolved `/8` theorem and stronger fixed coefficient; +3. add the complement corollary and tunable tail; +4. prove the balanced rare seed and, if concise, the labelled-slot balanced amplifier; +5. audit `theta_n=(ln n)^(-1/2)` placement quantitatively; +6. develop an all-signed-profile lower location; +7. only then promote global balance necessity and a near-root cochromatic corridor; +8. formulate the slow-support complexity bound with an actual base scale `B_n`; +9. pursue the ordinary-coloring third-order upper construction needed for the full matching upper bound. + +## 6. Statements unaffected by this correction + +The following remain correctly classified: + +- public candidate-proof chronology beginning on 12 July 2026; +- the exact phase-resolved root displacement; +- the midpoint `/8` coefficient; +- the stronger entropy certificate `A_4>ln(1000/639)`; +- the simultaneous complement corollary; +- the tunable rare-seed completion tail; +- the generic restriction-product theorem; +- the exact signed cycle-space factor; +- the limiting coefficient `(ln 2)^3/4` as the formal full-support, near-root target; +- the matching `O(n/(ln n)^3)` upper bound as the largest separate follow-up problem. From d61a8f70557ea5ce75cbb0d24816c233ca8edb7e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sun, 26 Jul 2026 17:50:02 +0300 Subject: [PATCH 6/6] Make high-precision coefficient checks rounding-safe --- .../full_tex_mathematical_reaudit.py | 24 +++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/625/experiments/full_tex_mathematical_reaudit.py b/625/experiments/full_tex_mathematical_reaudit.py index 36fd3f05..d7542da1 100644 --- a/625/experiments/full_tex_mathematical_reaudit.py +++ b/625/experiments/full_tex_mathematical_reaudit.py @@ -19,6 +19,13 @@ def require(condition: bool, message: str) -> None: raise RuntimeError(message) +def decimal_close(left: Decimal, right: Decimal) -> bool: + """Relative comparison at a scale well below the 80-digit work precision.""" + + scale = max(Decimal(1), abs(left), abs(right)) + return abs(left - right) <= Decimal("1e-70") * scale + + def falling(n: int, k: int) -> int: require(0 <= k <= n, f"invalid falling factorial ({n})_{k}") value = 1 @@ -68,8 +75,14 @@ def check_coefficient_ledger() -> dict[str, Decimal]: strong_near_root = q * q * (Decimal(1000) / Decimal(639)).ln() / Decimal(4) full_support_near_root = q**3 / Decimal(4) - require(old_certificate_midpoint == 4 * canonical, "factor-four ledger failed") - require(strong_near_root == 2 * strong_midpoint, "near-root factor-two failed") + require( + decimal_close(old_certificate_midpoint, 4 * canonical), + "factor-four ledger failed", + ) + require( + decimal_close(strong_near_root, 2 * strong_midpoint), + "near-root factor-two failed", + ) require( full_support_near_root > strong_near_root > strong_midpoint > canonical > 0, "coefficient ordering failed", @@ -78,7 +91,10 @@ def check_coefficient_ledger() -> dict[str, Decimal]: diagnostic_advantage = Decimal("0.520701335491") diagnostic_midpoint = q * q * diagnostic_advantage / Decimal(8) diagnostic_near_root = q * q * diagnostic_advantage / Decimal(4) - require(diagnostic_near_root == 2 * diagnostic_midpoint, "diagnostic ratio failed") + require( + decimal_close(diagnostic_near_root, 2 * diagnostic_midpoint), + "diagnostic ratio failed", + ) return { "canonical": canonical, @@ -199,7 +215,7 @@ def check_asymptotic_scales() -> list[tuple[int, Decimal, Decimal, Decimal]]: log_all_high = -N / 3 + (Decimal(16) / 3) * N.ln() # sqrt(nN) divided by n/N^4. log_transport = -N / 2 + (Decimal(9) / 2) * N.ln() - # theta=nlog^(-1/2): (theta*n/N) / N, comparing the seed log-margin + # theta=N^(-1/2): (theta*n/N) / N, comparing the seed log-margin # with a conservative O(N) logarithmic error. log_theta_margin = N - (Decimal(5) / 2) * N.ln()