The convex three-largest-distance graph

Definitions for the internal convex k = 3 Erdős 132 draft. Geometry is expressed through exact signed areas, while the graph uses squared distances; this keeps the rational campaign witnesses kernel-reducible.

The open Erdős 132 conjecture is not asserted here. Recon: ~/Knowledge/Construct/recon/erdos_132.md.

@[reducible, inline]

abbrev LeanPool.Erdos132ConvexK3.Point (K : Type u_1) : Type u_1

A Cartesian point over an ordered coordinate ring.

Equations

• LeanPool.Erdos132ConvexK3.Point K = (K × K)

def LeanPool.Erdos132ConvexK3.cross {K : Type u_1} [Ring K] (u v : Point K) : K

Signed two-dimensional cross product.

Equations

• LeanPool.Erdos132ConvexK3.cross u v = u.1 * v.2 - u.2 * v.1

def LeanPool.Erdos132ConvexK3.dot {K : Type u_1} [Ring K] (u v : Point K) : K

Cartesian dot product. Keeping this polynomial form explicit lets the majorant angle argument stay over exact ordered rings.

Equations

• LeanPool.Erdos132ConvexK3.dot u v = u.1 * v.1 + u.2 * v.2

def LeanPool.Erdos132ConvexK3.turn {K : Type u_1} [Ring K] (a b c : Point K) : K

Signed turn from the ray a ⟶ b to the ray a ⟶ c.

Equations

• LeanPool.Erdos132ConvexK3.turn a b c = (b.1 - a.1) * (c.2 - a.2) - (b.2 - a.2) * (c.1 - a.1)

def LeanPool.Erdos132ConvexK3.sqDist {K : Type u_1} [Ring K] (a b : Point K) : K

Squared Euclidean distance, used to compare distance classes exactly.

Equations

• LeanPool.Erdos132ConvexK3.sqDist a b = (b.1 - a.1) ^ 2 + (b.2 - a.2) ^ 2

theorem LeanPool.Erdos132ConvexK3.sqDist_comm {K : Type u_1} [CommRing K] (a b : Point K) : sqDist a b = sqDist b a

def LeanPool.Erdos132ConvexK3.cyclicNext {n : ℕ} [NeZero n] (i : Fin n) : Fin n

The next index in a cyclic labelling.

Equations

• LeanPool.Erdos132ConvexK3.cyclicNext i = i + 1

def LeanPool.Erdos132ConvexK3.CyclicStrictConvex {K : Type u_1} [Ring K] [LinearOrder K] {n : ℕ} [NeZero n] (P : Fin n → Point K) : Prop

Strict convex position in a specified cyclic order.

Every vertex other than the endpoints of a boundary edge lies strictly in that oriented edge's left open half-plane. This signed-area formulation is stronger and less ambiguous than checking consecutive turns alone.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Erdos132ConvexK3.StrictConvexQuad {K : Type u_1} [Ring K] [LinearOrder K] (a b c d : Point K) : Prop

Four vertices in positive cyclic order, in the exact form needed for the diagonal-crossing proof.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Erdos132ConvexK3.InLeftOpenHalfPlane {K : Type u_1} [Ring K] [LinearOrder K] (a b p : Point K) : Prop

Membership in the open left half-plane of the oriented line a ⟶ b.

Equations

• LeanPool.Erdos132ConvexK3.InLeftOpenHalfPlane a b p = (0 < LeanPool.Erdos132ConvexK3.turn a b p)

def LeanPool.Erdos132ConvexK3.unorderedPairList (n : ℕ) : List (Fin n × Fin n)

Executable increasing representatives of unordered pairs of labels.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Erdos132ConvexK3.unorderedPairs (n : ℕ) : Finset (Fin n × Fin n)

Increasing representatives of unordered pairs of labels.

Equations

• LeanPool.Erdos132ConvexK3.unorderedPairs n = (LeanPool.Erdos132ConvexK3.unorderedPairList n).toFinset

def LeanPool.Erdos132ConvexK3.realizedSquaredDistances {K : Type u_1} [Ring K] [DecidableEq K] {n : ℕ} (P : Fin n → Point K) : Finset K

The squared distance classes realized by a labelled configuration.

Equations

• LeanPool.Erdos132ConvexK3.realizedSquaredDistances P = Finset.image (fun (e : Fin n × Fin n) => LeanPool.Erdos132ConvexK3.sqDist (P e.1) (P e.2)) (LeanPool.Erdos132ConvexK3.unorderedPairs n)

