From five labelled points to five-element sets

no_five_chain_points is stated for five named points with a named shortest edge. This file removes both conveniences: no_five_chain_finset takes any five-element set of plane points whose pairwise squared distances lie in a geometric 3-chain, selects a shortest edge inside it, and rescales the chain so that the shortest edge has squared length exactly the new base.

theorem Erdos132ThreeChain.isChainValue_of_le {a c x : ℝ} (ha : 0 < a) {j₀ j : ℕ} (hc : c = a * 3 ^ j₀) (hx : x = a * 3 ^ j) (hle : c ≤ x) : IsChainValue c x

theorem Erdos132ThreeChain.exists_min_edge {S : Finset Point} {a : ℝ} (ha : 0 < a) (hcard : 2 ≤ S.card) (hch : ∀ p ∈ S, ∀ q ∈ S, p ≠ q → ∃ (j : ℕ), sqDist p q = a * 3 ^ j) : ∃ A ∈ S, ∃ B ∈ S, A ≠ B ∧ ∀ p ∈ S, ∀ q ∈ S, p ≠ q → IsChainValue (sqDist A B) (sqDist p q)

Inside a set whose pairwise squared distances lie in a geometric 3-chain, a shortest edge rescales the chain: every squared distance is the shortest one times a power of three.

theorem Erdos132ThreeChain.four_chain_adjacent {S : Finset Point} {a : ℝ} (ha : 0 < a) (hcard : S.card = 4) (hch : ∀ p ∈ S, ∀ q ∈ S, p ≠ q → ∃ (j : ℕ), sqDist p q = a * 3 ^ j) : ∃ (r : ℝ), 0 < r ∧ (∃ (j : ℕ), r = a * 3 ^ j) ∧ ∀ p ∈ S, ∀ q ∈ S, p ≠ q → sqDist p q = r ∨ sqDist p q = 3 * r

The chain-quadruple theorem. No planar chain quadruple spans two chain steps: if the six pairwise squared distances of a four-element set of plane points lie in a geometric 3-chain with positive base, then they all lie in a single adjacent pair {r, 3 * r} of that chain, and r is itself a member of the chain.

theorem Erdos132ThreeChain.no_five_chain_finset {S : Finset Point} {a : ℝ} (ha : 0 < a) (hcard : S.card = 5) (hch : ∀ p ∈ S, ∀ q ∈ S, p ≠ q → ∃ (j : ℕ), sqDist p q = a * 3 ^ j) : False

The five-point obstruction for five-element sets. No five-element set of plane points has all ten of its pairwise squared distances inside a geometric 3-chain with positive base.