Planar squared distances and geometric 3-chains

This file sets up the elementary objects used throughout the project: points of the Euclidean plane together with their squared distance, squared diameters and non-diameter distance supports, and the geometric 3-chain

L h a = {a, 3a, 9a, …, 3 ^ (h - 1) * a}

that the main theorem forbids as a non-diameter distance support.

Everything is deliberately self-contained and coordinate-based: Point is ℝ × ℝ and sqDist is the explicit sum of two squares, so that every planarity identity used later (Heron, the anchored Gram determinant) is provable by ring from coordinates.

@[reducible, inline]

abbrev Erdos132ThreeChain.Point : Type

A point of the Euclidean plane.

Equations

• Erdos132ThreeChain.Point = (ℝ × ℝ)

def Erdos132ThreeChain.sqDist (p q : Point) : ℝ

The squared Euclidean distance between two points of the plane.

Equations

• Erdos132ThreeChain.sqDist p q = (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2

@[simp]

theorem Erdos132ThreeChain.sqDist_self (p : Point) : sqDist p p = 0

theorem Erdos132ThreeChain.sqDist_comm (p q : Point) : sqDist p q = sqDist q p

theorem Erdos132ThreeChain.sqDist_nonneg (p q : Point) : 0 ≤ sqDist p q

theorem Erdos132ThreeChain.sqDist_eq_zero_iff {p q : Point} : sqDist p q = 0 ↔ p = q

theorem Erdos132ThreeChain.sqDist_pos {p q : Point} (h : p ≠ q) : 0 < sqDist p q

def Erdos132ThreeChain.IsSqDiameter (X : Finset Point) (D : ℝ) : Prop

IsSqDiameter X D says that D is the squared diameter of X: it is realised by two distinct points of X, and it dominates every squared distance inside X.

Equations

• Erdos132ThreeChain.IsSqDiameter X D = ((∃ p ∈ X, ∃ q ∈ X, p ≠ q ∧ Erdos132ThreeChain.sqDist p q = D) ∧ ∀ p ∈ X, ∀ q ∈ X, Erdos132ThreeChain.sqDist p q ≤ D)

def Erdos132ThreeChain.chain (a : ℝ) (h : ℕ) : Set ℝ

The geometric 3-chain of length h and base a: the set {a * 3 ^ j | j < h}.

Equations

• Erdos132ThreeChain.chain a h = {x : ℝ | ∃ j < h, x = a * 3 ^ j}

theorem Erdos132ThreeChain.mem_chain_iff {a x : ℝ} {h : ℕ} : x ∈ chain a h ↔ ∃ j < h, x = a * 3 ^ j

theorem Erdos132ThreeChain.base_mem_chain {a : ℝ} {h : ℕ} (hh : 0 < h) : a ∈ chain a h

theorem Erdos132ThreeChain.triple_base_mem_chain {a : ℝ} {h : ℕ} (hh : 2 ≤ h) : a * 3 ∈ chain a h

def Erdos132ThreeChain.nonDiameterSqDists (X : Finset Point) (D : ℝ) : Set ℝ

The set of squared distances realised by distinct points of X that are not the squared diameter D.

Equations

• Erdos132ThreeChain.nonDiameterSqDists X D = {d : ℝ | ∃ p ∈ X, ∃ q ∈ X, p ≠ q ∧ Erdos132ThreeChain.sqDist p q = d ∧ d ≠ D}

def Erdos132ThreeChain.IsChainValue (c x : ℝ) : Prop

IsChainValue c x records that x is c times a nonnegative power of three. It is the scale-free shadow of chain: if c is the smallest value of a chain that x belongs to, then x = c * 3 ^ j for some j : ℕ.

Equations

• Erdos132ThreeChain.IsChainValue c x = ∃ (j : ℕ), x = c * 3 ^ j

theorem Erdos132ThreeChain.IsChainValue.pos {c x : ℝ} (hc : 0 < c) (h : IsChainValue c x) : 0 < x