Certify a stronger four-support entropy advantage

.github/workflows/erdos625-four-support-entropy-certificate.yml

@@ -0,0 +1,34 @@
+name: Erdős 625 four-support entropy certificate
+
+on:
+  pull_request:
+    paths:
+      - "625/proofs/FOUR_SUPPORT_ENTROPY_CERTIFICATE.md"
+      - "625/audits/FOUR_SUPPORT_ENTROPY_CERTIFICATE_AUDIT.md"
+      - "625/experiments/four_support_entropy_certificate.py"
+      - ".github/workflows/erdos625-four-support-entropy-certificate.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  exact-certificate:
+    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/four_support_entropy_certificate.py
+
+      - name: Run exact certificate
+        run: python 625/experiments/four_support_entropy_certificate.py
+
+      - name: Verify optimization-independent gates
+        run: python -O 625/experiments/four_support_entropy_certificate.py

625/audits/FOUR_SUPPORT_ENTROPY_CERTIFICATE_AUDIT.md

@@ -0,0 +1,126 @@
+# Audit of the stronger Erdős 625 four-support entropy certificate
+
+**Audit date:** 24 July 2026  
+**Verdict:** **PASS for the stated limiting entropy certificate.**
+
+This audit checks the elementary weight comparison only. It is not an
+independent proof of the finite-`n` root displacement, normalized second moment,
+or final theorem.
+
+## 1. Claim audited
+
+For the retained support `S_4={2,3,4,5}`, the proposed certificate is
+
+\[
+ D_4(\delta)<\ln\frac{639}{500},
+ \qquad
+ \ln2-D_4(\delta)>\ln\frac{1000}{639}
+\]
+
+uniformly for the complete limiting phase interval.
+
+## 2. Independent structure check
+
+For a fixed target mean, the retained optimizer has weights
+
+\[
+ w_i(\lambda)=\exp\left(\lambda i-\frac{\ln2}{2}i^2\right).
+\]
+
+The retained mean is strictly increasing in `lambda`. The omitted low-to-kept
+ratio decreases because every low omitted index is smaller than every retained
+index. The omitted high-to-kept ratio increases because every high omitted
+index is larger than every retained index.
+
+Evaluating the full-support dual function at the retained optimizer gives
+
+\[
+ D_4\le\ln(1+L+H).
+\]
+
+These are the same monotonicity and dual-evaluation facts used by the canonical
+Lemma 5.1.
+
+## 3. Exact interval checks
+
+The checker encloses
+
+\[
+ q=\ln2
+\]
+
+using the positive series
+
+\[
+ q=2\sum_{k\ge0}\frac{(1/3)^{2k+1}}{2k+1}
+\]
+
+and an explicit geometric tail. It encloses `x=2^(1/20)` by checking the
+rational twentieth powers.
+
+Every subsequent comparison uses only `Fraction` arithmetic. In particular it
+checks:
+
+1. the retained mean at `49q/20` is below `2/q`;
+2. the retained mean at `83q/20` is above `1+2/q`;
+3. `L(49q/20)<263/1000`;
+4. `H(29q/10)<3/200`;
+5. `L(29q/10)<33/250`;
+6. `H(83q/20)<29/200`.
+
+The two monotonicity cases give respectively
+
+\[
+ \frac{263}{1000}+\frac3{200}=\frac{139}{500}
+\]
+
+and
+
+\[
+ \frac{33}{250}+\frac{29}{200}=\frac{277}{1000}
+ <\frac{139}{500}.
+\]
+
+No floating-point comparison enters the proof certificate.
+
+## 4. Tail directions checked
+
+The potentially error-prone interval directions were checked separately.
+
+- For positive exponents, upper numerators use the upper enclosure for `x` and
+  lower denominators use the lower enclosure.
+- For negative exponents, an upper bound uses the lower positive enclosure for
+  `x`.
+- At `29q/10`, the high tail starts with exponent `-12`; the first ratio is
+  `x^(-72)` and later ratios are smaller.
+- At `83q/20`, the high exponents are `138,91,24,-63,...`; after the exponent
+  `-63`, the first remaining ratio is `x^(-107)` and later ratios are smaller.
+- In the upper mean bracket, negative coefficients are paired with upper weight
+  bounds and positive coefficients with lower weight bounds.
+
+The displayed tail and mean inequalities therefore have the correct one-sided
+directions.
+
+## 5. Regression and optimization independence
+
+`625/experiments/four_support_entropy_certificate.py` uses explicit exceptions,
+not Python `assert`. The exact gates remain active under `python -O`.
+
+The same script performs a separate floating-point phase scan. That scan is
+labelled diagnostic and is not used to establish the rational certificate.
+
+## 6. Consequence boundary
+
+The audit supports replacing the limiting entropy advantage in Lemma 5.1 by
+
+\[
+ \ln2-D_4(\delta)>\ln(1000/639).
+\]
+
+To change the canonical theorem constant, a separate review must verify how
+this limiting inequality is transported to the finite optimizer and combined
+with the root displacement and final rounding. PR #31 addresses the latter
+propagation independently.
+
+No external peer review, priority claim, or complete formal verification is
+asserted.

