Prove2Me

Section 3, display on p. 387 — 2i/3(1−2/M)4i/3<200/((.1)1/322/3)2^{i/3}(1-2/M)^{4i/3} < 200/((.1)^{1/3}2^{2/3}) fails for i≥30i \ge 30

Proved
SzemerediTrotter.Incidence.termination_inequality

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-geometryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1real-inequalities

Let M=1010M = 10^{10}. For every natural number i≥30i \ge 30,

200(0.1)1/3 22/3≤2i/3(1−2M)4i/3.\frac{200}{(0.1)^{1/3}\,2^{2/3}} \le 2^{i/3}\Bigl(1-\frac{2}{M}\Bigr)^{4i/3}.

Equivalently, the inequality 2i/3(1−2/M)4i/3<200/((.1)1/322/3)2^{i/3}(1-2/M)^{4i/3} < 200/((.1)^{1/3}2^{2/3}) obtained on p. 387 of Szemerédi and Trotter fails whenever i≥30i \ge 30. In the proof of Theorem 1 this shows that the inductive construction of the point sets Pi\mathcal P_i terminates after fewer than 3030 steps.

Formalization Note M=1010M = 10^{10} is written out in the statement. The exponents i/3i/3 and 4i/34i/3 are real numbers (the natural number ii is cast to R\mathbb R before dividing), and the powers are Real.rpow; the bases 22, 0.10.1 and 1−2/M1 - 2/M are positive.

Preamble
import Mathlib
Formal statement
namespace SzemerediTrotter.Incidence

/-- Section 3, display on p. 387, with `M = 10¹⁰` (p. 386): the inequality
`2^{i/3}(1 − 2/M)^{4i/3} < 200/((.1)^{1/3} 2^{2/3})` fails for every `i ≥ 30`. -/
theorem termination_inequality :
    ∀ i : ℕ, 30 ≤ i →
      (200 : ℝ) / ((0.1 : ℝ) ^ (1 / 3 : ℝ) * (2 : ℝ) ^ (2 / 3 : ℝ))
        ≤ (2 : ℝ) ^ ((i : ℝ) / 3) * (1 - 2 / (10 : ℝ) ^ 10) ^ (4 * (i : ℝ) / 3) := by sorry

end SzemerediTrotter.Incidence
Source
Szemerédi, Trotter, Extremal Problems in Discrete Geometry, Combinatorica 3 (1983), p. 387, Section 3, display on p. 387 (with M = 10¹⁰ set on p. 386)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph