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

Proved

OAI.PlanarUnitDistances.IncidenceSequence.diagonal_sequence

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.IncidenceSequence.diagonal_sequence of lean/OAI/Geometry/UnitDistances/UnitDistances/Sequence.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.PlanarUnitDistances.IncidenceSequence, with open Filter PowerGrowth CircleIncidence, open scoped Classical):

theorem diagonal_sequence {t : ℕ → ℝ} {X : ℕ → Finset Plane}
    (ht : Tendsto t atTop atTop) (ht1 : ∀i,1 ≤ t i) (hX0 : ∀i,(X i).Nonempty)
    (hX : Upper atTop t (fun i => ((X i).card:ℝ)) 3)
    (hE : Lower atTop t (fun i => incidences (X i) (X i)) 4)
    (hAlg : ∀i,∀p∈X i,∀k,IsAlgebraic ℚ (p k)) : Nonempty Sequence

Definitions. The statement is written with OAI.PlanarUnitDistances.CircleIncidence.incidences, OAI.PlanarUnitDistances.IncidenceSequence.Plane, OAI.PlanarUnitDistances.IncidenceSequence.Sequence, 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

attribute [-instance] _root_.OAI.PlanarUnitDistances.IncidenceDiagonal.Data.instFieldK _root_.OAI.PlanarUnitDistances.IncidenceDiagonal.Data.instIsGaloisRatK _root_.OAI.PlanarUnitDistances.IncidenceDiagonal.Data.instNumberFieldK
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

namespace PlanarUnitDistances.IncidenceSequence
open Filter PowerGrowth CircleIncidence
open scoped Classical
noncomputable section

theorem diagonal_sequence {t : ℕ → ℝ} {X : ℕ → Finset Plane}
    (ht : Tendsto t atTop atTop) (ht1 : ∀i,1 ≤ t i) (hX0 : ∀i,(X i).Nonempty)
    (hX : Upper atTop t (fun i => ((X i).card:ℝ)) 3)
    (hE : Lower atTop t (fun i => incidences (X i) (X i)) 4)
    (hAlg : ∀i,∀p∈X i,∀k,IsAlgebraic ℚ (p k)) : Nonempty Sequence := by
  sorry

end
end PlanarUnitDistances.IncidenceSequence

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/Sequence.lean (declaration OAI.PlanarUnitDistances.IncidenceSequence.diagonal_sequence)

View graph