Main theorem: the Kalton-Roberts upper bound

The final proof that the Kalton-Roberts constant is less than 9919 / 500.

Case 1 details

theorem KaltonRoberts.case1_bound (M D' : ℝ) (_hD' : 0 ≤ D') (A₁ : ℝ) (h1 : M ≤ A₁ - 1 / 2 * D') (h2 : M ≤ 15 + 7 / 3 * D') : M ≤ (7 / 3 * A₁ + 1 / 2 * 15) / (7 / 3 + 1 / 2)

Case 1 of the proof of Theorem 1.1 (q ≤ q₀). Given M, D' satisfying the two recombination inequalities from E₁ and E₂: M ≤ A₁ − (1/2) D' (Equation (12), from one-sided recombination with E₁) M ≤ 15 + (7/3) D' (Equation (13), from one-sided recombination with E₂) we conclude M ≤ C₁.

Reference: Case 1 in Section 5 of the companion paper, Equations (12)–(14).

theorem KaltonRoberts.case1_bound_eq_C₁ : have D₁ := 6 * q₀ + 4 + τ₁ * (2 * q₀ + 2); have A₁ := 10 + 3 / 2 * D₁; (7 / 3 * A₁ + 1 / 2 * 15) / (7 / 3 + 1 / 2) = C₁

In Case 1, the balanced bound equals C₁. Reference: Equation (14) in Section 5 of the companion paper.

Case 2 details

theorem KaltonRoberts.case2_bound (M Y : ℝ) (_hY : 0 ≤ Y) (A₂ : ℝ) (h1 : M ≤ A₂ - 2 / 5 * Y) (h2 : M ≤ 47 / 3 + 11 / 6 * Y) : M ≤ (11 / 6 * A₂ + 2 / 5 * (47 / 3)) / (11 / 6 + 2 / 5)

Case 2 of the proof of Theorem 1.1 (q ≥ q₀). Given M, Y satisfying the two recombination inequalities from E₃ and E₄: M ≤ A₂ − (2/5) Y (Equation (15), from two-sided recombination with E₃) M ≤ 47/3 + (11/6) Y (Equation (16), from two-sided recombination with E₄) we conclude M ≤ C₂.

Reference: Case 2 in Section 5 of the companion paper, Equations (15)–(17).

theorem KaltonRoberts.case2_bound_eq_C₂ : have X₀ := 4 * p₀ + 6 + τ₂ * (p₀ + 1); have A₂ := 47 / 5 + 7 / 5 * X₀; (11 / 6 * A₂ + 2 / 5 * (47 / 3)) / (11 / 6 + 2 / 5) = C₂

In Case 2, the balanced bound equals C₂. Reference: Equation (17) in Section 5 of the companion paper.

The u-bound (Equation (3))

theorem KaltonRoberts.u_bound {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (_M : ℝ) (_hM : 0 ≤ _M) (hMbound : ∀ (S : Finset U), |f S| ≤ _M) (P : Finset U) (hP : f P = _M) (N : Finset U) (hN : f N = -_M) : |f Finset.univ| ≤ 1

The finite normalised theorem

theorem KaltonRoberts.exists_additive_approx (U : Type u_1) [Finite U] (f : Finset U → ℝ) (C : ℝ) (hC : distToAdditive f ≤ C) : ∃ (a : U → ℝ), ∀ (S : Finset U), |f S - additiveFunction a S| ≤ C

theorem KaltonRoberts.distToAdditive_le_C₂ (U : Type u_1) [DecidableEq U] [Finite U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) : distToAdditive f ≤ ↑C₂

Core distance bound: distToAdditive f ≤ C₂.

The proof depends on the full pipeline:

1. Dual certificate (proved in DualCert.lean)
2. Weighted collection construction (proved in Collections.lean)
3. Mixed intersection construction (Corollary 3.1)
4. Expander recombination (Lemmas 3.2–3.3)
5. Expander existence via Pippenger entropy (Lemma 4.1)
6. Case analysis and balancing (Section 5)

The theorem distToAdditive_le_C₂_from_pipeline in Pipeline.lean makes explicit each missing ingredient as a hypothesis. Here we instantiate those hypotheses from the concrete theorems.

theorem KaltonRoberts.finite_KR_bound (U : Type u_1) [DecidableEq U] [Finite U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) : ∃ (a : U → ℝ), ∀ (S : Finset U), |f S - additiveFunction a S| ≤ ↑C₂

theorem KaltonRoberts.boolean_KR_bound_C₂ (α : Type u_1) [BooleanAlgebra α] (f : α → ℝ) (hf : IsApproxAdditiveBA f 1) : ∃ (μ : α → ℝ), IsFinitelyAdditiveBA μ ∧ ∀ (A : α), |f A - μ A| ≤ ↑C₂

The normalized theorem on arbitrary Boolean algebras, obtained from the finite powerset theorem by the compact reduction.

theorem KaltonRoberts.boolean_KR_bound_C₂_delta (α : Type u_1) [BooleanAlgebra α] (f : α → ℝ) (Δ : ℝ) (hΔ : 0 ≤ Δ) (hf : IsApproxAdditiveBA f Δ) : ∃ (μ : α → ℝ), IsFinitelyAdditiveBA μ ∧ ∀ (A : α), |f A - μ A| ≤ ↑C₂ * Δ

Theorem 1.1 in its scaled Boolean-algebra form.

theorem KaltonRoberts.set_algebra_bound_C₂ {Ω : Type u_1} (F : BooleanSubalgebra (Set Ω)) (f : ↥F → ℝ) (Δ : ℝ) (hΔ : 0 ≤ Δ) (hf : IsApproxAdditiveBA f Δ) : ∃ (μ : ↥F → ℝ), IsFinitelyAdditiveBA μ ∧ ∀ (A : ↥F), |f A - μ A| ≤ ↑C₂ * Δ

The paper's set-algebra formulation. A set algebra is represented as a Boolean subalgebra of Set Ω.

Main theorem

theorem KaltonRoberts.KR_constant_le_C₂ : krConstant ≤ ↑C₂

Theorem 1.1 (Main theorem). The Kalton–Roberts constant satisfies K_KR ≤ C₂ = 694198146664396294486127753 / 34994834677886019996000000. Consequently, K_KR < 9919/500 = 19.838.

Reference: Theorem 1.1 in Section 1 of the companion paper.

theorem KaltonRoberts.KR_constant_lt : krConstant < 9919 / 500

Theorem 1.1, headline inequality. Reference: second display of Theorem 1.1 in the companion paper.