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

Boon Suan Ho; Tomasz Kania

arxiv: 2606.06807 · v1 · pith:S3GMHXULnew · submitted 2026-06-05 · 🧮 math.CO

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

Boon Suan Ho , Tomasz Kania This is my paper

Pith reviewed 2026-06-27 22:09 UTC · model grok-4.3

classification 🧮 math.CO

keywords Kalton-Roberts constantnearly additive set functionsexpander graphsrecombination methodupper boundinterval arithmeticLean formalization

0 comments

The pith

The Kalton-Roberts constant K_KR for nearly additive set functions is at most approximately 19.837.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves a new upper bound on the Kalton-Roberts constant K_KR, which measures how far a real-valued set function on an algebra can deviate from additivity while remaining controlled by its variation. Earlier results gave K_KR ≤ 89/2 = 44.5 and then ≤ 38.8; the new bound is the explicit rational 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837. The improvement comes from feeding different source collections into an expander-recombination procedure whose four final expander families are certified by exact rational interval arithmetic, with the entire argument formalised in Lean.

Core claim

Let K_KR denote the optimal Kalton--Roberts constant for approximately additive real-valued set functions on algebras of sets. We prove that K_KR ≤ 694198146664396294486127753 / 34994834677886019996000000 ≈ 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.

What carries the argument

Expander-recombination step driven by four specific expander families whose parameters are certified by exact rational interval arithmetic.

If this is right

The deviation of any nearly additive set function from true additivity is controlled by a constant less than 20 times its variation.
The original Kalton-Roberts bound of 44.5 is replaced by a value less than half that size.
Machine-verified certificates for expander families can be reused or improved in subsequent calculations of the same constant.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same certified-recombination technique might tighten other constants that arise from additive approximation problems on set algebras.
Explicit lower-bound constructions for K_KR would now be more informative, since the gap between 19.837 and the true optimum is smaller than before.
If smaller expander families with the required spectral properties can be found, the same proof skeleton would immediately yield a still tighter rational upper bound.

Load-bearing premise

The four specific expander families chosen for the final recombination step are correctly certified by the exact rational interval arithmetic computations described in the proof.

What would settle it

A concrete nearly additive set function whose deviation from additivity exceeds 19.837 times its total variation, or an arithmetic error found in the rational interval certification of any of the four expander families.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This cuts the Kalton-Roberts constant to roughly 19.837 via a Lean proof on modified recombination, with the main gap being external certification of the four expanders.

read the letter

The headline result is a new explicit upper bound K_KR ≤ 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837. That is more than half the prior 38.8 bound from Bondarenko-Prymak-Radchenko. The authors reach it by feeding different source collections into the expander-recombination construction while keeping the expander graphs themselves. The combinatorial steps are formalized in Lean, and the bound is given as an exact rational.

The formalization is the clearest strength. It removes the usual worry about arithmetic slips in the final calculation. The improvement is concrete and the paper states the numerical value outright rather than hiding it behind big-O notation.

The remaining uncertainty sits with the four chosen expander families. Their expansion and spectral properties are certified by separate exact rational interval arithmetic rather than being included in the Lean script. An error in any of those four checks would break the claimed bound, even though the recombination logic itself is verified. The paper presents those families as verified inputs, so the formalization is conditional on them.

This is a narrow, technical improvement inside combinatorial functional analysis. Specialists who care about the precise value of K_KR or who use expander-recombination arguments will want to see the details. It is solid enough on its own terms to merit referee time; the Lean artifact and the explicit rational make the central claim checkable.

Referee Report

1 major / 0 minor

Summary. The paper proves that the optimal Kalton-Roberts constant K_KR for approximately additive real-valued set functions satisfies K_KR ≤ 694198146664396294486127753 / 34994834677886019996000000 ≈ 19.837. This halves the original Kalton-Roberts upper bound of 89/2 and improves on the previous best bound of 38.8. The argument modifies the source collections in an expander-recombination construction, certifies the required properties of four specific expander families by exact rational interval arithmetic, and includes a Lean formalization of the combinatorial steps.

