OAI.PlanarUnitDistances.AlgebraicObstruction.no_rectangles: intermediate lemma from OpenAI, A power saving for planar unit distances

Proved

OAI.PlanarUnitDistances.AlgebraicObstruction.no_rectangles

by dbenbenn · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.PlanarUnitDistances.main, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, A power saving for planar unit distances, OpenAI Math Release, September 23, 2026, result family 167, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.PlanarUnitDistances.AlgebraicObstruction.no_rectangles of lean/OAI/Geometry/UnitDistances/UnitDistances/Obstruction.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.PlanarUnitDistances.AlgebraicObstruction, with open Filter UnitDistances.UltraField PowerGrowth FiniteGraphPruning):

theorem no_rectangles (U : Ultrafilter ℕ) (hU : (U : Filter ℕ)≤atTop)
    (t J : ℕ → ℝ) (ht : Tendsto t (U : Filter ℕ) atTop)
    (hJ : Tendsto J (U : Filter ℕ) atTop) (P : ℕ → Finset ℂ)
    (hP : Upper (U : Filter ℕ) t (fun n => (P n).card) 1)
    (E : ℕ → ℂ → ℂ → Prop)
    (he : Lower (U : Filter ℕ) t
      (fun n => (GenericGrid.edges (fun n (a : P n) (b : P n) => E n a b) n).card) 2)
    (K : ℕ → Type) [∀ n,Field (K n)] [∀ n,NumberField (K n)] [∀ n,IsGalois ℚ (K n)]
    (e : ∀ n,K n →+* ℂ) (ell : ∀ n,ℂ → ℂ → K n)
    (H : Hypotheses U t J P E K e ell) : False

Definitions. The statement is written with OAI.PlanarUnitDistances.AlgebraicObstruction.Hypotheses, OAI.PlanarUnitDistances.GenericGrid.edges, OAI.PlanarUnitDistances.PowerGrowth.Lower and OAI.PlanarUnitDistances.PowerGrowth.Upper (definitions bundle OAIQ2Un000 of this split).

Used by. The proof of OAI.PlanarUnitDistances.main of this split imports it.

Preamble

import Mathlib
import Definitions.Def_OAIQ2Un000

Formal statement

section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

namespace PlanarUnitDistances.AlgebraicObstruction
open Filter UnitDistances.UltraField PowerGrowth FiniteGraphPruning

theorem no_rectangles (U : Ultrafilter ℕ) (hU : (U : Filter ℕ)≤atTop)
    (t J : ℕ → ℝ) (ht : Tendsto t (U : Filter ℕ) atTop)
    (hJ : Tendsto J (U : Filter ℕ) atTop) (P : ℕ → Finset ℂ)
    (hP : Upper (U : Filter ℕ) t (fun n => (P n).card) 1)
    (E : ℕ → ℂ → ℂ → Prop)
    (he : Lower (U : Filter ℕ) t
      (fun n => (GenericGrid.edges (fun n (a : P n) (b : P n) => E n a b) n).card) 2)
    (K : ℕ → Type) [∀ n,Field (K n)] [∀ n,NumberField (K n)] [∀ n,IsGalois ℚ (K n)]
    (e : ∀ n,K n →+* ℂ) (ell : ∀ n,ℂ → ℂ → K n)
    (H : Hypotheses U t J P E K e ell) : False := by
  sorry
end PlanarUnitDistances.AlgebraicObstruction

end OAI
end

Source

OpenAI, A power saving for planar unit distances, OpenAI Math Release, September 23, 2026, https://github.com/openai/math (result family 167; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-power-saving-for-planar-unit-distances-September-23-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Geometry/UnitDistances/UnitDistances/Obstruction.lean (declaration OAI.PlanarUnitDistances.AlgebraicObstruction.no_rectangles)

View graph