diff --git a/.github/workflows/erdos625-four-support-entropy-certificate.yml b/.github/workflows/erdos625-four-support-entropy-certificate.yml new file mode 100644 index 00000000..2271ac6b --- /dev/null +++ b/.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 diff --git a/625/audits/FOUR_SUPPORT_ENTROPY_CERTIFICATE_AUDIT.md b/625/audits/FOUR_SUPPORT_ENTROPY_CERTIFICATE_AUDIT.md new file mode 100644 index 00000000..342b7c3e --- /dev/null +++ b/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. \ No newline at end of file diff --git a/625/experiments/four_support_entropy_certificate.py b/625/experiments/four_support_entropy_certificate.py new file mode 100644 index 00000000..57277e82 --- /dev/null +++ b/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() diff --git a/625/proofs/FOUR_SUPPORT_ENTROPY_CERTIFICATE.md b/625/proofs/FOUR_SUPPORT_ENTROPY_CERTIFICATE.md new file mode 100644 index 00000000..38a7ab6d --- /dev/null +++ b/625/proofs/FOUR_SUPPORT_ENTROPY_CERTIFICATE.md @@ -0,0 +1,261 @@ +# Erdős 625: an exact stronger four-support entropy certificate + +**Status.** This is a focused replacement certificate for Lemma 5.1 of the +candidate manuscript. It keeps the same four deficits + +\[ + S_4=\{2,3,4,5\} +\] + +and changes no later probabilistic argument. The note does not modify the +canonical manuscript, publication PDFs, Lean sources, or `Erdos625Statement`. + +Put + +\[ + q=\ln2, + \qquad + T\in\left[\frac2q,1+\frac2q\right]. +\] + +For a tilt `lambda`, write + +\[ + w_i(\lambda)=\exp\left(\lambda i-\frac q2i^2\right), + \qquad + Z_4(\lambda)=\sum_{i=2}^5w_i(\lambda). +\] + +Let `lambda_4(T)` be the unique tilt for which the retained mean equals `T`. +Define + +\[ + L(\lambda)= + \frac{\sum_{i=-1}^1w_i(\lambda)}{Z_4(\lambda)}, + \qquad + H(\lambda)= + \frac{\sum_{i\ge6}w_i(\lambda)}{Z_4(\lambda)}. +\] + +The low ratio `L` is decreasing in the tilt, while `H` is increasing. + +## 1. Exact rational enclosures + +Set + +\[ + x=2^{1/20}. +\] + +The accompanying checker proves by exact integer and rational arithmetic that + +\[ + 0.6931471805590, +\] + +which is equivalent to the mean being larger than `1+2/q`. Strict monotonicity +of the retained mean proves (2.1). \(\square\) + +## 3. Exact omitted-weight bounds + +Use the split tilt + +\[ + \lambda_s=\frac{29}{10}q. +\] + +The rational interval calculation proves + +\[ + L\left(\frac{49}{20}q\right)<\frac{263}{1000}, + \qquad + H\left(\frac{29}{10}q\right)<\frac3{200}, + \tag{3.1} +\] + +and + +\[ + L\left(\frac{29}{10}q\right)<\frac{33}{250}, + \qquad + H\left(\frac{83}{20}q\right)<\frac{29}{200}. + \tag{3.2} +\] + +For reference, the exponent patterns used by the exact checker are: + +- at `49q/20`, after division by the deficit `-1` weight, the low exponents + are `0,59,98` and the retained exponents are `117,116,95,54`; +- at `29q/10`, the deficit-6 exponent is `-12`, and every subsequent high-tail + ratio is at most `x^(-72)`; +- at `29q/10`, after the same low-weight normalization, the low exponents are + `0,68,116` and the retained exponents are `144,152,140,108`; +- at `83q/20`, the high exponents begin `138,91,24,-63`, and after deficit 9 + every successive ratio is at most `x^(-107)`. + +Now split according to the position of the target tilt. + +If `lambda_4<=lambda_s`, monotonicity and (3.1) give + +\[ + L(\lambda_4)+H(\lambda_4) + <\frac{263}{1000}+\frac3{200} + =\frac{139}{500}. + \tag{3.3} +\] + +If `lambda_4>=lambda_s`, equations (3.2) give + +\[ + L(\lambda_4)+H(\lambda_4) + <\frac{33}{250}+\frac{29}{200} + =\frac{277}{1000} + <\frac{139}{500}. + \tag{3.4} +\] + +Thus, uniformly through the full phase interval, + +\[ + \boxed{L(\lambda_4)+H(\lambda_4)<\frac{139}{500}.} + \tag{3.5} +\] + +## 4. Entropy loss + +Let `F_+` and `F_4` be the limiting constrained values from Section 3 of the +canonical manuscript. Evaluating the full-support dual function at the +four-support optimizer gives + +\[ + \begin{aligned} + D_4(\delta) + &=F_+(T_0)-F_4(T_0)\\ + &\le\ln\{1+L(\lambda_4)+H(\lambda_4)\}. + \end{aligned} + \tag{4.1} +\] + +Equation (3.5) therefore proves + +\[ + \boxed{ + D_4(\delta)<\ln\frac{639}{500}, + \qquad + q-D_4(\delta)>\ln\frac{1000}{639}.} + \tag{4.2} +\] + +This strengthens both the canonical certificate + +\[ + q-D_4(\delta)>\ln\frac{200}{153} +\] + +and the preliminary `ln(50/33)` certificate recorded in the broader research +notebook PR. + +## 5. Consequences for displayed constants + +Using only the canonical manuscript's present final safety factor, replacing +`gamma_4` by (4.2) would give + +\[ + \frac{q^2}{32}\ln\frac{1000}{639} + =0.006724102452095\ldots. + \tag{5.1} +\] + +If the independent root-gap propagation in PR #31 is accepted, the combined +coefficient becomes + +\[ + \boxed{ + \frac{q^2}{8}\ln\frac{1000}{639} + =0.026896409808379\ldots.} + \tag{5.2} +\] + +These are consequences of separate review layers. This note itself proves only +the limiting entropy certificate (4.2), conditional on the variational +comparison already used in Lemma 5.1. + +## 6. Numerical diagnostic + +A 2001-point phase scan of the limiting variational problem, using unrestricted +support cutoffs 59 and 89, gives identical displayed values for the two +truncations and reports + +\[ + \min_\delta\{q-D_4(\delta)\} + \approx0.520701335491228 +\] + +at `delta=1` on the grid. This numerical value is not part of the certificate. + +## 7. Scope boundary + +The exact checker verifies every displayed rational enclosure and weight +comparison. It does not independently prove the finite-to-limiting convergence +in Section 3, the signed root displacement, the second moment, amplification, +or `Erdos625Statement`. \ No newline at end of file