def LeanPool.Erdos132ConvexK3.HasTopThreeDistanceClasses {K : Type u_1} [Ring K] [LinearOrder K] {n : ℕ} (P : Fin n → Point K) (d₁ d₂ d₃ : K) : Prop

d₁ > d₂ > d₃ are exactly the three largest squared distance classes.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Erdos132ConvexK3.mem_unorderedPairList_iff {n : ℕ} {i j : Fin n} : (i, j) ∈ unorderedPairList n ↔ i < j

The executable unordered-pair list contains exactly the increasing representatives.

theorem LeanPool.Erdos132ConvexK3.sqDist_nonneg (a b : Point ℝ) : 0 ≤ sqDist a b

theorem LeanPool.Erdos132ConvexK3.sqDist_pos_of_ne {a b : Point ℝ} (h : a ≠ b) : 0 < sqDist a b

Distinct real points have positive squared distance.

theorem LeanPool.Erdos132ConvexK3.top_three_class_bounds_of_ne {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i j : Fin n} (hij : i ≠ j) : have d := sqDist (P i) (P j); d ≤ d₁ ∧ (d < d₁ → d ≤ d₂) ∧ (d < d₂ → d ≤ d₃)

The top-three predicate supplies its global distance bound for every ordered pair of distinct labels, not only for the increasing representative stored in unorderedPairList.

def LeanPool.Erdos132ConvexK3.cyclicStrictConvexCheck {K : Type u_1} [Ring K] [LinearOrder K] {n : ℕ} [NeZero n] (P : Fin n → Point K) : Bool

Executable checker for CyclicStrictConvex.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Erdos132ConvexK3.cyclicStrictConvex_of_check {K : Type u_1} [Ring K] [LinearOrder K] {n : ℕ} [NeZero n] {P : Fin n → Point K} (h : cyclicStrictConvexCheck P = true) : CyclicStrictConvex P

def LeanPool.Erdos132ConvexK3.hasTopThreeDistanceClassesCheck {K : Type u_1} [Ring K] [LinearOrder K] {n : ℕ} (P : Fin n → Point K) (d₁ d₂ d₃ : K) : Bool

Executable checker for the exact top-three distance-class predicate.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Erdos132ConvexK3.hasTopThreeDistanceClasses_of_check {K : Type u_1} [Ring K] [LinearOrder K] {n : ℕ} {P : Fin n → Point K} {d₁ d₂ d₃ : K} (h : hasTopThreeDistanceClassesCheck P d₁ d₂ d₃ = true) : HasTopThreeDistanceClasses P d₁ d₂ d₃

def LeanPool.Erdos132ConvexK3.TopThreeAdjacent {K : Type u_1} [Ring K] {n : ℕ} (P : Fin n → Point K) (d₁ d₂ d₃ : K) (i j : Fin n) : Prop

Adjacency in the union of the three named largest distance classes.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Erdos132ConvexK3.topThreeGraph {K : Type u_1} [CommRing K] {n : ℕ} (P : Fin n → Point K) (d₁ d₂ d₃ : K) : SimpleGraph (Fin n)

The graph G(S,3) for three explicitly identified distance classes.

Equations

• LeanPool.Erdos132ConvexK3.topThreeGraph P d₁ d₂ d₃ = { Adj := fun (i j : Fin n) => LeanPool.Erdos132ConvexK3.TopThreeAdjacent P d₁ d₂ d₃ i j, symm := ⋯, loopless := ⋯ }

def LeanPool.Erdos132ConvexK3.vertexDegree {K : Type u_1} [CommRing K] [DecidableEq K] {n : ℕ} (P : Fin n → Point K) (d₁ d₂ d₃ : K) (i : Fin n) : ℕ

Vertex degree in G(S,3), executable for exact coordinate fields.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Erdos132ConvexK3.vertexDegree_eq_of_neighbors {K : Type u_1} [CommRing K] [DecidableEq K] {n : ℕ} (P : Fin n → Point K) (d₁ d₂ d₃ : K) (i : Fin n) (N : Finset (Fin n)) (hN : ∀ (j : Fin n), j ∈ N ↔ j ≠ i ∧ (sqDist (P i) (P j) = d₁ ∨ sqDist (P i) (P j) = d₂ ∨ sqDist (P i) (P j) = d₃)) : vertexDegree P d₁ d₂ d₃ i = N.card