Significance. If the result holds, the improvement is substantial and directly addresses a long-standing quantitative question in functional analysis and combinatorics. Credit is due for the machine-checked Lean formalization of the core argument and for the parameter-free explicit rational bound obtained via certified interval arithmetic; these features strengthen verifiability beyond typical analytic proofs in the area.

major comments (1)

[Abstract and recombination construction] Abstract and § on the recombination construction: the final numerical bound is produced by feeding four externally certified expander families into the recombination step. The Lean formalization assumes the expansion and spectral properties of these families; an undetected error in any of the four interval-arithmetic certifications would invalidate the claimed constant. The manuscript should indicate whether the exact rational interval-arithmetic scripts or their outputs are deposited for independent checking.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive report and the recommendation to accept. We respond to the major comment below.

read point-by-point responses

Referee: [Abstract and recombination construction] Abstract and § on the recombination construction: the final numerical bound is produced by feeding four externally certified expander families into the recombination step. The Lean formalization assumes the expansion and spectral properties of these families; an undetected error in any of the four interval-arithmetic certifications would invalidate the claimed constant. The manuscript should indicate whether the exact rational interval-arithmetic scripts or their outputs are deposited for independent checking.

Authors: We agree that explicitly indicating the availability of the certification materials would improve verifiability. In the revised manuscript we will add a sentence in the abstract and in the section on the recombination construction stating that the exact rational interval-arithmetic scripts together with their outputs are deposited both in the supplementary files on the arXiv and in the public repository accompanying the Lean formalization. revision: yes

Circularity Check

0 steps flagged

No circularity: formal Lean proof against external expander data

full rationale

The derivation improves the Kalton-Roberts constant via an expander-recombination construction whose combinatorial steps are formalized in Lean. The four expander families enter as externally certified inputs (via exact rational interval arithmetic) rather than being derived from the target bound or fitted to it. No equations reduce by construction to their own inputs, no parameters are fitted then relabeled as predictions, and no load-bearing self-citations or imported uniqueness theorems appear. The result is therefore independent of the claimed numerical bound.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proof relies on standard mathematical axioms for real numbers and graph theory together with the external correctness of four expander families; no free parameters are fitted inside the derivation and no new entities are postulated.

axioms (1)

standard math Standard axioms of real arithmetic and graph theory as encoded in Lean
Invoked throughout the formalization to certify the interval-arithmetic bounds on the expander families.

pith-pipeline@v0.9.1-grok · 5688 in / 1202 out tokens · 17672 ms · 2026-06-27T22:09:11.061982+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

14 extracted references · 11 canonical work pages

[1]

B. S. Ho,KaltonRoberts: Lean formalisation of the Kalton–Roberts upper bound, GitHub repository, 2026. Leanv4.28.0, mathlibv4.28.0.https://github.com/boonsuan/KaltonRoberts

2026
[2]

Alon,Eigenvalues and expanders, Combinatorica6(1986), no

N. Alon,Eigenvalues and expanders, Combinatorica6(1986), no. 2, 83–96.https://doi.org/10.1007/ BF02579166

1986
[3]

Alon and J

N. Alon and J. H. Spencer,The Probabilistic Method, 4th ed., Wiley Series in Discrete Mathematics and Optimization, Wiley, Hoboken, 2016.https://doi.org/10.1002/9781119061953

work page doi:10.1002/9781119061953 2016
[4]

A. V. Bondarenko, A. Prymak and D. Radchenko,On concentrators and related approximation constants, J. Math. Anal. Appl.402(2013), no. 1, 234–241.https://doi.org/10.1016/j.jmaa.2013.01.019

work page doi:10.1016/j.jmaa.2013.01.019 2013
[5]

Capalbo, O

