Planar general position and distinct Euclidean distances
DefinitionEsgk_PlanarGeneralPositionDefines the Euclidean plane, a predicate excluding three collinear points, the number of distinct values of dist on pairs of different points, and full general position requiring both no three collinear and no four cocircular points.
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
import Mathlib
/-!
# Planar general-position primitives
Self-contained definitions used by the distinct-distances mission.
-/
scoped[EuclideanGeometry] notation "ℝ²" => EuclideanSpace ℝ (Fin 2)
namespace Set
variable {α : Type*}
/-- A ternary relation holds for every three pairwise-distinct members of a set. -/
protected def Triplewise (s : Set α) (r : α → α → α → Prop) : Prop :=
∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃z⦄, z ∈ s →
x ≠ y → y ≠ z → x ≠ z → r x y z
end Set
open scoped EuclideanGeometry Finset
namespace EuclideanGeometry
variable {V P : Type*}
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
/-- No three distinct points of `A` are collinear. -/
def NonTrilinear (A : Set P) : Prop :=
A.Triplewise (fun x y z ↦ ¬ Collinear ℝ {x, y, z})
/-- The number of distances occurring between distinct points of a finite planar set. -/
noncomputable def distinctDistances (points : Finset ℝ²) : ℕ :=
#(points.offDiag.image fun pair : ℝ² × ℝ² => dist pair.1 pair.2)
/-- No three points are collinear and no four points are cocircular. -/
def InGeneralPosition (X : Finset ℝ²) : Prop :=
NonTrilinear (SetLike.coe X) ∧
∀ T ⊆ X, #T = 4 → ¬Cospherical (SetLike.coe T)
end EuclideanGeometry
Read-back
What the Lean code literally says, in plain math · independent subagent audit (2026-09-11)
Defines ℝ² as EuclideanSpace ℝ (Fin 2). For any type α, Set.Triplewise s r says that a ternary relation r holds for every three pairwise-distinct members of s. For an ambient metric torsor P over a real inner-product space V, NonTrilinear A says that no three pairwise-distinct points of A are collinear. For a finite X ⊆ ℝ², distinctDistances X is the natural-number cardinality of the image of all ordered off-diagonal pairs under Euclidean distance. InGeneralPosition X requires NonTrilinear X and requires every four-point sub-finset of X not to be Cospherical.
Confirmed by the mission captain (proposal self-audit).