Coordinate geometry for the planar diameter bound

This file isolates the two algebraic facts used in the Perles charging proof of the planar diameter bound. Working with dot products and signed areas keeps all collinear cases explicit and avoids a general-position assumption.

def LeanPool.Erdos132N14.diameterDot (z w : ℂ) : ℝ

The real dot product on the complex model of the Euclidean plane.

Equations

• LeanPool.Erdos132N14.diameterDot z w = z.re * w.re + z.im * w.im

def LeanPool.Erdos132N14.planeCross (z w : ℂ) : ℝ

The signed two-dimensional cross product on the complex plane.

Equations

• LeanPool.Erdos132N14.planeCross z w = z.re * w.im - z.im * w.re

def LeanPool.Erdos132N14.planeTurn (a b c : ℂ) : ℝ

The signed turn from the ray a ⟶ b to the ray a ⟶ c.

Equations

• LeanPool.Erdos132N14.planeTurn a b c = LeanPool.Erdos132N14.planeCross (b - a) (c - a)

theorem LeanPool.Erdos132N14.planeDot_self (z : ℂ) : diameterDot z z = Complex.normSq z

theorem LeanPool.Erdos132N14.planeCross_swap (z w : ℂ) : planeCross w z = -planeCross z w

theorem LeanPool.Erdos132N14.planeTurn_swap (a b c : ℂ) : planeTurn a c b = -planeTurn a b c

theorem LeanPool.Erdos132N14.plane_lagrange (x y z : ℂ) : diameterDot x x * diameterDot y z = diameterDot x y * diameterDot x z + planeCross x y * planeCross x z

Lagrange's identity in the form needed by the diameter argument.

theorem LeanPool.Erdos132N14.equal_rays_of_cross_eq_zero {u v w : ℂ} {d : ℝ} (huv : dist u v = d) (huw : dist u w = d) (hvw : dist v w ≤ d) (hd : 0 < d) (hcross : planeCross (v - u) (w - u) = 0) : v = w

Two equal-length rays with zero signed area coincide if the distance between their endpoints is no longer than the rays.

theorem LeanPool.Erdos132N14.opposite_turns_force_longer_pair {u v a b : ℂ} {d : ℝ} (huv : dist u v = d) (hua : dist u a = d) (hvb : dist v b = d) (hd : 0 < d) (ha : planeTurn u v a < 0) (hb : planeTurn v u b < 0) : d < dist a b

If three equal-length edges leave the two ends of a fourth one on opposite signed sides, the two free endpoints are farther apart.

This is the algebraic core of the fact that two disjoint diameter edges in the plane must cross.