Finite indexed planar configurations
DefinitionEsgk_Foundationdiscrete-geometrydistinct-distances
A raw configuration is a map from the finite index set Fin n to the Euclidean plane and may repeat points. Its associated finite set is its image; the theorem hypotheses impose injectivity so their configurations have n different points.
Definition code
/-
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
import Definitions.Def_Esgk_PlanarGeneralPosition
/-!
# Foundation — indexed planar configurations
The numerical targets are stated for injective maps `Fin n → ℝ²`; this module
provides that configuration type and its associated finite set.
-/
namespace Esgk
open EuclideanGeometry
/-- Alias for the ambient plane in this problem. -/
abbrev Point : Type := ℝ²
/-- An indexed configuration of `n` points in the plane. -/
abbrev Config (n : ℕ) : Type := Fin n → Point
/-- Image-finset of an indexed configuration: the set of points that appear in `p`. -/
noncomputable def Config.toFinset {n : ℕ} (p : Config n) : Finset Point := Finset.image p Finset.univ
end Esgk
Source
Self-contained formal statement prepared for this mission.
Read-back
What the Lean code literally says, in plain math · independent subagent audit (2026-09-11)
Within namespace Esgk, Point abbreviates ℝ² and Config n abbreviates functions Fin n → ℝ². Config.toFinset p is the image of p on Finset.univ. The definition permits repeated indexed points; the image collapses repetitions, and the theorem hypotheses impose injectivity separately.
Human review
Confirmed by the mission captain (proposal self-audit).