The five-point obstruction

The four-point catalogue confines a chain configuration to one adjacent pair {c, 3 * c} and forces a common anchor. What survives is a very rigid picture: four points at squared distance c from a common centre, with pairwise squared distances c or 3 * c.

no_four_on_circle rules that picture out. Writing u i for the vector from the centre to the i-th point, the hypotheses give ⟪u i, u i⟫ = c and ⟪u i, u j⟫ = ± c / 2. Singularity of every three-vector Gram matrix in the plane forces each triple product ⟪u i, u j⟫ ⟪u i, u k⟫ ⟪u j, u k⟫ to equal -c ^ 3 / 8, and then the explicit combination `c • u₁ - 2 ⟪u₁, u₂⟫ • u₂

• 2 ⟪u₁, u₃⟫ • u₃ - 2 ⟪u₁, u₄⟫ • u₄has squared length-2 * c ^ 3 < 0`.

This is the five-point Gram obstruction in its scale-free form.

theorem Erdos132ThreeChain.dot_sq_of_chain {O P Q : Point} {c : ℝ} (hP : sqDist P O = c) (hQ : sqDist Q O = c) (h : sqDist P Q = c ∨ sqDist P Q = 3 * c) : dotp O P Q ^ 2 = c ^ 2 / 4

Two points on the circle of squared radius c about o, at squared distance c or 3 * c, subtend an inner product of ± c / 2.

theorem Erdos132ThreeChain.dot_triple_prod {O P Q R : Point} {c : ℝ} (hP : sqDist P O = c) (hQ : sqDist Q O = c) (hR : sqDist R O = c) (hpq : dotp O P Q ^ 2 = c ^ 2 / 4) (hpr : dotp O P R ^ 2 = c ^ 2 / 4) (hqr : dotp O Q R ^ 2 = c ^ 2 / 4) : dotp O P Q * dotp O P R * dotp O Q R = -(c ^ 3 / 8)

Singularity of the three-vector Gram matrix pins the triple product of the three inner products.

theorem Erdos132ThreeChain.no_four_on_circle {O P Q R S : Point} {c : ℝ} (hc : 0 < c) (hP : sqDist P O = c) (hQ : sqDist Q O = c) (hR : sqDist R O = c) (hS : sqDist S O = c) (hPQ : sqDist P Q = c ∨ sqDist P Q = 3 * c) (hPR : sqDist P R = c ∨ sqDist P R = 3 * c) (hPS : sqDist P S = c ∨ sqDist P S = 3 * c) (hQR : sqDist Q R = c ∨ sqDist Q R = 3 * c) (hQS : sqDist Q S = c ∨ sqDist Q S = 3 * c) (hRS : sqDist R S = c ∨ sqDist R S = 3 * c) : False

No four points on a circle. Four points at squared distance c > 0 from a common centre cannot have all six pairwise squared distances in {c, 3 * c}.

theorem Erdos132ThreeChain.no_five_chain_points {A B C D E : Point} {c : ℝ} (hc : 0 < c) (hAB : sqDist A B = c) (hAC : IsChainValue c (sqDist A C)) (hAD : IsChainValue c (sqDist A D)) (hAE : IsChainValue c (sqDist A E)) (hBC : IsChainValue c (sqDist B C)) (hBD : IsChainValue c (sqDist B D)) (hBE : IsChainValue c (sqDist B E)) (hCD : IsChainValue c (sqDist C D)) (hCE : IsChainValue c (sqDist C E)) (hDE : IsChainValue c (sqDist D E)) : False

The five-point obstruction. Five plane points whose ten squared distances are all c times a nonnegative power of three, with c realised by the edge A B, do not exist. Since IsChainValue c x forces c ≤ x, the hypothesis sqDist A B = c says exactly that A B is a shortest edge.