The bridge: Problem 97 implies the 3n bound and Problem 96
ProvedErdos9796Mission.linear_bound_of_problem97Assume the affirmative statement of Erdős Problem 97 for every nonempty finite convex-independent point set in the Euclidean plane. Then every finite convex-independent set , including the empty set, satisfies
and the extremal function satisfies
Here counts unordered pairs of distinct points at distance one, each pair once, and is the supremum of these counts over convex-independent n-point sets. Both conclusions are required. This is a conditional theorem, with Problem 97 as an explicit hypothesis. The repository records the conditional peeling proof and the subsequent supremum-to-Big-O step; transferring both makes the complete link between the two mission targets reusable.
/- Statement-only mission draft: SKETCH — NOT PROMOTABLE. Source and precise status are recorded in items.json. -/ import Definitions.Def_Erdos9796Mission open Erdos9796Mission
theorem Erdos9796Mission.linear_bound_of_problem97 :
Problem97 → (∀ A : Finset Plane, ConvexIndep (A : Set Plane) → unitDistancePairsCount A ≤ 3 * A.card) ∧ Problem96 := by sorryRead-back
What the Lean code literally says, in plain math · gpt-5.6-luna
Assume that every nonempty finite set of points in the real Euclidean plane whose points all lie outside the real convex hull of the remaining points fails to have the following property: for every there is a positive real radius such that has cardinality at least . Then both of the following hold: for every finite set of plane points satisfying the same convex-hull condition, including the possibility that is empty, the number of unordered two-element pairs from counted once, where a pair is counted exactly when and , is at most ; and the real-valued function sending to the natural-number supremum of these unit-distance counts over finite convex-independent point sets of cardinality grows as along natural numbers tending to infinity.
Confirmed by the mission captain (proposal self-audit).