Erdős 97 convex-octagon formalization: Cayley Menger

noncomputable def Erdos97Octagon.sqDist (a b : Plane) : ℝ

Squared Euclidean distance.

Equations

• Erdos97Octagon.sqDist a b = dist a b ^ 2

def Erdos97Octagon.cm4 (A B C D E F : ℝ) : ℝ

The four-point Cayley--Menger polynomial in its six squared distances.

Equations

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

theorem Erdos97Octagon.inner_sub_sub_eq (a b c : Plane) : inner ℝ (b - a) (c - a) = (sqDist a b + sqDist a c - sqDist b c) / 2

Polarisation expresses an inner product through three squared distances.

theorem Erdos97Octagon.cm4_sqDist_eq_zero (a b c d : Plane) : cm4 (sqDist a b) (sqDist a c) (sqDist a d) (sqDist b c) (sqDist b d) (sqDist c d) = 0

Four planar points have vanishing Cayley--Menger determinant.

theorem Erdos97Octagon.cm4_normalized_eq_zero (a b c d : Plane) {s : ℝ} (hs : s ≠ 0) : cm4 (sqDist a b / s) (sqDist a c / s) (sqDist a d / s) (sqDist b c / s) (sqDist b d / s) (sqDist c d / s) = 0

The Cayley--Menger identity remains zero after dividing all squared distances by one common nonzero scale.