M. Capalbo, O. Reingold, S. Vadhan and A. Wigderson,Randomness conductors and constant-degree lossless expanders, STOC’02: Proceedings of the Thirty-Fourth Annual ACM Symposium on Theory of Computing, 659–668.https://doi.org/10.1145/509907.510003

work page doi:10.1145/509907.510003
[6]

Feige, M

U. Feige, M. Feldman and I. Talgam-Cohen,Approximate modularity revisited, SIAM J. Comput.49 (2020), no. 1, 67–97.https://doi.org/10.1137/18M1173873

work page doi:10.1137/18m1173873 2020
[7]

Gnacik, M

M. Gnacik, M. Guzik and T. Kania,Approximate modularity: Kalton’s constant is not smaller than 3, Proc. Amer. Math. Soc.149(2021), no. 2, 661–669.https://doi.org/10.1090/proc/15195

work page doi:10.1090/proc/15195 2021
[8]

Guruswami, C

V. Guruswami, C. Umans and S. Vadhan,Unbalanced expanders and randomness extractors from Parvaresh– Vardy codes, J. ACM56(2009), no. 4, Article 20.https://doi.org/10.1145/1538902.1538904

work page doi:10.1145/1538902.1538904 2009
[9]

Hoory, N

S. Hoory, N. Linial and A. Wigderson,Expander graphs and their applications, Bull. Amer. Math. Soc. (N.S.)43(2006), no. 4, 439–561.https://doi.org/10.1090/bull/1879

work page doi:10.1090/bull/1879 2006
[10]

N. J. Kalton and J. W. Roberts,Uniformly exhaustive submeasures and nearly additive set functions, Trans. Amer. Math. Soc.278(1983), no. 2, 803–816.https://doi.org/10.1090/S0002-9947-1983-0701524-4

work page doi:10.1090/s0002-9947-1983-0701524-4 1983
[11]

Lubotzky, R

A. Lubotzky, R. Phillips and P. Sarnak,Ramanujan graphs, Combinatorica8(1988), no. 3, 261–277. https://doi.org/10.1007/BF02126799

work page doi:10.1007/bf02126799 1988
[12]

Morgenstern,Existence and explicit constructions ofq + 1regular Ramanujan graphs for every prime powerq, J

M. Morgenstern,Existence and explicit constructions ofq + 1regular Ramanujan graphs for every prime powerq, J. Combin. Theory Ser. B62(1994), no. 1, 44–62.https://doi.org/10.1006/jctb.1994.1054 14 B. S. HO AND T. KANIA

work page doi:10.1006/jctb.1994.1054 1994
[13]

Pawlik,Approximately additive set functions, Colloq

B. Pawlik,Approximately additive set functions, Colloq. Math.54(1987), no. 1, 163–164.https://doi. org/10.4064/cm-54-1-163-164

work page doi:10.4064/cm-54-1-163-164 1987
[14]

Pippenger,Superconcentrators, SIAM J

N. Pippenger,Superconcentrators, SIAM J. Comput.6(1977), no. 2, 298–304.https://doi.org/10.1137/ 0206022 (B. S. Ho)Department of Mathematics, National University of Singapore, Singapore Email address:hbs@u.nus.edu (T. Kania)Mathematical Institute, Czech Academy of Sciences, Žitná 25, 115 67 Praha 1, Czech Republic and Institute of Mathematics and Computer...

1977

[1] [1]

B. S. Ho,KaltonRoberts: Lean formalisation of the Kalton–Roberts upper bound, GitHub repository, 2026. Leanv4.28.0, mathlibv4.28.0.https://github.com/boonsuan/KaltonRoberts

2026

[2] [2]

Alon,Eigenvalues and expanders, Combinatorica6(1986), no

N. Alon,Eigenvalues and expanders, Combinatorica6(1986), no. 2, 83–96.https://doi.org/10.1007/ BF02579166

1986

[3] [3]

Alon and J

N. Alon and J. H. Spencer,The Probabilistic Method, 4th ed., Wiley Series in Discrete Mathematics and Optimization, Wiley, Hoboken, 2016.https://doi.org/10.1002/9781119061953

