The four-point catalogue relative to a shortest edge

Fix four plane points A, B, C, D whose six squared distances are all of the form c * 3 ^ e with e : ℕ, where c = sqDist A B is the smallest of the six. This file classifies every such configuration.

classify_point uses only the triangle inequality: relative to the shortest edge A B, a further point P is either isoceles, with sqDist A P = sqDist B P, or spanning, with {sqDist A P, sqDist B P} = {c, 3 * c}.

The pair_* lemmas then feed the anchored Gram determinant, which must vanish for coplanar points, into the arithmetic of PowerThree. The outcome is that the two further points are never both spanning in opposite senses, that every isoceles point has squared radius exactly c, and that their mutual squared distance is c or 3 * c. Consequently all six squared distances lie in the single adjacent pair {c, 3 * c}: no planar chain quadruple spans two steps of the chain.

theorem Erdos132ThreeChain.classify_point {A B P : Point} {c : ℝ} (hc : 0 < c) (hAB : sqDist A B = c) (hAP : IsChainValue c (sqDist A P)) (hBP : IsChainValue c (sqDist B P)) : (∃ (x : ℕ), sqDist A P = c * 3 ^ x ∧ sqDist B P = c * 3 ^ x) ∨ sqDist A P = c ∧ sqDist B P = 3 * c ∨ sqDist A P = 3 * c ∧ sqDist B P = c

Relative to a shortest edge A B, every further point is isoceles or spanning.

theorem Erdos132ThreeChain.gramDet_isoceles (c r s t : ℝ) : gramDet c r s r s t = -2 * c * (r ^ 2 + s ^ 2 + t ^ 2 - 2 * r * s - 2 * r * t - 2 * s * t + c * t)

theorem Erdos132ThreeChain.gramDet_mixed (c r t : ℝ) : gramDet c r c r (3 * c) t = -2 * c * ((r - t) ^ 2 - 3 * c * t + 3 * c ^ 2)

theorem Erdos132ThreeChain.gramDet_mixed' (c r t : ℝ) : gramDet c r (3 * c) r c t = -2 * c * ((r - t) ^ 2 - 3 * c * t + 3 * c ^ 2)

theorem Erdos132ThreeChain.gramDet_spanning (c t : ℝ) : gramDet c c c (3 * c) (3 * c) t = 2 * t * c * (3 * c - t)

theorem Erdos132ThreeChain.gramDet_spanning' (c t : ℝ) : gramDet c (3 * c) (3 * c) c c t = 2 * t * c * (3 * c - t)

theorem Erdos132ThreeChain.gramDet_opposite (c t : ℝ) : gramDet c c (3 * c) (3 * c) c t = -2 * c * (4 * c - t) * (7 * c - t)

theorem Erdos132ThreeChain.pair_isoceles_aux {A B C D : Point} {c : ℝ} (hc : 0 < c) {x y l : ℕ} (hxy : x ≤ y) (hAB : sqDist A B = c) (hAC : sqDist A C = c * 3 ^ x) (hBC : sqDist B C = c * 3 ^ x) (hAD : sqDist A D = c * 3 ^ y) (hBD : sqDist B D = c * 3 ^ y) (hCD : sqDist C D = c * 3 ^ l) : x = 0 ∧ y = 0 ∧ l = 1

Two isoceles points: the shortest edge and both isoceles radii are equal to c, and the two points are 3 * c apart. Auxiliary form, with the radii ordered.

theorem Erdos132ThreeChain.pair_isoceles {A B C D : Point} {c : ℝ} (hc : 0 < c) {x y l : ℕ} (hAB : sqDist A B = c) (hAC : sqDist A C = c * 3 ^ x) (hBC : sqDist B C = c * 3 ^ x) (hAD : sqDist A D = c * 3 ^ y) (hBD : sqDist B D = c * 3 ^ y) (hCD : sqDist C D = c * 3 ^ l) : x = 0 ∧ y = 0 ∧ l = 1

Two isoceles points relative to the shortest edge A B force both radii to equal c and their mutual squared distance to equal 3 * c.

theorem Erdos132ThreeChain.pair_mixed {A B C D : Point} {c : ℝ} (hc : 0 < c) {x l : ℕ} (hAB : sqDist A B = c) (hAC : sqDist A C = c * 3 ^ x) (hBC : sqDist B C = c * 3 ^ x) (hD : sqDist A D = c ∧ sqDist B D = 3 * c ∨ sqDist A D = 3 * c ∧ sqDist B D = c) (hCD : sqDist C D = c * 3 ^ l) : x = 0 ∧ l = 0

One isoceles point and one spanning point: the isoceles radius is c and the two points are c apart.

theorem Erdos132ThreeChain.pair_spanning {A B C D : Point} {c : ℝ} (hc : 0 < c) {l : ℕ} (hAB : sqDist A B = c) (hCD : sqDist C D = c * 3 ^ l) (h : sqDist A C = c ∧ sqDist B C = 3 * c ∧ sqDist A D = c ∧ sqDist B D = 3 * c ∨ sqDist A C = 3 * c ∧ sqDist B C = c ∧ sqDist A D = 3 * c ∧ sqDist B D = c) : l = 1

