Verify factor-four root-gap constant propagation

.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

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<L+1,
+ \qquad
+ \left\lceil\frac{x+y}{2}\right\rceil<\frac{x+y}{2}+1
+\]
+
+give
+
+\[
+ k_\chi^- - k_{co}>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.

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()