Five asterisks, replayed

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:

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.

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 the amplification rule of O'Donnell–Tan (2013) and Hod (2017, Prop. 1.2), cited and not re-proved here, gives 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.

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.1352394769… < 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.0007150507: 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.

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.

• 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.