Two spanning points of the same sense are 3 * c apart.

theorem Erdos132ThreeChain.pair_opposite {A B C D : Point} {c : ℝ} (hc : 0 < c) {l : ℕ} (hAB : sqDist A B = c) (hCD : sqDist C D = c * 3 ^ l) (hAC : sqDist A C = c) (hBC : sqDist B C = 3 * c) (hAD : sqDist A D = 3 * c) (hBD : sqDist B D = c) : False

Two spanning points of opposite senses cannot both occur.

structure Erdos132ThreeChain.ChainPos (A B P : Point) (c : ℝ) : Prop

The position of a further point P relative to a shortest edge A B of squared length c: both squared distances lie in the adjacent pair {c, 3 * c}, and at least one of them is c.

• fromLeft : sqDist A P = c ∨ sqDist A P = 3 * c

  P is at squared distance c or 3 * c from A.

• fromRight : sqDist B P = c ∨ sqDist B P = 3 * c

  P is at squared distance c or 3 * c from B.

• nearEnd : sqDist A P = c ∨ sqDist B P = c

  At least one endpoint of the shortest edge is at squared distance exactly c from P.

inductive Erdos132ThreeChain.ChainPattern (A B C D : Point) (c : ℝ) : Prop

The seven labelled patterns a chain quadruple can take, once A B is a shortest edge of squared length c. Five of them carry a single long edge — the rhombus of two glued equilateral triangles, with the long edge in any position other than A B — and two carry a triangle of three long edges, the equilateral triangle together with its centroid, whose centroid must be A or B because A B is short. Dropping the choice of shortest edge these are the 6 + 4 = 10 labelled assignments per adjacent pair of the chain.

• longCD {A B C D : Point} {c : ℝ} : sqDist A C = c → sqDist B C = c → sqDist A D = c → sqDist B D = c → sqDist C D = 3 * c → ChainPattern A B C D c

  Rhombus whose single long edge is C D.

• longBD {A B C D : Point} {c : ℝ} : sqDist A C = c → sqDist B C = c → sqDist A D = c → sqDist B D = 3 * c → sqDist C D = c → ChainPattern A B C D c

  Rhombus whose single long edge is B D.

• longAD {A B C D : Point} {c : ℝ} : sqDist A C = c → sqDist B C = c → sqDist A D = 3 * c → sqDist B D = c → sqDist C D = c → ChainPattern A B C D c

  Rhombus whose single long edge is A D.

• longBC {A B C D : Point} {c : ℝ} : sqDist A C = c → sqDist B C = 3 * c → sqDist A D = c → sqDist B D = c → sqDist C D = c → ChainPattern A B C D c

  Rhombus whose single long edge is B C.

• longAC {A B C D : Point} {c : ℝ} : sqDist A C = 3 * c → sqDist B C = c → sqDist A D = c → sqDist B D = c → sqDist C D = c → ChainPattern A B C D c

  Rhombus whose single long edge is A C.

• centreA {A B C D : Point} {c : ℝ} : sqDist A C = c → sqDist B C = 3 * c → sqDist A D = c → sqDist B D = 3 * c → sqDist C D = 3 * c → ChainPattern A B C D c

  Equilateral triangle B C D of long edges with centroid A.

• centreB {A B C D : Point} {c : ℝ} : sqDist A C = 3 * c → sqDist B C = c → sqDist A D = 3 * c → sqDist B D = c → sqDist C D = 3 * c → ChainPattern A B C D c

  Equilateral triangle A C D of long edges with centroid B.

structure Erdos132ThreeChain.ChainQuadruple (A B C D : Point) (c : ℝ) : Prop

The conclusion of the four-point catalogue: everything the shortest edge A B forces on a chain quadruple A, B, C, D.

• posC : ChainPos A B C c

  C sits in the adjacent pair {c, 3 * c} relative to A B.

• posD : ChainPos A B D c

  D sits in the adjacent pair {c, 3 * c} relative to A B.

• distCD : sqDist C D = c ∨ sqDist C D = 3 * c

  C and D are c or 3 * c apart.

• sharedLeft : sqDist A C = c ∨ sqDist B D = c

  C and D never span A B in opposite senses, first half.

• sharedRight : sqDist B C = c ∨ sqDist A D = c

  C and D never span A B in opposite senses, second half.

• pattern : ChainPattern A B C D c

  The labelling is one of the seven patterns of the catalogue.

theorem Erdos132ThreeChain.pair_classification {A B C D : Point} {c : ℝ} (hc : 0 < c) (hAB : sqDist A B = c) (hAC : IsChainValue c (sqDist A C)) (hBC : IsChainValue c (sqDist B C)) (hAD : IsChainValue c (sqDist A D)) (hBD : IsChainValue c (sqDist B D)) (hCD : IsChainValue c (sqDist C D)) : ChainQuadruple A B C D c

The chain-quadruple theorem relative to a shortest edge. If the six squared distances of A, B, C, D are all c times a power of three, with c = sqDist A B the smallest, then all six lie in the adjacent pair {c, 3 * c}, the points C and D never span the edge A B in opposite senses, and the labelling is one of the seven patterns of ChainPattern.