Erdős Problems 97 and 96: the combined convex-distance mission
DisprovedErdos9796Mission.combinedEstablish both affirmative statements in one package: every nonempty finite convex-independent planar point set has a vertex with no four other vertices at a common positive distance, and the maximum number of unordered unit-distance pairs among convex-independent -point sets is .
The two targets are linked by deletion: Problem 97 supplies a vertex of unit degree at most three in every nonempty remaining subset, so counting each edge when its first endpoint is removed gives at most unordered unit-distance pairs. No implication from Problem 96 back to Problem 97 is asserted. Both statements are open targets, not assumptions hidden in the definitions.
import Definitions.Def_Erdos9796Mission /-! The combined open Erdős Problems 97 and 96 mission statement. -/
theorem Erdos9796Mission.combined :
Erdos9796Mission.Problem97 ∧ Erdos9796Mission.Problem96 := by sorryRead-back
What the Lean code literally says, in plain math · gpt-5.6-luna
The declaration asserts the conjunction of the two preceding targets. First, for every nonempty finite point set in the Euclidean plane whose points are all absent from the convex hull over of the other points, at least one has fewer than four points of at every positive exact distance from . Second, there are and such that for every natural , the supremum of the numbers of unordered unit-distance pairs among convexly independent -point sets, cast to , is at most ; the supremum is the natural-number supremum of the set of counts and uses its empty-set convention. The theorem body is sorry, so this conjunction is an asserted target rather than an established result.
Confirmed by the mission captain (proposal self-audit).