cert-machine · one of six · re-verified from the manuscript
The Korenblum constant
c₂ ≥ 0.4263, via a moment-duality criterion and an explicit rational eight-atom measure (arXiv:2607.17748). The Korenblum constant c₂ had a best published lower bound of 0.3554.
tl;dr
The finding.CONFIRMED — the numerical criterion. What a machine can decide about this claim, it decided, and it held. What it cannot decide is stated below rather than left to the reader to notice.
The mechanism. Written against the manuscript. The author's code was never executed. Verification that existed at source: An Arb interval certificate shipped with the paper, plus a Zenodo archive.
Check it.node legacy/research/challenges/lane/laneb-korenblum/verify.js — 5.4 s at this build, 15 named checks and 4 mutation controls, every control rejected.
verdict
CONFIRMED
the numerical criterion
named checks
15
each one printed by the verifier at this build and listed on this page
the verifier's own total
—
this verifier prints no total of its own
mutation controls
4
deliberate corruptions of the claim — every one rejected, or this page would not build
runtime
5.4 s
plain Node, no packages, no author code
analytic core
not audited
true of all six claims in this set, and the reason the flagship exists
§1 · at source
What was claimed, by whom, and what checking already existed
field
as recorded at source
the claim
c₂ ≥ 0.4263, via a moment-duality criterion and an explicit rational eight-atom measure (arXiv:2607.17748).
the problem
The Korenblum constant c₂ had a best published lower bound of 0.3554.
credited AI system
OpenAI Codex (GPT-5.6 Sol), disclosed in the paper; author proof by Frank Wikström
verification at source
An Arb interval certificate shipped with the paper, plus a Zenodo archive.
our verdict
CONFIRMEDthe numerical criterion
§2 · what we certified
The ledger, as the verifier printed it at this build
Every inequality of the paper’s moment-duality criterion for its explicit measure, under our own outward-rounded interval arithmetic — no Arb, no python-flint, and no code from the Zenodo archive executed. The A-family over k = 1..2183, the B-family over k = 1..1299, both tails by exact induction.
The verifier organises its own run into 7 stages. This is that structure, counted at build time — not a summary written by hand.
[0] Exact rational structure (BigInt)
1
measure structure: sum w = R, t1 = c^2, t8 = R, support in [c^2,1), mass 1, weights > 0
[6] B-family tail, k >= 1300 (base case + exact ratio induction)
1
base case k=1300: integral >= 4.798906373e-9 > 1.611068196e-9 >= sum w_j t_j^1300 (paper: 1.6668e-9 > 1.6111e-9)
2
induction ratio: a = 0.9980001 > 0.99 = max_j t_j exactly => B_k > 0 for all k >= 1300
§3 · the falsifiers
Proof that this verifier can fail
A verifier that cannot reject a false claim is not evidence, it is decoration. So each one carries mutation controls: the claim is deliberately corrupted and the verifier must refuse it. All 4 were rejected in the run that built this page, and a control that stopped firing would refuse the page instead.
the corruption, and how it was caught
1
M1 (w_3 += 1e-3) rejected by exact layer: sum w_j = 991/1000 != R
2
M2 (w *= 0.999) rejected: mass check fails AND A_k certified NEGATIVE at k=2 (A_hi=-3.213e-4)
3
M3 (claim c = 0.43) rejected by exact layer: t_1 != c^2
4
M4 (move 3e-3 mass from atom 7 to atom 8) passes exact layer but B-certification fails at k=1 (B_lo=-2.496e-6) — rejected
§4 · the boundary
What this audit did NOT reach
not audited
The duality argument itself — the paper’s Lemma 3.1 and Wang’s Proposition 2.1. The bound follows from what we certified only if that argument holds.
This is the part worth reading twice. The verdict at the top of this page is true inside its scope line and false outside it, and the sentence above is where the scope line comes from. Across all six claims in this set the same split appears: the computational fragment certifies and the analytic core does not — the flagship page measures exactly that.
§5 · re-run it
One command, no dependencies
git clone https://github.com/carlostoledo1891/cert-machine
cd cert-machine
node legacy/research/challenges/lane/laneb-korenblum/verify.js
Plain Node, no packages. It prints the ledger above, runs its own falsifiers, and exits non-zero if anything fails. node instruments/laneaudit/audit.js runs all six.