work page doi:10.1002/9781119061953 2016

[4] [4]

A. V. Bondarenko, A. Prymak and D. Radchenko,On concentrators and related approximation constants, J. Math. Anal. Appl.402(2013), no. 1, 234–241.https://doi.org/10.1016/j.jmaa.2013.01.019

work page doi:10.1016/j.jmaa.2013.01.019 2013

[5] [5]

Capalbo, O

M. Capalbo, O. Reingold, S. Vadhan and A. Wigderson,Randomness conductors and constant-degree lossless expanders, STOC’02: Proceedings of the Thirty-Fourth Annual ACM Symposium on Theory of Computing, 659–668.https://doi.org/10.1145/509907.510003

work page doi:10.1145/509907.510003

[6] [6]

Feige, M

U. Feige, M. Feldman and I. Talgam-Cohen,Approximate modularity revisited, SIAM J. Comput.49 (2020), no. 1, 67–97.https://doi.org/10.1137/18M1173873

work page doi:10.1137/18m1173873 2020

[7] [7]

Gnacik, M

M. Gnacik, M. Guzik and T. Kania,Approximate modularity: Kalton’s constant is not smaller than 3, Proc. Amer. Math. Soc.149(2021), no. 2, 661–669.https://doi.org/10.1090/proc/15195

work page doi:10.1090/proc/15195 2021

[8] [8]

Guruswami, C

V. Guruswami, C. Umans and S. Vadhan,Unbalanced expanders and randomness extractors from Parvaresh– Vardy codes, J. ACM56(2009), no. 4, Article 20.https://doi.org/10.1145/1538902.1538904

work page doi:10.1145/1538902.1538904 2009

[9] [9]

Hoory, N

S. Hoory, N. Linial and A. Wigderson,Expander graphs and their applications, Bull. Amer. Math. Soc. (N.S.)43(2006), no. 4, 439–561.https://doi.org/10.1090/bull/1879

work page doi:10.1090/bull/1879 2006

[10] [10]

N. J. Kalton and J. W. Roberts,Uniformly exhaustive submeasures and nearly additive set functions, Trans. Amer. Math. Soc.278(1983), no. 2, 803–816.https://doi.org/10.1090/S0002-9947-1983-0701524-4

work page doi:10.1090/s0002-9947-1983-0701524-4 1983

[11] [11]

Lubotzky, R

A. Lubotzky, R. Phillips and P. Sarnak,Ramanujan graphs, Combinatorica8(1988), no. 3, 261–277. https://doi.org/10.1007/BF02126799

work page doi:10.1007/bf02126799 1988

[12] [12]

Morgenstern,Existence and explicit constructions ofq + 1regular Ramanujan graphs for every prime powerq, J

M. Morgenstern,Existence and explicit constructions ofq + 1regular Ramanujan graphs for every prime powerq, J. Combin. Theory Ser. B62(1994), no. 1, 44–62.https://doi.org/10.1006/jctb.1994.1054 14 B. S. HO AND T. KANIA

work page doi:10.1006/jctb.1994.1054 1994

[13] [13]

Pawlik,Approximately additive set functions, Colloq

B. Pawlik,Approximately additive set functions, Colloq. Math.54(1987), no. 1, 163–164.https://doi. org/10.4064/cm-54-1-163-164

work page doi:10.4064/cm-54-1-163-164 1987

[14] [14]

Pippenger,Superconcentrators, SIAM J

N. Pippenger,Superconcentrators, SIAM J. Comput.6(1977), no. 2, 298–304.https://doi.org/10.1137/ 0206022 (B. S. Ho)Department of Mathematics, National University of Singapore, Singapore Email address:hbs@u.nus.edu (T. Kania)Mathematical Institute, Czech Academy of Sciences, Žitná 25, 115 67 Praha 1, Czech Republic and Institute of Mathematics and Computer...

1977