Papers With

← All papers
First page of Halving the original Kalton--Roberts upper bound for nearly additive set functions

Halving the original Kalton--Roberts upper bound for nearly additive set functions

Boon Suan Ho, Tomasz Kania

math.CO Jun 5, 2026 · v1
formalization mathlib combinatorics analysis
Read PDF arXiv abstract Code
TL;DR
The improved Kalton-Roberts upper bound, including exact rational interval-arithmetic certificates, is formalised in about 6,200 lines of Lean and Mathlib.
Abstract
Let $K_\mathrm{KR}$ denote the optimal Kalton--Roberts constant for approximately additive real-valued set functions on algebras of sets. Kalton and Roberts proved $K_\mathrm{KR}\le89/2$, and Bondarenko, Prymak, and Radchenko improved the upper bound to $38.8$. We prove that $$K_\mathrm{KR}\le\frac{694,198,146,664,396,294,486,127,753}{34,994,834,677,886,019,996,000,000}\,\approx 19.837.$$ Thus the original Kalton--Roberts upper bound is more than halved. The proof changes the source collections fed into the expander-recombination step however still uses expander graphs as the other proofs do. The four expander families used in the final recombination are certified by exact rational interval arithmetic, and the proof has been formalised in Lean.
Problem

The optimal Kalton-Roberts constant K_KR for approximating nearly additive set functions by finitely additive measures had an upper bound of 89/2 (original) and 38.8 (improved), but the gap to the lower bound of 3 remained large.

Approach

The proof modifies the source collections fed into the expander-recombination step of the Kalton-Roberts argument. Instead of minimising an oscillation and building a submeasure, it uses an l-infinity duality certificate for best approximation by additive measures, which supplies low-frequency near-extremal multisets. Rational mixtures of neighbouring intersection levels further reduce the frequencies. Four expander families are certified by exact rational interval arithmetic. The entire proof is formalized in Lean 4 (v4.28.0, ~6.2k lines across 18 files).

Results

The new bound is K_KR <= 694198146664396294486127753 / 34994834677886019996000000, approximately 19.837, more than halving the original Kalton-Roberts upper bound of 89/2. All numerical comparisons are exact rational arithmetic, and the Lean formalization covers the complete argument including the set-algebra statement.