Superlinear convex unit-distance family
OpenErdos9796Mission.problem96_superlinear_familyconvex-positiondiscrete-geometryerdos-96unit-distances
For every nonnegative proposed linear constant and every cutoff, some larger cardinality has maximum convex unit-distance count exceeding that constant times the cardinality.
Closed by the mission owner on 2026-09-13 after the Kruer–Kohlmeyer–Price negative resolution of Erdős 96 and 97. No further work is requested on this historical project task. This retirement is administrative and does not assert that this individual lemma is false. The resolution is recorded on Erdos9796Mission.problem97, Erdos9796Mission.problem96, and Erdos9796Mission.combined.
Preamble
import Definitions.Def_Erdos9796Mission
Formal statement
theorem Erdos9796Mission.problem96_superlinear_family :
∀ C : ℝ, 0 ≤ C → ∀ N : ℕ, ∃ n : ℕ,
N ≤ n ∧
C * (n : ℝ) <
(Erdos9796Mission.maxConvexUnitDistances n : ℝ) := by sorrySource