625/experiments/four_support_entropy_certificate.py

@@ -0,0 +1,216 @@
+#!/usr/bin/env python3
+"""Exact certificate and diagnostics for the Erdős 625 four-support entropy loss.
+
+The exact part proves, by rational interval arithmetic,
+    D_4(delta) < log(639/500),
+    log(2)-D_4(delta) > log(1000/639).
+
+The continuum scan is diagnostic only.
+"""
+from __future__ import annotations
+
+from fractions import Fraction
+from pathlib import Path
+import math
+
+Q_LO = Fraction(693147180559, 10**12)
+Q_HI = Fraction(693147180560, 10**12)
+X_LO = Fraction(1035264923841, 10**12)  # lower bound for 2^(1/20)
+X_HI = Fraction(1035264923842, 10**12)
+
+
+def require(condition: bool, message: str) -> None:
+    """Raise even under ``python -O`` when a verification condition fails."""
+    if not condition:
+        raise RuntimeError(message)
+
+
+def certify_constants() -> None:
+    """Certify rational intervals for log(2) and 2^(1/20)."""
+    a = Fraction(1, 3)
+    terms = 14
+    partial = sum(
+        Fraction(2) * a ** (2 * k + 1) / (2 * k + 1)
+        for k in range(terms)
+    )
+    tail = (
+        Fraction(2, 2 * terms + 1)
+        * a ** (2 * terms + 1)
+        / (1 - a * a)
+    )
+    require(Q_LO < partial, "lower log(2) enclosure failed")
+    require(partial + tail < Q_HI, "upper log(2) enclosure failed")
+    require(X_LO**20 < 2 < X_HI**20, "twentieth-root enclosure failed")
+
+
+def certify_tilt_bracket() -> None:
+    """Certify (49/20)q < lambda_4 < (83/20)q."""
+    # At lambda=(49/20)q, after a common shift the retained exponents are
+    # 63, 62, 41, 0 for deficits 2, 3, 4, 5.
+    numerator_hi = 2 * X_HI**63 + 3 * X_HI**62 + 4 * X_HI**41 + 5
+    denominator_lo = X_LO**63 + X_LO**62 + X_LO**41 + 1
+    require(
+        Q_HI * numerator_hi < 2 * denominator_lo,
+        "lower tilt does not certify mean < 2/q",
+    )
+
+    # At lambda=(83/20)q, the retained exponents are 126,159,172,165.
+    lower_sum = Fraction(0)
+    for i, exponent in ((2, 126), (3, 159), (4, 172), (5, 165)):
+        coefficient = Q_LO * (i - 1) - 2
+        power = X_HI**exponent if coefficient < 0 else X_LO**exponent
+        lower_sum += coefficient * power
+    require(
+        lower_sum > 0,
+        "upper tilt does not certify mean > 1+2/q",
+    )
+
+
+def certify_omitted_ratios() -> dict[str, Fraction]:
+    """Certify the four rational low/high omitted-ratio bounds."""
+    # L((49/20)q): shift by the deficit -1 exponent.
+    low_num_hi = 1 + X_HI**59 + X_HI**98
+    kept_den_lo = X_LO**117 + X_LO**116 + X_LO**95 + X_LO**54
+    require(
+        1000 * low_num_hi < 263 * kept_den_lo,
+        "L(49q/20) bound failed",
+    )
+
+    # H((29/10)q): deficit 6 has exponent -12 and subsequent ratios are
+    # at most x^(-72).
+    high_split_hi = X_LO**(-12) / (1 - X_LO**(-72))
+    kept_split_lo = X_LO**76 + X_LO**84 + X_LO**72 + X_LO**40
+    require(
+        200 * high_split_hi < 3 * kept_split_lo,
+        "H(29q/10) bound failed",
+    )
+
+    # L((29/10)q): normalized low exponents 0,68,116 and retained
+    # exponents 144,152,140,108.
+    low_split_hi = 1 + X_HI**68 + X_HI**116
+    kept_shifted_lo = X_LO**144 + X_LO**152 + X_LO**140 + X_LO**108
+    require(
+        250 * low_split_hi < 33 * kept_shifted_lo,
+        "L(29q/10) bound failed",
+    )
+
+    # H((83/20)q): high exponents 138,91,24,-63,...; after deficit 9
+    # every successive ratio is at most x^(-107).
+    high_upper_hi = (
+        X_HI**138
+        + X_HI**91
+        + X_HI**24
+        + X_LO**(-63) / (1 - X_LO**(-107))
+    )
+    kept_upper_lo = X_LO**126 + X_LO**159 + X_LO**172 + X_LO**165
+    require(
+        200 * high_upper_hi < 29 * kept_upper_lo,
+        "H(83q/20) bound failed",
+    )
+
+    low_case = Fraction(263, 1000) + Fraction(3, 200)
+    high_case = Fraction(33, 250) + Fraction(29, 200)
+    require(low_case == Fraction(139, 500), "low-case rational sum changed")
+    require(high_case == Fraction(277, 1000), "high-case rational sum changed")
+    require(high_case < low_case, "case ordering changed")
+    return {
+        "L_lower": Fraction(263, 1000),
+        "H_split": Fraction(3, 200),
+        "L_split": Fraction(33, 250),
+        "H_upper": Fraction(29, 200),
+        "omitted": low_case,
+    }
+
+
+def value_function(support: tuple[int, ...], target: float) -> float:
+    """Numerically evaluate the limiting constrained value."""
+    q = math.log(2.0)
+    lo, hi = -20.0, 20.0
+    for _ in range(90):
+        lam = (lo + hi) / 2
+        scores = [lam * i - q * i * i / 2 for i in support]
+        top = max(scores)
+        weights = [math.exp(score - top) for score in scores]
+        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
+    scores = [lam * i - q * i * i / 2 for i in support]
+    top = max(scores)
+    log_partition = top + math.log(
+        sum(math.exp(score - top) for score in scores)
+    )
+    return log_partition - lam * target
+
+
+def phase_scan(points: int = 2001) -> tuple[float, float, float]:
+    """Diagnostic scan; not used by the rational certificate."""
+    q = math.log(2.0)
+    support4 = (2, 3, 4, 5)
+    plus60 = tuple(range(-1, 60))
+    plus90 = tuple(range(-1, 90))
+    best = (float("inf"), 0.0)
+    truncation = 0.0
+    for step in range(points):
+        delta = step / (points - 1)
+        target = 1 + 2 / q - delta
+        value4 = value_function(support4, target)
+        value60 = value_function(plus60, target)
+        value90 = value_function(plus90, target)
+        truncation = max(truncation, abs(value60 - value90))
+        advantage = q - (value90 - value4)
+        if advantage < best[0]:
+            best = (advantage, delta)
+    return best[0], best[1], truncation
+
+
+def source_check() -> str:
+    """Guard the canonical definitions used by this certificate."""
+    path = Path("625/proofs/COMPLETE_PROOF_SELF_CONTAINED.md")
+    if not path.exists():
+        return "SKIPPED"
+    text = path.read_text(encoding="utf-8")
+    for tag in ("\\tag{5.1}", "\\tag{5.2}", "\\tag{5.3}", "\\tag{5.7}"):
+        require(tag in text, f"missing canonical equation tag {tag}")
+    return "PASS"
+
+
+def main() -> None:
+    certify_constants()
+    certify_tilt_bracket()
+    bounds = certify_omitted_ratios()
+    minimum, delta, truncation = phase_scan()
+    gamma = math.log(1000 / 639)
+    q = math.log(2.0)
+
+    print("ERDOS 625 FOUR-SUPPORT ENTROPY CERTIFICATE: PASS")
+    print("  tilt bracket: (49/20)q < lambda_4 < (83/20)q")
+    print(f"  L(49q/20) < {bounds['L_lower']}")
+    print(f"  H(29q/10) < {bounds['H_split']}")
+    print(f"  L(29q/10) < {bounds['L_split']}")
+    print(f"  H(83q/20) < {bounds['H_upper']}")
+    print(f"  uniform omitted ratio < {bounds['omitted']}")
+    print("  D_4(delta) < log(639/500)")
+    print("  log(2)-D_4(delta) > log(1000/639)")
+    print(f"  certificate gamma = {gamma:.15f}")
+    print(
+        "  coefficient with current /32 propagation = "
+        f"{q*q*gamma/32:.15f}"
+    )
+    print(
+        "  coefficient combined with PR #31 /8 propagation = "
+        f"{q*q*gamma/8:.15f}"
+    )
+    print(f"  canonical source scan: {source_check()}")
+    print("DIAGNOSTIC ONLY:")
+    print(
+        f"  phase-grid min advantage = {minimum:.15f} "
+        f"at delta={delta:.6f}"
+    )
+    print(f"  S_plus truncation disagreement = {truncation:.3e}")
+
+
+if __name__ == "__main__":
+    main()