Witnesses for the chain configurations

The four-point catalogue is not vacuous: rhombus_chain_config and centroid_chain_config exhibit the two planar patterns of the chain-quadruple theorem — the rhombus made of two equilateral triangles glued along an edge (five short edges and one long one) and the equilateral triangle together with its centroid (three short edges and three long ones). Both have all six squared distances inside the adjacent pair {1, 3}.

theorem Erdos132ThreeChain.rhombus_chain_config : ∃ (A : Point) (B : Point) (C : Point) (D : Point), A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D ∧ sqDist A B = 1 ∧ sqDist A C = 1 ∧ sqDist A D = 1 ∧ sqDist B C = 1 ∧ sqDist B D = 1 ∧ sqDist C D = 3

The rhombus of two equilateral triangles glued along an edge: five squared distances equal 1 and one equals 3. This is the first pattern of the four-point catalogue, and it witnesses that the hypotheses of four_chain_adjacent are satisfiable.

theorem Erdos132ThreeChain.centroid_chain_config : ∃ (A : Point) (B : Point) (C : Point) (D : Point), A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D ∧ sqDist A B = 1 ∧ sqDist A C = 1 ∧ sqDist A D = 1 ∧ sqDist B C = 3 ∧ sqDist B D = 3 ∧ sqDist C D = 3

The equilateral triangle together with its centroid: three squared distances equal 1 and three equal 3. This is the second pattern of the four-point catalogue.

theorem Erdos132ThreeChain.chainTwo_config : ∃ (A : Point) (B : Point) (C : Point) (E : Point) (F : Point), A ≠ B ∧ A ≠ C ∧ A ≠ E ∧ A ≠ F ∧ B ≠ C ∧ B ≠ E ∧ B ≠ F ∧ C ≠ E ∧ C ≠ F ∧ E ≠ F ∧ sqDist A B = 1 ∧ sqDist A C = 1 ∧ sqDist A E = 1 ∧ sqDist A F = 3 ∧ sqDist B C = 3 ∧ sqDist B E = 1 ∧ sqDist B F = 4 ∧ sqDist C E = 1 ∧ sqDist C F = 1 ∧ sqDist E F = 1

Five points of the plane whose squared distances are 1, 3 and 4: the rhombus of two glued equilateral triangles together with the reflection of one vertex. Its squared diameter is 4, realised once, and both 1 and 3 occur as non-diameter squared distances.

theorem Erdos132ThreeChain.chainTwo_nonDiameter_support : ∃ (X : Finset Point), X.card = 5 ∧ IsSqDiameter X 4 ∧ nonDiameterSqDists X 4 = chain 1 2

A witness at chain length two. There is a five-point set of the plane whose squared diameter is 4 and whose set of non-diameter squared distances is exactly the two-term geometric 3-chain chain 1 2 = {1, 3}. Thus the configuration that nonDiameterSqDists_ne_chain forbids once n ≥ 13 is realisable at n = 5 with h = 2, so the headline is not vacuous in its own h ≥ 2 regime.