OAI.PlanarUnitDistances.main
ProvedThe theorem states that there exist real constants C and β with C>0, 1≤β<4/3, such that u(n) ≤ C·n^β for every natural number n. Here the plane is two-dimensional Euclidean space ℝ². A pair of points is a unit pair when their Euclidean distance is exactly 1 (the condition is symmetric, so it is defined on unordered pairs). For a finite set X of points, unitPairCount(X) is the number of unordered pairs from X, as given by Sym2 of X, that are unit pairs. Then u(n) is the supremum, taken in the natural numbers, of the values unitPairCount(X) over all n-point finite subsets X of the plane, i.e. the maximum possible number of unit distances among n points. So the statement is a power-law upper bound on this maximum with exponent strictly below 4/3; the proof is admitted with sorry in the source.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/PlanarUnitDistances.lean; bytes 458..600 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_PlanarUnitDistances namespace OAI namespace PlanarUnitDistances
theorem main : ∃ C β : ℝ, 0 < C ∧ 1 ≤ β ∧ β < (4 : ℝ) / 3 ∧
∀ n : ℕ, (u n : ℝ) ≤ C * (n : ℝ) ^ β := by
sorry
end PlanarUnitDistances
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.