From c29b230751e47d3edb500968c4cc96eb43a53cc4 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:50:29 +0300 Subject: [PATCH 1/5] Add isolated Section 7 and Section 9 proof note --- 625/proofs/SECTION7_SECTION9_SUPERCHECK.md | 254 +++++++++++++++++++++ 1 file changed, 254 insertions(+) create mode 100644 625/proofs/SECTION7_SECTION9_SUPERCHECK.md diff --git a/625/proofs/SECTION7_SECTION9_SUPERCHECK.md b/625/proofs/SECTION7_SECTION9_SUPERCHECK.md new file mode 100644 index 00000000..3be9bd32 --- /dev/null +++ b/625/proofs/SECTION7_SECTION9_SUPERCHECK.md @@ -0,0 +1,254 @@ +# Erdős 625: isolated Section 7 and Section 9 simplifications + +**Status.** This note isolates two claims from draft PR #27 that survived a +second adversarial review and an independent exact finite test suite. It is a +review note, not a replacement for the canonical manuscript and not a proof of +`Erdos625Statement`. + +Throughout, + +\[ + q=\ln 2,\qquad N=\ln n. +\] + +## 1. An exact central-rate certificate + +Use the notation of Lemma 7.1 of the canonical manuscript. Let +\(p=(p_i)_{i=2}^5\) be a probability vector with mean + +\[ + \sum_{i=2}^5 i p_i=T, + \qquad + \frac2q\le T\le1+\frac2q. +\] + +For \(0\le z_i\le p_i\), put + +\[ + R=\sum_i z_i,\qquad Y=1-R,\qquad I_r=\sum_i i z_i, +\] + +and + +\[ + \Phi_T(z)=R\ln R+\frac q2(I_r-TR). +\] + +### Lemma 1.1 + +For \(1/64\le R\le1\), + +\[ + \boxed{\Phi_T(z)\le-\frac{1-R}{100}.} + \tag{1.1} +\] + +### Proof + +The support bounds give + +\[ + I_r-TR\le(5-T)R, + \tag{1.2} +\] + +while, with \(y_i=p_i-z_i\), + +\[ + I_r-TR=\sum_i(T-i)y_i\le(T-2)(1-R). + \tag{1.3} +\] + +For \(1/64\le R\le47/100\), use \(T\ge2/q\): + +\[ + \Phi_T(z)\le R\ln R+(5q/2-1)R. + \tag{1.4} +\] + +The function + +\[ + f(R)=R\ln R+(5q/2-1)R+\frac{1-R}{100} +\] + +is convex. Its endpoint values are strictly negative. The accompanying +script certifies these signs using exact `Fraction` bounds obtained from + +\[ + \ln x=2\,\operatorname{arctanh}\!\left(\frac{x-1}{x+1}\right). +\] + +In particular, it proves rational upper bounds below zero for +\(f(1/64)\) and \(f(47/100)\). Convexity then gives \(f\le0\) on the +whole interval. + +For \(47/100\le R\le1\), use \(T\le1+2/q\): + +\[ + \Phi_T(z)\le R\ln R+(1-q/2)(1-R). + \tag{1.5} +\] + +The function + +\[ + h(R)=R\ln R+(1-q/2+1/100)(1-R) +\] + +is convex, satisfies \(h(1)=0\), and has a rigorously certified negative +value at \(47/100\). Hence \(h\le0\) on the second interval. Combining +the two ranges proves (1.1). \(\square\) + +This improves the manuscript's displayed constant \(1/5000\) to +\(1/100\). It does not change the asymptotic order, but gives substantially +more room when absorbing the entropy and Stirling errors in the central +partial-diagonal range. + +## 2. Residual restriction replaces the cycle-to-walk argument + +Start from equation (9.12) of the canonical manuscript. Let \(M\) be the +exposed canonical high matching and let \(R\) be the finite potential residual +edge relation. For an even edge set \(F\subseteq M\cup R\), the matching edges +have weight one and each residual edge \(e\) has a nonnegative weight \(q_e\). + +### Lemma 2.1 (unique even completion) + +The map + +\[ + F\longmapsto F\setminus M + \tag{2.1} +\] + +is injective on the family of even edge sets contained in \(M\cup R\). + +### Proof + +If two even sets have the same restriction, their symmetric difference is an +even edge set contained in \(M\). A nonempty subset of a matching has degree +one at every incident vertex, so it is not even. The symmetric difference is +therefore empty. \(\square\) + +### Corollary 2.2 (weighted subset-product bound) + +\[ + \sum_{F\text{ even}}\prod_{e\in F\setminus M}q_e + \le + \prod_{e\in R\setminus M}(1+q_e) + \le + \exp\!\left(\sum_{e\in R\setminus M}q_e\right). + \tag{2.2} +\] + +The first inequality follows from Lemma 2.1 by enlarging the image to the full +power set. The second is the finite identity for a subset generating function, +and the third uses \(1+x\le e^x\). + +The finite injection already has a Lean counterpart in +`EvenMatchingRestriction.lean`, and the generic product-to-exponential algebra +has a counterpart in `Section9FiniteFamilyAlgebra.lean`. This note does not +claim that the complete probability specialization is already formalized. + +## 3. The improved large-residual envelope + +Equation (9.12) and Corollary 2.2 give + +\[ + \mathcal A(M,j) + \le + \exp\!\left(\Lambda_0+\sum_{e\in R\setminus M}q_e\right). + \tag{3.1} +\] + +For off-matching cells define + +\[ + \widetilde\theta_{ab}=\frac{e\,d_a d_b'}{m_0}. +\] + +Because \(q_e=0\) on \(M\), the correct identity and inequality are + +\[ + \sum_{e\in R\setminus M}q_e + =\frac12\sum_{(a,b)\notin M}\widetilde\theta_{ab}^{\,2}+\Lambda_0 + \le + \frac12\sum_{a,b}\widetilde\theta_{ab}^{\,2}+\Lambda_0. + \tag{3.2} +\] + +Only the unrestricted square sum factorizes: + +\[ + \sum_{a,b}\widetilde\theta_{ab}^{\,2} + =\frac{e^2}{m_0^2} + \left(\sum_a d_a^2\right) + \left(\sum_b(d_b')^2\right). + \tag{3.3} +\] + +Every residual degree is at most \(U\), and both degree sums equal \(m_0\). +Thus + +\[ + \sum_a d_a^2\le Um_0, + \qquad + \sum_b(d_b')^2\le Um_0, + \tag{3.4} +\] + +so + +\[ + \sum_{a,b}\widetilde\theta_{ab}^{\,2}\le e^2U^2. + \tag{3.5} +\] + +Using the existing large-residual estimate + +\[ + \Lambda_0\le C\frac{U^4}{m_0}, + \tag{3.6} +\] + +we obtain + +\[ + \boxed{ + \mathcal A(M,j) + \le + \exp\!\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} + \tag{3.7} +\] + +When \(m_0\ge n/N^6\) and \(U=O(N)\), + +\[ + \frac{U^4}{m_0}=O(N^{10}/n)=o(1), +\] + +and therefore + +\[ + \mathcal A(M,j)\le\exp(O(N^2)) + =\exp\{o(n/N^4)\}. + \tag{3.8} +\] + +This replaces the manuscript's \(\exp(O(N^8))\) large-residual envelope and +removes the simple-cycle decomposition, residual-walk enumeration, mixed +matching-cycle encoding, the parameter \(\tau\), and the term \(h\tau\). + +## 4. Scope boundary + +The arguments above depend on the canonical manuscript's threshold expansion +through (9.12) and its local increment estimate through (9.13). They do not +prove the Section 8 global high-skeleton sum, the complete normalized second +moment, or `Erdos625Statement` by themselves. + +The companion exact script exhausts all matchings, residual relations, and even +edge sets for \(K_{2,2}\), \(K_{2,3}\), and \(K_{3,3}\), checks two rational +weight systems, verifies the off-matching square-sum inequality on more than +six hundred thousand degree/matching instances, and certifies the Section 7 +endpoint signs by rational logarithm bounds. These are regression tests, not a +substitute for the displayed proofs. From 583093dd57540a6c807d9ed661a8b951f380d94b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:50:45 +0300 Subject: [PATCH 2/5] Add independent Section 7 and 9 super-check record --- 625/audits/SECTION7_SECTION9_SUPERCHECK.md | 75 ++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 625/audits/SECTION7_SECTION9_SUPERCHECK.md diff --git a/625/audits/SECTION7_SECTION9_SUPERCHECK.md b/625/audits/SECTION7_SECTION9_SUPERCHECK.md new file mode 100644 index 00000000..13f58486 --- /dev/null +++ b/625/audits/SECTION7_SECTION9_SUPERCHECK.md @@ -0,0 +1,75 @@ +# Super-check of the proposed Erdős 625 Section 7 and Section 9 simplifications + +**Repository base:** `main` at `cda78922ea6c87bfc81f9bf693374dd045dac624`. + +**Verdict:** the two isolated claims in +`proofs/SECTION7_SECTION9_SUPERCHECK.md` pass this review. This is not a verdict +on all of draft PR #27 or on the complete candidate proof. + +## Checked claims + +1. The central partial-diagonal rate satisfies + \[ + \Phi_T(z)\le-(1-R)/100 + \] + on the displayed domain. +2. Restriction away from a matching is injective on even edge sets. +3. The resulting weighted family sum is bounded by the full residual subset + product. +4. The off-matching square sum is bounded by the unrestricted factorized sum. +5. The large-residual attachment envelope is therefore + \[ + \mathcal A(M,j)\le + \exp\{C(U^2+U^4/m_0)\}=\exp(O(N^2)). + \] + +## Independent exact checks + +Run from the repository root: + +```text +python 625/experiments/section7_section9_supercheck.py +``` + +The current run reports: + +```text +ERDOS 625 SECTION 7/9 SUPERCHECK: PASS + central-rate endpoint inequalities: exact Fraction bounds + residual relations exhausted: 5912 + even edge sets checked: 12561 + square-sum instances checked: 613711 +``` + +The logarithm endpoint checks use rational lower and upper bounds from the +atanh series, rather than floating-point signs. The graph checks exhaust every +partial matching and every residual relation in the listed small complete +bipartite graphs. + +## Adversarial points checked + +- The matching hypothesis is essential. No restriction-injectivity statement + is made for a general high-edge graph. +- The product runs only over residual edges outside the matching. +- The identity in the square-sum step is used only for the unrestricted sum; + the off-matching sum enters by a one-sided inequality. +- The bound `sum d^2 <= U m_0` uses both nonnegativity and the residual degree + cap `d <= U`. +- The estimate still relies on the previously established threshold expansion + and `Lambda_0 <= C U^4/m_0`. + +## Material deliberately excluded + +This clean review does not promote the following PR #27 items: + +- the complete Section 8 global skeleton inequality; +- the factor-four theorem-constant improvement; +- the stronger four-support entropy certificate; +- the three-size profile; +- non-midpoint root placement; +- literature-dependent fixed-density and upper-bound corollaries. + +Those claims may be correct, but their complete interfaces require separate +review. Keeping them out of this focused change prevents a verified finite +simplification from being coupled to broader speculative or still-unintegrated +claims. From 72d52b8a7e18c87bdfcb7c1cd6ca4a29900f3a25 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:51:14 +0300 Subject: [PATCH 3/5] Add exact Section 7 and 9 super-check script --- .../section7_section9_supercheck.py | 185 ++++++++++++++++++ 1 file changed, 185 insertions(+) create mode 100644 625/experiments/section7_section9_supercheck.py diff --git a/625/experiments/section7_section9_supercheck.py b/625/experiments/section7_section9_supercheck.py new file mode 100644 index 00000000..c1491a44 --- /dev/null +++ b/625/experiments/section7_section9_supercheck.py @@ -0,0 +1,185 @@ +#!/usr/bin/env python3 +"""Exact super-checks for two proposed Erdős 625 simplifications. + +All assertions use integer or Fraction arithmetic. The script checks: + * the Section 7 central-rate endpoint inequalities with rigorous rational + intervals for logarithms; + * exhaustive restriction injectivity for even subgraphs on small complete + bipartite graphs; + * the weighted subset-product inequality for several rational weight systems; + * the off-matching square-sum inequality used in the Section 9 envelope. + +These finite checks are regression tests, not a proof of the asymptotic theorem. +""" +from __future__ import annotations + +from fractions import Fraction +from itertools import combinations, product +from typing import Iterable, Iterator + + +def require(condition: bool, message: str) -> None: + """Raise even under ``python -O`` when a verification condition fails.""" + if not condition: + raise RuntimeError(message) + + +def log_bounds(r: Fraction, terms: int = 120) -> tuple[Fraction, Fraction]: + """Rigorous bounds for log(r) via 2*atanh((r-1)/(r+1)).""" + if r <= 0: + raise ValueError("log requires r > 0") + if r == 1: + return Fraction(0), Fraction(0) + if r < 1: + lo, hi = log_bounds(1 / r, terms) + return -hi, -lo + x = (r - 1) / (r + 1) + partial = sum( + Fraction(2) * x ** (2 * k + 1) / (2 * k + 1) + for k in range(terms) + ) + # 1/(2k+1) <= 1/(2*terms+1) for k >= terms. + tail = ( + Fraction(2, 2 * terms + 1) + * x ** (2 * terms + 1) + / (1 - x * x) + ) + return partial, partial + tail + + +def central_rate_certificate() -> None: + """Prove the three endpoint signs used for Phi_T <= -(1-R)/100.""" + q_lo, q_hi = log_bounds(Fraction(2), terms=32) + c = Fraction(1, 100) + + # R=1/64 and log R = -6 log 2 exactly. + r0 = Fraction(1, 64) + f0_upper = r0 * (-Fraction(7, 2) * q_lo - 1) + c * (1 - r0) + require(f0_upper < 0, "central-rate endpoint R=1/64 failed") + + r1 = Fraction(47, 100) + _, log_r1_hi = log_bounds(r1) + f1_upper = r1 * log_r1_hi + (Fraction(5, 2) * q_hi - 1) * r1 + c * (1 - r1) + h1_upper = r1 * log_r1_hi + (1 - q_lo / 2 + c) * (1 - r1) + require(f1_upper < 0, "central-rate first bound at R=47/100 failed") + require(h1_upper < 0, "central-rate second bound at R=47/100 failed") + + +def all_partial_matchings(nr: int, nc: int) -> Iterator[frozenset[tuple[int, int]]]: + edges = tuple((i, j) for i in range(nr) for j in range(nc)) + for size in range(min(nr, nc) + 1): + for chosen in combinations(edges, size): + rows = {i for i, _ in chosen} + cols = {j for _, j in chosen} + if len(rows) == size and len(cols) == size: + yield frozenset(chosen) + + +def is_even(edges: Iterable[tuple[int, int]], nr: int, nc: int) -> bool: + row = [0] * nr + col = [0] * nc + for i, j in edges: + row[i] ^= 1 + col[j] ^= 1 + return not any(row) and not any(col) + + +def subsets(items: tuple[tuple[int, int], ...]) -> Iterator[frozenset[tuple[int, int]]]: + for mask in range(1 << len(items)): + yield frozenset(items[k] for k in range(len(items)) if (mask >> k) & 1) + + +def residual_restriction_exhaustive() -> tuple[int, int]: + """Exhaust all M,R,F for K_2,2, K_2,3 and K_3,3.""" + relation_cases = 0 + even_sets_checked = 0 + weight_patterns = ( + (Fraction(1, 7), Fraction(2, 5), Fraction(3, 4), Fraction(5, 3)), + (Fraction(0), Fraction(1, 3), Fraction(7, 5), Fraction(11, 2)), + ) + for nr, nc in ((2, 2), (2, 3), (3, 3)): + all_edges = frozenset((i, j) for i in range(nr) for j in range(nc)) + for matching in all_partial_matchings(nr, nc): + remaining = tuple(sorted(all_edges - matching)) + for residual in subsets(remaining): + relation_cases += 1 + universe = tuple(sorted(matching | residual)) + images: dict[frozenset[tuple[int, int]], frozenset[tuple[int, int]]] = {} + even_family: list[frozenset[tuple[int, int]]] = [] + for edge_set in subsets(universe): + if not is_even(edge_set, nr, nc): + continue + even_sets_checked += 1 + image = edge_set - matching + require(image not in images, "even completion restriction was not injective") + images[image] = edge_set + even_family.append(edge_set) + + for pattern in weight_patterns: + weights = { + edge: pattern[k % len(pattern)] + for k, edge in enumerate(sorted(residual)) + } + lhs = sum( + ( + _product(weights[e] for e in edge_set - matching) + for edge_set in even_family + ), + Fraction(0), + ) + rhs = _product(1 + weights[e] for e in residual) + require(lhs <= rhs, "weighted restriction product bound failed") + return relation_cases, even_sets_checked + + +def _product(values: Iterable[Fraction]) -> Fraction: + out = Fraction(1) + for value in values: + out *= value + return out + + +def square_sum_exhaustive() -> int: + """Check off-matching <= unrestricted factorized square sum.""" + checked = 0 + for nr, nc in ((2, 2), (2, 3), (3, 2), (3, 3)): + matchings = tuple(all_partial_matchings(nr, nc)) + for cap in range(1, 7): + for row_deg in product(range(cap + 1), repeat=nr): + total = sum(row_deg) + if total == 0: + continue + for col_deg in product(range(cap + 1), repeat=nc): + if sum(col_deg) != total: + continue + row_sq = sum(d * d for d in row_deg) + col_sq = sum(d * d for d in col_deg) + full = row_sq * col_sq + require(row_sq <= cap * total, "row square-sum cap failed") + require(col_sq <= cap * total, "column square-sum cap failed") + require(full <= cap * cap * total * total, "factorized square-sum cap failed") + for matching in matchings: + off = sum( + row_deg[i] ** 2 * col_deg[j] ** 2 + for i in range(nr) + for j in range(nc) + if (i, j) not in matching + ) + require(off <= full, "off-matching square sum exceeded full sum") + checked += 1 + return checked + + +def main() -> None: + central_rate_certificate() + relations, even_sets = residual_restriction_exhaustive() + squares = square_sum_exhaustive() + print("ERDOS 625 SECTION 7/9 SUPERCHECK: PASS") + print(" central-rate endpoint inequalities: exact Fraction bounds") + print(f" residual relations exhausted: {relations}") + print(f" even edge sets checked: {even_sets}") + print(f" square-sum instances checked: {squares}") + + +if __name__ == "__main__": + main() From 2640f9519977cd14a1c0ceaeb8c9d6e241f4190a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:53:10 +0300 Subject: [PATCH 4/5] Clarify the residual subset-product expansion --- 625/proofs/SECTION7_SECTION9_SUPERCHECK.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/625/proofs/SECTION7_SECTION9_SUPERCHECK.md b/625/proofs/SECTION7_SECTION9_SUPERCHECK.md index 3be9bd32..23dbe00b 100644 --- a/625/proofs/SECTION7_SECTION9_SUPERCHECK.md +++ b/625/proofs/SECTION7_SECTION9_SUPERCHECK.md @@ -135,6 +135,8 @@ therefore empty. \(\square\) \[ \sum_{F\text{ even}}\prod_{e\in F\setminus M}q_e \le + \sum_{S\subseteq R\setminus M}\prod_{e\in S}q_e + = \prod_{e\in R\setminus M}(1+q_e) \le \exp\!\left(\sum_{e\in R\setminus M}q_e\right). @@ -142,8 +144,8 @@ therefore empty. \(\square\) \] The first inequality follows from Lemma 2.1 by enlarging the image to the full -power set. The second is the finite identity for a subset generating function, -and the third uses \(1+x\le e^x\). +power set. The equality is the finite subset generating-function identity, +and the final inequality uses \(1+x\le e^x\). The finite injection already has a Lean counterpart in `EvenMatchingRestriction.lean`, and the generic product-to-exponential algebra From 9e40ff52bee811ca073ccff66dd5f5afa8be75ce Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:54:46 +0300 Subject: [PATCH 5/5] Add CI for the Section 7 and 9 super-check --- .../erdos625-section7-section9-supercheck.yml | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 .github/workflows/erdos625-section7-section9-supercheck.yml diff --git a/.github/workflows/erdos625-section7-section9-supercheck.yml b/.github/workflows/erdos625-section7-section9-supercheck.yml new file mode 100644 index 00000000..90eebe9a --- /dev/null +++ b/.github/workflows/erdos625-section7-section9-supercheck.yml @@ -0,0 +1,36 @@ +name: Erdős 625 Section 7 and 9 supercheck + +on: + pull_request: + paths: + - "625/proofs/SECTION7_SECTION9_SUPERCHECK.md" + - "625/audits/SECTION7_SECTION9_SUPERCHECK.md" + - "625/experiments/section7_section9_supercheck.py" + - ".github/workflows/erdos625-section7-section9-supercheck.yml" + push: + branches: + - main + paths: + - "625/proofs/SECTION7_SECTION9_SUPERCHECK.md" + - "625/audits/SECTION7_SECTION9_SUPERCHECK.md" + - "625/experiments/section7_section9_supercheck.py" + - ".github/workflows/erdos625-section7-section9-supercheck.yml" + +permissions: + contents: read + +jobs: + exact-supercheck: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - name: Compile the checker + run: python -m py_compile 625/experiments/section7_section9_supercheck.py + - name: Run exact checks + run: python 625/experiments/section7_section9_supercheck.py + - name: Verify optimization-independent failure handling + run: python -O 625/experiments/section7_section9_supercheck.py