The Kalton–Roberts constant K_KR is the least constant such that every approximately additive set function is uniformly close to a finitely additive signed measure. The best published upper bound was 38.8.

A Hahn–Banach dual certificate for best ℓ∞-approximation yields two families of near-extremal sets with complementary point frequencies. Rational mixtures of neighbouring intersection levels lower these frequencies, and Pippenger-style random biregular expanders drive two recombination schemes, used on different case ranges. The argument is formalized in Lean 4 with Mathlib, where K_KR is defined as an infimum and the exact rational estimate is proved; a Python script performs independent arithmetic checks.

The proof gives K_KR ≤ 694198146664396294486127753/34994834677886019996000000 ≈ 19.837, hence K_KR < 19.838, more than halving the original bound of 89/2. The abstract states a sharper bound of 374167/20000 = 18.70835, which differs from the constant derived in the body and formalized in Lean.