cert-machine · the registry's asterisks

Two asterisks, replayed

The optimization-constants registry marks a bound with an asterisk when its verification is "at minimal levels". Two of its lower bounds rest on entropy certificates small enough to decide exactly, and both hold. One of the two checkers published with them 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, and nothing has been sent to them.

tl;dr

The finding. Both hold. 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⁻¹¹, 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.

asterisked bounds decided

Both CERTIFIED. The registry's table is pinned at commit 2c1968cd.

digits of each ratio

Enclosed, not estimated; the 60-digit bound the 147-point certificate prints is decided at 256 bits.

implementations

JavaScript over BigInt and dyadic intervals; Python over the standard library. They agree to every digit shown.

false bounds the checker accepts

Observed, run on the pinned script: its last comparison is at 53 bits. Both are refuted here.

§1 · the claims

What the registry prints, and what the certificates give

claim	by	certificate	verdict	the ratio, enclosed
C3b >= 1.77898884 *	Mosaic Intelligence (2026)	13 points, denominator of 37 digits 2efe99360a1f…	CERTIFIED	1.7789888414206935498051938874772894343542 1.7789888414206935498051938874772894344895
C3c >= 1.6747338950414058 *	Y. Lin (2026)	147 points, denominator of 321 digits b3dc9587ba7a…	CERTIFIED	1.6747338950414058700631357567222139986329 1.6747338950414058700631357567222139998144
C3c >= 1.6747338950208249 (superseded)	Mosaic Intelligence (2026)	95 points, denominator of 201 digits 2ebd7ba7a32e…	CERTIFIED	1.6747338950208249933782075776022651846547 1.6747338950208249933782075776022651853483

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⁻¹¹ 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(verified) >= 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:

claimed	the checker printed	decided here
1.674733895041405870063135756722213999136383713818148696811828	OK	CERTIFIED here (the certificate's own bound)
1.674733895041405870063135756722213999136383713818148696811900	OK	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.

§3 · 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.