Wikström’s Moment duality and an improved lower bound for Korenblum’s constant (arXiv:2607.17748, AI-assisted per the claim database) proves c₂ ≥ 0.4263 — up from 0.3554 — via a moment-duality criterion and an explicit eight-atom rational measure, and ships a rigorous Arb ball-arithmetic certificate. We re-derived the entire numerical-inequality side independently of Arb, in our own outward-rounded intervals plus exact BigInt rationals. It holds: 17/17 checks, 4/4 mutation controls rejected, 4.2 s.
node verify.js · exit 0 · 4.2 s · independent of ArbThe obstacle is that the criterion looks transcendental. It is not: Kc(√t)² is a rational function of t (the square root enters only squared), so the whole B-family reduces to rational arithmetic with self-derived truncation-tail bounds — ours match the paper’s own equations (14)–(15) at ~1e−20. Because 1 − K² ≈ 5e−10, the K² → 1/G chain is catastrophically cancellation-prone in floating point, so it runs in a fixed-point BigInt interval layer (10−32 quantum, exact integer square root). Monotonicity of K² on [R, 0.99999] — where the paper computes a derivative — is instead proven by adaptive bisection of an algebraically paired form of d/dt log K², 10,368 leaves. The A-family, the mass identity Σwj = R, t₁ = c², t₈ = R, and both tail inductions are exact BigInt rationals, not intervals at all.
Three of the four controls die on the exact gates, which is easy. The fourth is the interesting one: a mass-preserving transfer of 3e−3 between atoms 7 and 8 passes every exact check — the measure still has the right total mass, support and positivity — and is killed only by the B-family interval numerics at k = 1. A control that survives the cheap gates and dies on the expensive one is the evidence that the expensive one is doing work.
The duality argument itself — Lemma 3.1 and Wang’s Proposition 2.1, which turn these inequalities into a statement about c₂, are mathematics we did not audit; our verdict is explicitly modulo them. Also unchecked: Wang 2025’s annular estimate and the Kc/Gc formula, the behaviour of Kc on the discarded sliver (0.99999, 1), the previous-bound (0.3554) literature claim, and anything specific to Arb’s implementation. What we assert is narrow and complete: the finite system of inequalities the paper relies on is true, in an arithmetic that shares no code with the one that first checked it.
The two earlier pilots re-checked identities that had only author-side verification. This one re-checks a claim that already ships a rigorous, public, third-party-grade certificate — the hardest target in the lane, and the case where independent agreement carries the most information. Two implementations, two arithmetics, no shared code, same answer to seven digits.