From bfc19dbd96ff9791c2b71626cc61f5fc89ced157 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:01:16 +0300 Subject: [PATCH 1/4] Add root-gap constant propagation note --- 625/proofs/ROOT_GAP_CONSTANT_PROPAGATION.md | 273 ++++++++++++++++++++ 1 file changed, 273 insertions(+) create mode 100644 625/proofs/ROOT_GAP_CONSTANT_PROPAGATION.md diff --git a/625/proofs/ROOT_GAP_CONSTANT_PROPAGATION.md b/625/proofs/ROOT_GAP_CONSTANT_PROPAGATION.md new file mode 100644 index 00000000..7b43fd12 --- /dev/null +++ b/625/proofs/ROOT_GAP_CONSTANT_PROPAGATION.md @@ -0,0 +1,273 @@ +# Erdős 625: root-gap constant propagation and placement experiment + +**Status.** This is a focused mathematical review note. It derives a sharper +constant from equations already stated in the canonical candidate manuscript. +It does not alter the canonical manuscript, publication PDFs, Lean sources, or +`Erdos625Statement`. + +Throughout, put + +\[ + q=\ln 2,\qquad N=\ln n,\qquad H_n=\frac{n}{N^3}, +\] + +and define the limiting four-support advantage + +\[ + A(\delta)=q-D_4(\delta),\qquad + \gamma_4=\ln\frac{200}{153}. +\] + +The inputs used below are: + +1. the uniform root-displacement formula from equation (5.11), + \[ + r_+(n)-r_4^{co}(n) + =\left(\frac{q^2}{4}A(\delta_n)+o(1)\right)H_n; + \tag{1.1} + \] +2. the midpoint integer from equation (5.13), + \[ + k_{co}=\left\lceil\frac{r_4^{co}+r_+}{2}\right\rceil; + \tag{1.2} + \] +3. the chromatic lower integer + \[ + k_\chi^-=\lfloor r_+\rfloor-\lceil N\rceil; + \tag{1.3} + \] +4. the amplification loss `a_n=o(H_n)` from equations (10.12)--(10.13). + +All uses of `o(1)` in this note inherit the manuscript's asserted uniformity in +the complete phase parameter. + +## 1. Exact floor-and-ceiling loss + +### Lemma 1.1 + +For real numbers `x>y` and `L>=0`, define + +\[ + K_\chi=\lfloor x\rfloor-\lceil L\rceil, + \qquad + K_{1/2}=\left\lceil\frac{x+y}{2}\right\rceil. +\] + +Then + +\[ + \boxed{ + K_\chi-K_{1/2}> + \frac{x-y}{2}-L-3.} + \tag{1.4} +\] + +#### Proof + +Use + +\[ + \lfloor x\rfloor>x-1, + \qquad + \lceil L\rceil + (1-\theta)(x-y)-L-3.} + \tag{1.5} +\] + +Equation (1.5) is exact deterministic arithmetic. Whether a non-midpoint +choice preserves every later second-moment estimate is a separate question. + +## 2. The midpoint retains the full phase-resolved coefficient + +Apply Lemma 1.1 with + +\[ + x=r_+(n),\qquad y=r_4^{co}(n),\qquad L=N. +\] + +Equations (1.1)--(1.3) give + +\[ + \begin{aligned} + k_\chi^- - k_{co} + &>\frac12\{r_+-r_4^{co}\}-N-3\\ + &=\left( + \frac{q^2}{8}A(\delta_n)+o(1) + \right)H_n, + \end{aligned} + \tag{2.1} +\] + +because + +\[ + \frac{N+3}{H_n}=\frac{(N+3)N^3}{n}\longrightarrow0. + \tag{2.2} +\] + +No witness or profile is changed here: `k_co` remains exactly the midpoint +integer used in the canonical manuscript. In particular, the signed +first-moment margin and every subsequent overlap estimate are the same ones +already invoked there. + +## 3. Amplification does not consume the coefficient + +On the intersection of the two high-probability events used in Section 11, + +\[ + \chi(G_n)>k_\chi^-, + \qquad + \zeta(G_n)\le k_{co}+a_n, +\] + +one has + +\[ + \chi(G_n)-\zeta(G_n) + > k_\chi^- - k_{co}-a_n. + \tag{3.1} +\] + +Since `a_n=o(H_n)`, equation (2.1) yields the phase-resolved conclusion + +\[ + \boxed{ + \chi(G_n)-\zeta(G_n) + \ge + \left( + \frac{q^2}{8}A(\delta_n)-o(1) + \right)H_n} + \tag{3.2} +\] + +with high probability. + +This is only a propagation of the manuscript's own root formula. It uses no +new second-moment or concentration estimate. + +## 4. A factor-four explicit constant + +The proof of Lemma 5.1 supplies a uniform strict inequality + +\[ + A(\delta)>\gamma_4 + \qquad(0\le\delta\le1). + \tag{4.1} +\] + +The limiting value functions, and hence `A`, are continuous on the closed phase +interval. Equivalently, one may use the fixed strict omitted-mass bounds inside +the proof of Lemma 5.1. In either formulation there is an `eta_0>0` such that + +\[ + A(\delta)\ge\gamma_4+\eta_0 + \qquad(0\le\delta\le1). + \tag{4.2} +\] + +Combining (3.2) and (4.2), and absorbing the uniform `o(1)`, gives for all +sufficiently large `n` + +\[ + \boxed{ + \chi(G_n)-\zeta(G_n) + \ge + \frac{q^2}{8}\ln\frac{200}{153} + \frac{n}{(\ln n)^3}} + \tag{4.3} +\] + +with high probability, conditional on the correctness and stated uniformity of +the canonical proof chain. + +The currently displayed coefficient is + +\[ + \frac{q^2}{32}\ln\frac{200}{153}. +\] + +Thus (4.3) is a factor-four constant improvement obtained without changing the +four-size profile or any probabilistic estimate. + +## 5. Numerical phase scan — diagnostic only + +The accompanying standard-library script also scans the limiting variational +problem. With the unrestricted support truncated at deficits 59 and 89, the two +computations agree to displayed floating-point precision. On a 1001-point phase +grid it reports approximately + +\[ + \min_{0\le\delta\le1}A(\delta) + \approx0.520701335491, + \] + +attained at the endpoint `delta=1` on that grid. This would correspond to the +phase-uniform coefficient + +\[ + \frac{q^2}{8}\min A\approx0.031271565748. +\] + +This scan is evidence about available slack, not a proof and not a proposed +replacement constant. + +## 6. Root-placement experiment + +Equation (1.5) suggests replacing the midpoint by + +\[ + k_\theta= + \left\lceil + r_4^{co}+\theta(r_+-r_4^{co}) + \right\rceil, + \qquad 0<\theta<1. + \tag{6.1} +\] + +The deterministic retained gap would be + +\[ + \left( + (1-\theta)\frac{q^2}{4}A(\delta_n)+o(1) + \right)H_n. + \tag{6.2} +\] + +At the level of the continuous first-moment objective, the distance from the +signed root is `theta` times the root separation, so every fixed `theta>0` +should retain a positive exponential first-moment margin of order `n/N`. +However, the constants in the partial-diagonal and dense-overlap estimates must +be replayed with their dependence on that margin exposed. Therefore (6.2) is an +experimental route, not a theorem claimed by this note. + +A conservative next test would be `theta=1/4`, which increases the retained +root gap by a factor `3/2` relative to the midpoint while retaining one quarter +of the continuous signed-root margin. + +## 7. Scope boundary + +This note does not verify equation (5.11), Lemma 5.1, Proposition 9.2, or the +amplification theorem independently. It verifies the deterministic rounding and +coefficient propagation once those canonical inputs, including their uniformity, +are accepted. The exact checker is a regression test and not a substitute for +the asymptotic argument. \ No newline at end of file From 11354bf3e9ad7c9fe120ae93efceb48f2a39ae3f Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:01:45 +0300 Subject: [PATCH 2/4] Add root-gap propagation audit --- .../ROOT_GAP_CONSTANT_PROPAGATION_AUDIT.md | 148 ++++++++++++++++++ 1 file changed, 148 insertions(+) create mode 100644 625/audits/ROOT_GAP_CONSTANT_PROPAGATION_AUDIT.md diff --git a/625/audits/ROOT_GAP_CONSTANT_PROPAGATION_AUDIT.md b/625/audits/ROOT_GAP_CONSTANT_PROPAGATION_AUDIT.md new file mode 100644 index 00000000..9911e7f5 --- /dev/null +++ b/625/audits/ROOT_GAP_CONSTANT_PROPAGATION_AUDIT.md @@ -0,0 +1,148 @@ +# Audit of the Erdős 625 root-gap constant propagation + +**Audit date:** 24 July 2026 +**Canonical base:** repository `main` at the branch point of this PR +**Verdict:** **PASS conditional on the canonical inputs explicitly listed below.** + +This is an arithmetic/asymptotic propagation audit. It is not an independent +verification of the signed second moment or of `Erdos625Statement`. + +## 1. Inputs treated as hypotheses + +The audit uses only the following claims from the canonical candidate +manuscript: + +1. equation (5.11), uniformly in the phase, + \[ + r_+-r_4^{co} + =\left(\frac{q^2}{4}\{q-D_4(\delta)\}+o(1)\right) + \frac{n}{N^3}; + \] +2. the exact midpoint definition (5.13); +3. the chromatic lower integer from (4.1); +4. the uniform strict entropy advantage in Lemma 5.1; +5. the deterministic amplification loss `a_n=o(n/N^3)` from (10.12)--(10.13); +6. the final event intersection used in Section 11. + +No conclusion of this audit should be read as an independent proof of those +inputs. + +## 2. Independent derivation + +Let `x=r_+`, `y=r_4^{co}`, and `L=N`. The exact inequalities + +\[ + \lfloor x\rfloor>x-1, + \qquad + \lceil L\rceil rac{x-y}{2}-N-3. +\] + +Since + +\[ + \frac{N+3}{n/N^3}=\frac{(N+3)N^3}{n}\to0, +\] + +equation (5.11) implies + +\[ + k_\chi^- - k_{co} + =\left(\frac{q^2}{8}\{q-D_4(\delta_n)\}+o(1)\right) + \frac{n}{N^3} +\] + +in the one-sided form required by the proof. + +Subtracting `a_n=o(n/N^3)` does not change this coefficient. Therefore the +phase-resolved final gap has coefficient + +\[ + \frac{q^2}{8}\{q-D_4(\delta_n)\}. +\] + +The factor `1/8` comes from the coefficient `1/4` in the root displacement and +the single midpoint factor `1/2`. There is no second asymptotic halving forced +by integer rounding or amplification. + +## 3. Uniform explicit constant + +Lemma 5.1 gives + +\[ + q-D_4(\delta)>\gamma_4:=\ln(200/153) +\] + +on the closed phase interval. The limiting value functions are continuous, so +the strict inequality has uniform positive slack. The same conclusion can be +read directly from the fixed strict omitted-weight bounds in the proof of Lemma +5.1. + +Consequently the phase-resolved coefficient eventually dominates + +\[ + \frac{q^2\gamma_4}{8}. +\] + +The currently displayed theorem uses `q^2 gamma_4/32`; the proposed arithmetic +corollary is therefore exactly four times larger. + +## 4. Exact regression checker + +`625/experiments/root_gap_constant_supercheck.py` performs: + +- 55,296 exact `Fraction` checks of the midpoint and general-`theta` + floor/ceiling inequality; +- an exact decimal identity check that the propagated displayed coefficient is + four times the current coefficient; +- a canonical equation-tag scan when run from the repository root; +- a numerical limiting-phase scan, clearly marked diagnostic; +- a finite-`n` table showing the decay of the additive rounding loss relative to + `n/(log n)^3`. + +The checker uses explicit exceptions rather than Python `assert`, so its gates +remain active under `python -O`. + +## 5. Adversarial checks + +### Could the rounding loss contain another factor of two? + +No. The exact loss is additive, bounded by `N+3`, not multiplicative. Since +`N=o(n/N^3)`, it disappears after normalization. + +### Does amplification halve the gap? + +No. The amplification theorem contributes an additive deterministic loss +`a_n=o(n/N^3)`. It does not multiply the root separation by a fixed constant. + +### Is pointwise strictness enough for the displayed constant? + +Pointwise strictness alone on a noncompact domain would not be enough. Here the +phase interval closes at `delta=1`, the limiting value functions are continuous, +and the proof of Lemma 5.1 itself uses fixed strict numerical bounds. Hence a +uniform slack exists. + +### Does this alter the witness profile? + +No. The integer `k_co` is the same midpoint integer as in the canonical proof. +No Section 7--9 estimate is rerun or weakened. + +## 6. Remaining boundary + +The audit does not independently establish: + +- the uniform `o(1)` in equation (5.11); +- continuity and exact finite-`n` approximation of the entropy loss; +- the complete normalized second moment; +- the rare-seed amplification theorem; +- external peer review or formal verification. + +Within the stated dependency boundary, no additional loss reducing +`q^2 gamma_4/8` to `q^2 gamma_4/32` was found. \ No newline at end of file From 911c2607873e45ad2849f2f41eb90ae0e83aa84d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:02:29 +0300 Subject: [PATCH 3/4] Add exact root-gap constant checker --- .../root_gap_constant_supercheck.py | 195 ++++++++++++++++++ 1 file changed, 195 insertions(+) create mode 100644 625/experiments/root_gap_constant_supercheck.py diff --git a/625/experiments/root_gap_constant_supercheck.py b/625/experiments/root_gap_constant_supercheck.py new file mode 100644 index 00000000..6df3e051 --- /dev/null +++ b/625/experiments/root_gap_constant_supercheck.py @@ -0,0 +1,195 @@ +#!/usr/bin/env python3 +"""Exact and diagnostic checks for Erdős 625 root-gap constant propagation. + +Exact checks: + * midpoint and general-theta floor/ceiling inequalities on a rational grid; + * the factor-four coefficient arithmetic; + * canonical equation-tag presence when run from the repository root. + +Diagnostics, explicitly not proofs: + * a numerical scan of the limiting four-support advantage A(delta); + * the finite-n size of the additive rounding loss relative to n/(log n)^3. +""" +from __future__ import annotations + +from decimal import Decimal, getcontext +from fractions import Fraction +from pathlib import Path +import math + + +def require(condition: bool, message: str) -> None: + """Raise even under ``python -O`` when a verification condition fails.""" + if not condition: + raise RuntimeError(message) + + +def floor_fraction(x: Fraction) -> int: + return x.numerator // x.denominator + + +def ceil_fraction(x: Fraction) -> int: + return -((-x.numerator) // x.denominator) + + +def rounding_grid() -> tuple[int, Fraction, tuple[Fraction, ...]]: + """Check midpoint/general-theta inequalities on a structured exact grid.""" + fracs = tuple(Fraction(k, 12) for k in range(12)) + thetas = (Fraction(1, 2), Fraction(1, 4), Fraction(1, 10), Fraction(3, 4)) + checked = 0 + worst_deficit = Fraction(-10) + worst_case: tuple[Fraction, ...] = () + + for integer_gap in range(1, 9): + for fx in fracs: + for fy in fracs: + x = Fraction(20 + integer_gap) + fx + y = Fraction(20) + fy + if x <= y: + continue + gap = x - y + for fn in fracs: + nlog = Fraction(7) + fn + k_chi = floor_fraction(x) - ceil_fraction(nlog) + for theta in thetas: + k_theta = ceil_fraction(y + theta * gap) + lhs = k_chi - k_theta + main = (1 - theta) * gap - nlog + require( + lhs > main - 3, + "rounding inequality failed: " + f"x={x}, y={y}, N={nlog}, theta={theta}", + ) + deficit = main - lhs + if deficit > worst_deficit: + worst_deficit = deficit + worst_case = ( + x, + y, + nlog, + theta, + Fraction(lhs), + main, + ) + checked += 1 + return checked, worst_deficit, worst_case + + +def coefficient_arithmetic() -> tuple[Decimal, Decimal, Decimal]: + """Check the exact factor four between the displayed coefficients.""" + getcontext().prec = 60 + q = Decimal(2).ln() + gamma = (Decimal(200) / Decimal(153)).ln() + old = q * q * gamma / Decimal(32) + propagated = q * q * gamma / Decimal(8) + require( + propagated == Decimal(4) * old, + "factor-four coefficient identity failed", + ) + return old, propagated, gamma + + +def limiting_value(support: tuple[int, ...], target: float) -> tuple[float, float]: + """Numerically evaluate the limiting constrained entropy value.""" + q = math.log(2.0) + lo, hi = -20.0, 20.0 + for _ in range(90): + lam = (lo + hi) / 2.0 + weights = [math.exp(lam * i - q * i * i / 2.0) for i in support] + mean = sum(i * w for i, w in zip(support, weights)) / sum(weights) + if mean < target: + lo = lam + else: + hi = lam + lam = (lo + hi) / 2.0 + weights = [math.exp(lam * i - q * i * i / 2.0) for i in support] + partition = sum(weights) + value = math.log(partition) - lam * target + return lam, value + + +def phase_scan(points: int = 1001) -> tuple[float, float, float]: + """Diagnostic scan of A(delta)=log(2)-(F_plus-F_4).""" + q = math.log(2.0) + support4 = (2, 3, 4, 5) + support_plus_60 = tuple(range(-1, 60)) + support_plus_90 = tuple(range(-1, 90)) + best = (float("inf"), 0.0) + truncation_disagreement = 0.0 + + for k in range(points): + delta = k / (points - 1) + target = 1.0 + 2.0 / q - delta + _, value4 = limiting_value(support4, target) + _, value_plus_60 = limiting_value(support_plus_60, target) + _, value_plus_90 = limiting_value(support_plus_90, target) + truncation_disagreement = max( + truncation_disagreement, + abs(value_plus_60 - value_plus_90), + ) + advantage = q - (value_plus_90 - value4) + if advantage < best[0]: + best = (advantage, delta) + + return best[0], best[1], truncation_disagreement + + +def rounding_scale_table() -> list[tuple[int, Decimal]]: + """Diagnostic values of (N+3)N^3/n for widely separated n.""" + getcontext().prec = 80 + out: list[tuple[int, Decimal]] = [] + for exponent in (6, 12, 24, 48, 96, 192): + n = Decimal(10) ** exponent + log_n = n.ln() + ratio = (log_n + 3) * log_n**3 / n + out.append((exponent, ratio)) + return out + + +def source_tag_check() -> str: + """Guard the canonical equations on which the review note depends.""" + path = Path("625/proofs/COMPLETE_PROOF_SELF_CONTAINED.md") + if not path.exists(): + return "SKIPPED (canonical source not present in working directory)" + text = path.read_text(encoding="utf-8") + for tag in ("\\tag{5.11}", "\\tag{5.13}", "\\tag{10.13}", "\\tag{11.1}"): + require(tag in text, f"missing canonical equation tag {tag}") + return "PASS" + + +def main() -> None: + checked, worst_deficit, worst_case = rounding_grid() + old, propagated, gamma = coefficient_arithmetic() + min_advantage, min_delta, truncation_error = phase_scan() + source_status = source_tag_check() + + print("ERDOS 625 ROOT-GAP CONSTANT SUPERCHECK: PASS") + print(f" exact rounding cases: {checked}") + print( + " largest observed additive rounding deficit: " + f"{float(worst_deficit):.12f} (< 3)" + ) + print(f" worst grid case: {worst_case}") + print(f" current displayed coefficient: {old}") + print(f" factor-four propagated coefficient: {propagated}") + print(f" manuscript gamma: {gamma}") + print(f" canonical equation-tag scan: {source_status}") + print("DIAGNOSTIC ONLY:") + print( + f" scanned min A(delta): {min_advantage:.12f} " + f"at delta={min_delta:.6f}" + ) + print( + " corresponding q^2*A/8: " + f"{math.log(2.0) ** 2 * min_advantage / 8.0:.12f}" + ) + print( + " S_plus truncation disagreement (60 vs 90): " + f"{truncation_error:.3e}" + ) + for exponent, ratio in rounding_scale_table(): + print(f" n=10^{exponent}: (N+3)N^3/n = {ratio:.6E}") + + +if __name__ == "__main__": + main() From 3a4e41399e5da24cfd65bc190d9766b9a28818a1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:02:50 +0300 Subject: [PATCH 4/4] Add root-gap constant supercheck workflow --- .../erdos625-root-gap-constant-supercheck.yml | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 .github/workflows/erdos625-root-gap-constant-supercheck.yml diff --git a/.github/workflows/erdos625-root-gap-constant-supercheck.yml b/.github/workflows/erdos625-root-gap-constant-supercheck.yml new file mode 100644 index 00000000..c9ee523b --- /dev/null +++ b/.github/workflows/erdos625-root-gap-constant-supercheck.yml @@ -0,0 +1,34 @@ +name: Erdős 625 root-gap constant supercheck + +on: + pull_request: + paths: + - "625/proofs/ROOT_GAP_CONSTANT_PROPAGATION.md" + - "625/audits/ROOT_GAP_CONSTANT_PROPAGATION_AUDIT.md" + - "625/experiments/root_gap_constant_supercheck.py" + - ".github/workflows/erdos625-root-gap-constant-supercheck.yml" + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-supercheck: + runs-on: ubuntu-latest + steps: + - name: Check out repository + uses: actions/checkout@v4 + + - name: Set up Python + uses: actions/setup-python@v5 + with: + python-version: "3.x" + + - name: Compile checker + run: python -m py_compile 625/experiments/root_gap_constant_supercheck.py + + - name: Run exact and diagnostic checks + run: python 625/experiments/root_gap_constant_supercheck.py + + - name: Verify optimization-independent gates + run: python -O 625/experiments/root_gap_constant_supercheck.py