Planarity constraints on squared distances

Three exact identities carry all of the geometry in this project. Each is a polynomial identity in the coordinates of the points involved, so each is proved by ring.

• four_mul_mul_sub_sq_eq is Heron's formula in squared-distance form. Its corollary sq_le_four_mul is the triangle inequality written without square roots, and it is the only inequality the classification of chain triangles needs.
• gramDet_eq_zero says that the doubled Gram matrix of three plane vectors anchored at a fourth point is singular. Expressed in the six squared distances of four points this is the Cayley--Menger relation, and it is the only equation the four-point catalogue needs.
• gram3_det_eq_zero is the same singularity written directly in inner products; together with sq_nonneg_combo it supplies the five-point obstruction.

def Erdos132ThreeChain.cross (p q r : Point) : ℝ

Twice the signed area of the triangle p q r; equivalently the two-dimensional cross product of q - p and r - p.

Equations

• Erdos132ThreeChain.cross p q r = (q.1 - p.1) * (r.2 - p.2) - (r.1 - p.1) * (q.2 - p.2)

theorem Erdos132ThreeChain.four_mul_mul_sub_sq_eq (p q r : Point) : 4 * sqDist p q * sqDist p r - (sqDist q r - sqDist p q - sqDist p r) ^ 2 = 4 * cross p q r ^ 2

Heron's formula in squared-distance form: the Cayley--Menger expression of a triangle is four times the square of its doubled signed area.

theorem Erdos132ThreeChain.sq_le_four_mul (p q r : Point) : (sqDist q r - sqDist p q - sqDist p r) ^ 2 ≤ 4 * sqDist p q * sqDist p r

The triangle inequality for three plane points, stated without square roots.

def Erdos132ThreeChain.dotp (o p q : Point) : ℝ

The inner product of p - o and q - o.

Equations

• Erdos132ThreeChain.dotp o p q = (p.1 - o.1) * (q.1 - o.1) + (p.2 - o.2) * (q.2 - o.2)

theorem Erdos132ThreeChain.dotp_self (o p : Point) : dotp o p p = sqDist p o

theorem Erdos132ThreeChain.two_mul_dotp (o p q : Point) : 2 * dotp o p q = sqDist p o + sqDist q o - sqDist p q

def Erdos132ThreeChain.gramDet (dab dac dad dbc dbd dcd : ℝ) : ℝ

The determinant of the doubled Gram matrix of b - a, c - a, d - a, written in the six squared distances of a, b, c, d.

Equations

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

theorem Erdos132ThreeChain.gramDet_eq_zero (a b c d : Point) : gramDet (sqDist a b) (sqDist a c) (sqDist a d) (sqDist b c) (sqDist b d) (sqDist c d) = 0

Three vectors of the plane are linearly dependent, so the anchored Gram determinant of any four plane points vanishes. This is the Cayley--Menger relation for four coplanar points.

theorem Erdos132ThreeChain.gram3_det_eq_zero (o p q r : Point) : dotp o p p * (dotp o q q * dotp o r r - dotp o q r ^ 2) - dotp o p q * (dotp o p q * dotp o r r - dotp o q r * dotp o p r) + dotp o p r * (dotp o p q * dotp o q r - dotp o q q * dotp o p r) = 0

The Gram determinant of three plane vectors vanishes.

theorem Erdos132ThreeChain.sq_nonneg_combo (o p q r s : Point) (x y z w : ℝ) : 0 ≤ x ^ 2 * dotp o p p + y ^ 2 * dotp o q q + z ^ 2 * dotp o r r + w ^ 2 * dotp o s s + 2 * (x * y * dotp o p q + x * z * dotp o p r + x * w * dotp o p s + y * z * dotp o q r + y * w * dotp o q s + z * w * dotp o r s)

The squared length of a linear combination of four plane vectors is nonnegative, expanded in inner products.