The optimization-constants registry: five asterisked bounds replayed
Five asterisks, replayed
The optimization-constants registry marks a bound with an asterisk when its verification is "at minimal levels". Five of its bounds rest on arithmetic small enough to decide exactly. Three hold as printed — two entropy laws and one Boolean function on 18 variables. For Turán's power sums the limiting certificate holds and the passage to it is the author's argument. The sum–product row quotes a constant its own source calls only "suggested", and the source's calculation cannot reach it; what that source proves holds. One of the checkers published with the entropy laws would also have accepted a false bound.
Decided: that the law each cited certificate writes down gives the ratio the registry prints — a lower bound on the constant, never its value. Not decided: the upper bounds, the constants themselves, and the registry's other asterisked rows. The asterisk is the maintainers' to keep or remove; this page is evidence. The 147-point checker's 53-bit comparison was reported to its author on 2026-10-05 (a comment on gist CoolRmal/5368357c); the replay was proposed to the registry as teorth/optimizationproblems PR #216 the same day.
tl;dr
The finding.Three hold as printed, one partly, one is repaired. C71 > 6.521845710923046575 is CERTIFIED from its truth table, given the amplification rule, cited (§3); C84b ≤ 1.999281 holds only as 1.9993, what its source proves (§4); C42 ≤ 0.6906538 rests on a limiting inequality that holds, |Y|/D ≤ 0.6906536951…, and on an asymptotic argument in prose (§5). And C3b ≥ 1.77898884 and C3c ≥ 1.6747338950414058 are CERTIFIED from the certificates the registry cites: the ratios are 1.7789888414206935498051… and 1.6747338950414058700631…, each enclosed to 40 digits. The 147-point certificate's own 60-digit bound holds, so does the 95-point bound it superseded, and the improvement the registry prints, 2.06 × 10−11, is the rounding of the certified gap. And the checker published with the 147-point certificate prints OK for C3c >= 1.6747338950414059, which is false: it encloses the ratio at 100 digits, then compares in doubles.
The mechanism. A law on Z² with rational weights gives C ≥ H(X−Y) / max of the entropies of the other forms. The pushforwards are exact; each entropy term is an interval whose logarithm is rounded outward. Two implementations share no code with each other or with the claimants: instruments/sumdiff (JavaScript, BigInt and dyadic intervals at 128–1024 bits) and tools/verify_sumdiff.py (the Python standard library, decimal at 120 digits).
Check it.python3 tools/verify_sumdiff.py — standard library only, four CERTIFIED and one red control. node instruments/sumdiff/battery.js — 22 checks, 7 red controls.
afterwards · 2026-10-18
The registry's maintainer merged the replay on this page (PR #216, commit ad40c534): the asterisks on C₃b, C₃c and C₇₁ are gone, and each of the three pages cites this replay as [T2026], under the rule he had stated on #176 that an independent replay removes the mark. The registry's bytes after the merge are pinned in corpus/optconst-queue/registry-2026-10-18/.
asterisked bounds decided
5
C3b, C3c and C71 CERTIFIED; C42 PARTIAL; C84b REPAIRED. The registry's table is pinned at commit 2c1968cd.
digits of each ratio
40
Enclosed, not estimated; the 60-digit bound the 147-point certificate prints is decided at 256 bits.
implementations
2
JavaScript over BigInt and dyadic intervals; Python over the standard library. They agree to every digit shown.
false bounds the checker accepts
2
Observed, run on the pinned script: its last comparison is at 53 bits. Both are refuted here.
how to read the marks
Every number on this page is decided by exact arithmetic unless it is marked. Underlined dashed: nothing here decided it — what a claimant's checker printed is its claim, and so is a proof read rather than computed. A verdict that holds given a published theorem names it in italic; C42, whose limit is decided and whose passage to it is an argument in prose, lists what it rests on and how far each step was checked (§5).
decided
exact arithmetic backs it
computed
float, or a number someone printed; nothing decided it
§1 · the claims
What the registry prints, and what the certificates give
Also decided from the same certificates: the 13-point certificate's printed "true value" 1.778988841420693549 is a truncation of the ratio (it is CERTIFIED and the next value up is REFUTED); the 95-point certificate's 39-digit bound and the 147-point certificate's 60-digit bound are CERTIFIED; the 147-point ratio exceeds the 95-point one by 2.058080 × 10^-11…, which rounds to the 2.06 × 10−11 the registry prints.
§2 · the checker
What a checker's last line proves
The 147-point certificate ships a checker (check_cert.py, pinned here by sha256 and not copied). It computes the ratio in interval arithmetic at 100 digits, which is right, and then decides the claim with mpmath.mpf(lo_str) >= mpmath.mpf(claimed) in mpmath's default context — 53 bits, a double. Every decimal within a double of the true bound compares equal to it. Run on the pinned script with claims written here:
not certified here: above the certified lower end at the 58th decimal
1.6747338950414058800
OK
REFUTED here: above the ratio at the 17th significant digit
1.67473389504140590
OK
REFUTED here
The bound the registry prints is true, and it is decided above without that checker. The point is the checker: C3c >= 1.6747338950414059 is false at the seventeenth significant digit, is the same double as the true 60-digit bound, and prints OK. A verifier's last comparison has to be as exact as its enclosure, or the enclosure proves nothing the output line says. The Mosaic Intelligence checkers set the working precision to 80 digits before comparing and do not have this weakness. And one of our own two implementations had its mirror image while this page was built: Python's unary minus on a Decimal rounds to the default context's 28 digits, which moved the first draft's ratio at the 28th digit until the two implementations were compared.
why these numbers stand as they do
computed — what the claimant's checker printed: its claim, compared in doubles; not a decision
§3 · the third asterisk
C71: a Boolean function on 18 variables
The Fourier entropy–influence constant is the least C with H[f] ≤ C·I[f] for every Boolean f, where H is the entropy of the Fourier weights (base 2) and I the total influence. For a balanced g, given the amplification rule of O'Donnell–Tan (2013) and Hod (2017, Prop. 1.2), cited and not re-proved here, C71 ≥ H[g]/(I[g] − 1). The registry's asterisked C71 > 6.521845710923046575 cites a truth table on 18 variables published by Numaro (numaro.tech, "AI Autoresearch"), Zenodo 10.5281/zenodo.21497769.
Decided. The table read from its hex and bound by its published sha256; the integer Walsh–Hadamard transform of all 262,144 entries; balance, Parseval, I = 261/128 exactly; H from 10 distinct weight sizes over 2,770 nonzero coefficients, each logarithm in an outward-rounded Decimal interval. The ratio is 6.5218457109230465756581439729…, above the registry's number, and above the record it replaced. The function is also logic-monotone, as claimed.
Not decided. The amplification rule itself, which is a published theorem; the claimant's checker (mpmath intervals), pinned and not run.
§4 · the fourth asterisk
C84b: a suggested constant, quoted as a bound
The registry's asterisked row for the real sum–product exponent reads C84b ≤ 1.999281: "a ChatGPT 5.5 long-thinking optimization of the explicit constant of [BSSZ2026, §5] giving c ≥ 0.000719. Unverified." The note it cites states its theorem with 0.0007 and adds: "The optimized value suggested by the same calculation is about 0.000719, but 0.0007 is the safer quoted constant."
What the note proves holds. Its chain, decided in intervals: the regulator estimate at s = 1.371966384 is 101.95607583… ≤ 103; at Y = 1415 and X = ⌊e¹⁴²³⌋ the product factor 515/Y < 0.364, the additive factor 0.1352394770… < 0.136, log|A|/d < 1432, and −log 0.364 > 0.0007 · 1432. So C84b ≤ 1.9993, given BSSZ2026 §5, the note's lattice-doubling lemma and the regulator bound.
What the registry quotes is out of its reach. For every s > 1 and every X and Y the same chain gives c ≤ 0.0007150508: the regulator estimate is at least 101.9 for every s (a sweep of s with ζ by Euler–Maclaurin and Γ by Stirling, each with its remainder), the additive factor forces log X > Y + log M₁ − 2 log Y, and the product factor caps the gain at log(Y/5R). 0.000719 is not reached; at the note's own choice the chain gives 0.0007062455…
Verdict: REPAIRED. The row holds as C84b ≤ 1.9993, which is what its source proves.
§5 · the fifth asterisk
C42: a limiting inequality, and the argument that reaches it
Turán's pure power-sum constant is the limsup of R_n, the least possible max over k ≤ n of |Σ z_iᵏ| when max |z_i| = 1. The registry's asterisked C42 ≤ 0.6906538 cites S. Griego's certificate: power sums set to s = 1 − α on the first τn indices, to η in the middle, and to values on the last block that force b_n = 0, so the numbers built from them have every power sum at most C in modulus — for all large n, by an asymptotic argument that reduces everything to four exact facts.
Decided. The four facts, in Decimal intervals: |1 − α| < C and |η| < C exactly, τ > 1/3, and the limiting inequality |Y| < C·D, with K, A₁, A₂ and D as convergent series in a complex exponent, each summed with its tail bound (the note's, checked). |Y|/D ≤ 0.690653695151…, below 0.6906538; every enclosure the certificate prints meets the one computed here. Written apart from the claimant's verifier, which is pinned and not run.
Not decided. The passage from the limit to every large n — the uniform asymptotics of the binomial coefficients, the boundary terms, the double sum — which the note argues in prose and for which it gives no finite threshold. Verdict: PARTIAL.
And the pull request after it. An open pull request to the registry (#184, A. Röhrig with Codex) replaces the single middle value by eight and claims C42 ≤ 0.688983. The same decider, written for step profiles and checked to reproduce Griego's number with one block, decides its limiting inequality: |Y|/D ≤ 0.688982098504… < 0.688983, every block inside C. PARTIAL for the same reason: the limit is decided, the passage to it is prose.
What both rows rest on, in the order the bound travels through it:
assumed
The passage from the limit to every large nthe note's argument in prose — the uniform asymptotics of the binomial coefficients, the boundary terms, the double sum — with no finite threshold; read here, not decided (certs/turan-ledger.json: “the asymptotic reduction … is the note's prose”)
Each limiting inequality is decided exactly; the weakest premise is assumed, the argument that carries it to every large n. Hence PARTIAL, for Griego's 0.6906538 and for #184's 0.688983 alike.
§6 · how
How it is decided
The formulation. The registry states both constants in their entropy form (Green–Ruzsa 2019): C3b is the least C with H(X−Y) ≤ C·max(H(X), H(Y), H(X+Y)); C3c adds H(X+2Y) to the maximum. One law gives a lower bound.
The door. Weights must be positive integers over the common denominator and sum to it exactly; a point may not repeat. The 320-digit numerators are read as integers — a reader that parses them as doubles is refused, a red control.
The arithmetic. Pushforwards exact; each −p ln p an interval; the maximum taken end by end; the ratio by interval division; precision doubled from 128 bits while a verdict straddles. An exact equality is refused at every precision, never certified.
The pins. The registry at commit 2c1968cd (Apache-2.0), the Zenodo archive (CC BY 4.0) with its own manifest checked, the gist at revision 62621d2d. corpus/optimization-constants/meta.json holds every sha256.
outside
What has come back from outside
Re-run independently, 2026-10-23. maximusrufus (GitHub): Twelve register rows re-decided with their own exact code, at cert-machine aa52e8d (Linux): the kissing configurations of AlphaEvolve (593) and EinsteinArena (594, 604); the sum–difference certificates of 3b (13 points) and 3c (147 and 95 points), agreeing to 30 digits; and six EinsteinArena constructions — two circles-in-a-rectangle (with the 44 overlapping pairs of the as-published Together AI packing), two Heilbronn convex, two min-distance ratios. A duplicated vector and moved probability weight are rejected by their check as by ours. Outcome: the same verdict on all twelve rows, no disagreement; two findings, both answered on the thread. (their code)
Re-run independently, 2026-10-23. maximusrufus (GitHub): The three ledgers re-derived with the tools that write them, at cert-machine aa52e8d (Linux, Python 3.14.4, Node v22.11.0); verify_sumdiff.py run beside the sum–difference ledger, its false-bound control firing. Outcome: every verdict and count identical. (their code)
Re-run independently, 2026-10-24. JeetuSK0808 (GitHub): The registry’s C₈₄b correction (reports/optimization-constants.html §4) re-derived in their own interval arithmetic (mpmath), the note’s lemmas and inputs taken as given: c ≈ 0.000706 at the note’s choice; at most about 0.000707 over Y and X with R_K ≤ 103^d, and 0.00071385 with the regulator at its limit — so 0.000719 is not reached and 1.9993 is the entry. Outcome: the same verdict; their 0.00071385 is the maximum, our 0.0007150508 a ceiling above it (answered on the thread, where we printed 0.0007150507: the ceiling truncated, rounded outward since 2026-10-24). (their code · the report)
Re-run independently, 2026-10-24. maximusrufus (GitHub): The registry’s C₄₂ record (certs/turan-ledger.json) re-derived with the tool that writes it, at cert-machine 8924797: both rows identical. The rerun’s reading of instruments/turan/c42.py found three defects, none moving a verdict: failed checks answered REFUTED where the rule asks REFUSED, printed upper ends truncated rather than rounded outward, and the two routes compared on truncated strings. Outcome: the same verdicts (PARTIAL); the three defects fixed, recorded in the self-audit’s amendment of 2026-10-24. (their code)
Cited by a registry, 2026-10-18. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): Three asterisks removed on our replays — C₃b, C₃c and C₇₁ — merged by T. Tao (pull request #216); the constants' pages cite the replays as [T2026]. In their words: “with no code shared with the claimants, by C. Toledo” (the source, pinned)
Cited by a registry, 2026-10-26. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): C₈₄b corrected on our check: the row now records the note's theorem, 1.9993*, instead of its "suggested" 0.000719; merged by T. Tao (pull request #257), and the page cites the check as [T2026]. In their words: “[T2026] Toledo, Carlos. Interval-arithmetic check of the [Al26] chain” (the source, pinned)
Each credit is quoted from a snapshot pinned by sha256 (corpus/recognition.json); each re-run is a row of corpus/external-reruns.json. Neither is a peer review.