diff --git a/LeanPool.lean b/LeanPool.lean index e42065ecb7..d7b037cb30 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -1020,6 +1020,17 @@ import LeanPool.Erdos132N14.HopfPannwitzGeometry import LeanPool.Erdos132N14.Main import LeanPool.Erdos132N14.PublishedInputs import LeanPool.Erdos132N14.RegularTridecagon +import LeanPool.Erdos132ThreeChain +import LeanPool.Erdos132ThreeChain.Basic +import LeanPool.Erdos132ThreeChain.CaroWei +import LeanPool.Erdos132ThreeChain.FivePoints +import LeanPool.Erdos132ThreeChain.FourPoints +import LeanPool.Erdos132ThreeChain.HopfPannwitz +import LeanPool.Erdos132ThreeChain.Plane +import LeanPool.Erdos132ThreeChain.PowerThree +import LeanPool.Erdos132ThreeChain.Statement +import LeanPool.Erdos132ThreeChain.Support +import LeanPool.Erdos132ThreeChain.Witnesses import LeanPool.Erdos137 import LeanPool.Erdos137.AxiomAudit import LeanPool.Erdos137.Base diff --git a/LeanPool/Erdos132ThreeChain.lean b/LeanPool/Erdos132ThreeChain.lean new file mode 100644 index 0000000000..d79852355e --- /dev/null +++ b/LeanPool/Erdos132ThreeChain.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.HopfPannwitz +import LeanPool.Erdos132ThreeChain.Statement +import LeanPool.Erdos132ThreeChain.Witnesses + +/-! +# Planar Point Sets Whose Non-Diameter Distances Form a Geometric 3-Chain + +Source: url:https://www.erdosproblems.com/132 +Authors: Egor Lyfar +Status: verified +Main declarations: `Erdos132ThreeChain.nonDiameterSqDists_ne_chain` +Tags: discrete-geometry, distance-geometry, erdos-problems +MSC: 52C10, 52C35, 05C69 +-/ diff --git a/LeanPool/Erdos132ThreeChain/Basic.lean b/LeanPool/Erdos132ThreeChain/Basic.lean new file mode 100644 index 0000000000..0bed03a21e --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Basic.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import Mathlib.Data.Real.Basic +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# 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. +-/ + +namespace Erdos132ThreeChain + +/-- A point of the Euclidean plane. -/ +abbrev Point : Type := ℝ × ℝ + +/-- The squared Euclidean distance between two points of the plane. -/ +def sqDist (p q : Point) : ℝ := (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 + +@[simp] +theorem sqDist_self (p : Point) : sqDist p p = 0 := by simp [sqDist] + +theorem sqDist_comm (p q : Point) : sqDist p q = sqDist q p := by + simp only [sqDist]; ring + +theorem sqDist_nonneg (p q : Point) : 0 ≤ sqDist p q := by + simp only [sqDist]; positivity + +theorem sqDist_eq_zero_iff {p q : Point} : sqDist p q = 0 ↔ p = q := by + simp only [sqDist] + refine ⟨fun h => ?_, fun h => by rw [h]; ring⟩ + have h1 : (p.1 - q.1) ^ 2 = 0 := by nlinarith [sq_nonneg (p.1 - q.1), sq_nonneg (p.2 - q.2)] + have h2 : (p.2 - q.2) ^ 2 = 0 := by nlinarith [sq_nonneg (p.1 - q.1), sq_nonneg (p.2 - q.2)] + have e1 : p.1 = q.1 := by + have := (pow_eq_zero_iff (n := 2) (by norm_num)).mp h1 + linarith + have e2 : p.2 = q.2 := by + have := (pow_eq_zero_iff (n := 2) (by norm_num)).mp h2 + linarith + exact Prod.ext e1 e2 + +theorem sqDist_pos {p q : Point} (h : p ≠ q) : 0 < sqDist p q := + lt_of_le_of_ne (sqDist_nonneg p q) fun hc => h (sqDist_eq_zero_iff.mp hc.symm) + +/-- `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`. -/ +def IsSqDiameter (X : Finset Point) (D : ℝ) : Prop := + (∃ p ∈ X, ∃ q ∈ X, p ≠ q ∧ sqDist p q = D) ∧ ∀ p ∈ X, ∀ q ∈ X, sqDist p q ≤ D + +/-- The geometric 3-chain of length `h` and base `a`: the set `{a * 3 ^ j | j < h}`. -/ +def chain (a : ℝ) (h : ℕ) : Set ℝ := {x : ℝ | ∃ j < h, x = a * 3 ^ j} + +theorem mem_chain_iff {a x : ℝ} {h : ℕ} : x ∈ chain a h ↔ ∃ j < h, x = a * 3 ^ j := Iff.rfl + +theorem base_mem_chain {a : ℝ} {h : ℕ} (hh : 0 < h) : a ∈ chain a h := + ⟨0, hh, by simp⟩ + +theorem triple_base_mem_chain {a : ℝ} {h : ℕ} (hh : 2 ≤ h) : a * 3 ∈ chain a h := + ⟨1, hh, by norm_num⟩ + +/-- The set of squared distances realised by distinct points of `X` that are not the squared +diameter `D`. -/ +def nonDiameterSqDists (X : Finset Point) (D : ℝ) : Set ℝ := + {d : ℝ | ∃ p ∈ X, ∃ q ∈ X, p ≠ q ∧ sqDist p q = d ∧ d ≠ D} + +/-- `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 : ℕ`. -/ +def IsChainValue (c x : ℝ) : Prop := ∃ j : ℕ, x = c * 3 ^ j + +theorem IsChainValue.pos {c x : ℝ} (hc : 0 < c) (h : IsChainValue c x) : 0 < x := by + obtain ⟨j, rfl⟩ := h + positivity + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/CaroWei.lean b/LeanPool/Erdos132ThreeChain/CaroWei.lean new file mode 100644 index 0000000000..d280ceb2e6 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/CaroWei.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import Mathlib.Data.Real.Basic +import Mathlib.Data.Finset.Max +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# The Caro--Wei independence bound + +`carowei` is the classical greedy/random-order bound: every finite graph has an independent set +of size at least `∑ v, 1 / (deg v + 1)`. It is proved here by the standard induction that +deletes the closed neighbourhood of a minimum-degree vertex. + +`exists_independent_five` specialises it to the shape the main theorem needs. The tangent-line +estimate `1 / (d + 1) ≥ (5 - d) / 9`, valid because `(d - 2) ^ 2 ≥ 0`, converts a degree-sum +bound into a lower bound on the independence number, and integrality upgrades `n / 3 > 4` to an +independent set of size `5` once `n ≥ 13`. +-/ + +namespace Erdos132ThreeChain + +open Finset + +variable {α : Type*} + +/-- The degree of `v` in the graph that `adj` induces on the vertex set `V`. -/ +def degree (adj : α → α → Prop) [DecidableRel adj] (V : Finset α) (v : α) : ℕ := + (V.filter (adj v)).card + +theorem degree_mono {adj : α → α → Prop} [DecidableRel adj] {V W : Finset α} (h : W ⊆ V) + (v : α) : degree adj W v ≤ degree adj V v := + Finset.card_le_card (Finset.filter_subset_filter _ h) + +/-- **Caro--Wei.** Every finite graph has an independent set of size at least the sum over its +vertices of the reciprocal of one more than the degree. -/ +theorem carowei (adj : α → α → Prop) [DecidableRel adj] (hsymm : ∀ a b, adj a b → adj b a) + (hirr : ∀ a, ¬ adj a a) (V : Finset α) : + ∃ S ⊆ V, (∀ p ∈ S, ∀ q ∈ S, ¬ adj p q) ∧ + ∑ v ∈ V, (1 : ℝ) / (degree adj V v + 1) ≤ S.card := by + classical + induction V using Finset.strongInduction with + | _ V ih => + rcases V.eq_empty_or_nonempty with rfl | hne + · exact ⟨∅, by simp, by simp, by simp⟩ + obtain ⟨v, hv, hmin⟩ := Finset.exists_min_image V (degree adj V) hne + set N : Finset α := V.filter (adj v) with hN + have hvN : v ∉ N := by simp [hN, hirr v] + set NV : Finset α := insert v N with hNV + have hNVsub : NV ⊆ V := by + intro x hx + rcases Finset.mem_insert.mp hx with rfl | hx + · exact hv + · exact (Finset.mem_filter.mp hx).1 + set W : Finset α := V \ NV with hW + have hWsub : W ⊆ V := Finset.sdiff_subset + have hvW : v ∉ W := by simp [hW, hNV] + have hWlt : W ⊂ V := ⟨hWsub, fun hc => hvW (hc hv)⟩ + obtain ⟨S', hS'W, hS'ind, hS'card⟩ := ih W hWlt + have hvS' : v ∉ S' := fun hc => hvW (hS'W hc) + refine ⟨insert v S', ?_, ?_, ?_⟩ + · intro x hx + rcases Finset.mem_insert.mp hx with rfl | hx + · exact hv + · exact hWsub (hS'W hx) + · intro p hp q hq + have hnadj : ∀ u ∈ S', ¬ adj v u := by + intro u hu hadj + exact (Finset.mem_sdiff.mp (hS'W hu)).2 + (Finset.mem_insert_of_mem (Finset.mem_filter.mpr ⟨hWsub (hS'W hu), hadj⟩)) + rcases Finset.mem_insert.mp hp with hp' | hp' + · rcases Finset.mem_insert.mp hq with hq' | hq' + · rw [hp', hq']; exact hirr v + · rw [hp']; exact hnadj q hq' + · rcases Finset.mem_insert.mp hq with hq' | hq' + · rw [hq']; exact fun hadj => hnadj p hp' (hsymm _ _ hadj) + · exact hS'ind p hp' q hq' + · have hcard : ((insert v S').card : ℝ) = (S'.card : ℝ) + 1 := by + rw [Finset.card_insert_of_notMem hvS', Nat.cast_add, Nat.cast_one] + rw [hcard] + have hsplit : ∑ u ∈ W, (1 : ℝ) / (degree adj V u + 1) + + ∑ u ∈ NV, (1 : ℝ) / (degree adj V u + 1) + = ∑ u ∈ V, (1 : ℝ) / (degree adj V u + 1) := Finset.sum_sdiff hNVsub + have hhead : ∑ u ∈ NV, (1 : ℝ) / (degree adj V u + 1) ≤ 1 := by + have hbound : ∀ u ∈ NV, (1 : ℝ) / (degree adj V u + 1) + ≤ 1 / (degree adj V v + 1) := by + intro u hu + have := hmin u (hNVsub hu) + apply one_div_le_one_div_of_le (by positivity) + exact_mod_cast Nat.add_le_add_right this 1 + calc ∑ u ∈ NV, (1 : ℝ) / (degree adj V u + 1) + ≤ NV.card • ((1 : ℝ) / (degree adj V v + 1)) := + Finset.sum_le_card_nsmul _ _ _ hbound + _ = 1 := by + rw [hNV, Finset.card_insert_of_notMem hvN, nsmul_eq_mul] + have : degree adj V v = N.card := rfl + rw [this] + push_cast + field_simp + have htail : ∑ u ∈ W, (1 : ℝ) / (degree adj V u + 1) + ≤ ∑ u ∈ W, (1 : ℝ) / (degree adj W u + 1) := by + refine Finset.sum_le_sum fun u _ => ?_ + apply one_div_le_one_div_of_le (by positivity) + exact_mod_cast Nat.add_le_add_right (degree_mono hWsub u) 1 + linarith [hsplit, hhead, htail, hS'card] + + +/-- A graph on at least thirteen vertices whose degrees sum to at most twice the number of +vertices has an independent set of five vertices. The degree sum is twice the number of edges, +so the hypothesis is the edge bound `#edges ≤ #vertices`. -/ +theorem exists_independent_five (adj : α → α → Prop) [DecidableRel adj] + (hsymm : ∀ a b, adj a b → adj b a) (hirr : ∀ a, ¬ adj a a) (V : Finset α) + (hcard : 13 ≤ V.card) (hdeg : ∑ v ∈ V, degree adj V v ≤ 2 * V.card) : + ∃ S ⊆ V, S.card = 5 ∧ ∀ p ∈ S, ∀ q ∈ S, ¬ adj p q := by + obtain ⟨T, hTV, hTind, hTcard⟩ := carowei adj hsymm hirr V + have hterm : ∀ v ∈ V, (5 - (degree adj V v : ℝ)) / 9 ≤ 1 / ((degree adj V v : ℝ) + 1) := by + intro v _ + have hd : (0 : ℝ) ≤ (degree adj V v : ℝ) := Nat.cast_nonneg _ + have hpos : (0 : ℝ) < (degree adj V v : ℝ) + 1 := by linarith + have key : 1 / ((degree adj V v : ℝ) + 1) - (5 - (degree adj V v : ℝ)) / 9 + = ((degree adj V v : ℝ) - 2) ^ 2 / (9 * ((degree adj V v : ℝ) + 1)) := by + field_simp; ring + have hnn : (0 : ℝ) ≤ ((degree adj V v : ℝ) - 2) ^ 2 / (9 * ((degree adj V v : ℝ) + 1)) := by + positivity + rw [← key] at hnn + linarith + have hsum : ∑ v ∈ V, (5 - (degree adj V v : ℝ)) / 9 + = (5 * (V.card : ℝ) - ((∑ v ∈ V, degree adj V v : ℕ) : ℝ)) / 9 := by + rw [← Finset.sum_div, Finset.sum_sub_distrib, Finset.sum_const, nsmul_eq_mul, Nat.cast_sum] + ring + have hdegR : ((∑ v ∈ V, degree adj V v : ℕ) : ℝ) ≤ 2 * (V.card : ℝ) := by exact_mod_cast hdeg + have hcardR : (13 : ℝ) ≤ (V.card : ℝ) := by exact_mod_cast hcard + have hT5 : 5 ≤ T.card := by + by_contra hcon + rw [Nat.not_le] at hcon + have hle : (T.card : ℝ) ≤ 4 := by exact_mod_cast Nat.lt_succ_iff.mp hcon + have h1 := Finset.sum_le_sum hterm + rw [hsum] at h1 + linarith + obtain ⟨S, hST, hScard⟩ := Finset.exists_subset_card_eq hT5 + exact ⟨S, hST.trans hTV, hScard, fun p hp q hq => hTind p (hST hp) q (hST hq)⟩ + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/FivePoints.lean b/LeanPool/Erdos132ThreeChain/FivePoints.lean new file mode 100644 index 0000000000..def828b378 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/FivePoints.lean @@ -0,0 +1,123 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.FourPoints + +/-! +# 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. +-/ + +namespace Erdos132ThreeChain + +/-- 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 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 := by + have hd := two_mul_dotp O P Q + rw [hP, hQ] at hd + rcases h with h | h <;> rw [h] at hd + · have : dotp O P Q = c / 2 := by linarith + rw [this]; ring + · have : dotp O P Q = -(c / 2) := by linarith + rw [this]; ring + +/-- Singularity of the three-vector Gram matrix pins the triple product of the three inner +products. -/ +theorem 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) := by + have hg := gram3_det_eq_zero O P Q R + rw [dotp_self, dotp_self, dotp_self, hP, hQ, hR] at hg + linear_combination (1 / 2) * hg + (c / 2) * hpq + (c / 2) * hpr + (c / 2) * hqr + +/-- **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 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 := by + have spq := dot_sq_of_chain hP hQ hPQ + have spr := dot_sq_of_chain hP hR hPR + have sps := dot_sq_of_chain hP hS hPS + have sqr := dot_sq_of_chain hQ hR hQR + have sqs := dot_sq_of_chain hQ hS hQS + have srs := dot_sq_of_chain hR hS hRS + have tPQR := dot_triple_prod hP hQ hR spq spr sqr + have tPQS := dot_triple_prod hP hQ hS spq sps sqs + have tPRS := dot_triple_prod hP hR hS spr sps srs + have hkey := sq_nonneg_combo O P Q R S c (-2 * dotp O P Q) (-2 * dotp O P R) (-2 * dotp O P S) + rw [dotp_self, dotp_self, dotp_self, dotp_self, hP, hQ, hR, hS] at hkey + have hval : c ^ 2 * c + (-2 * dotp O P Q) ^ 2 * c + (-2 * dotp O P R) ^ 2 * c + + (-2 * dotp O P S) ^ 2 * c + + 2 * (c * (-2 * dotp O P Q) * dotp O P Q + c * (-2 * dotp O P R) * dotp O P R + + c * (-2 * dotp O P S) * dotp O P S + + (-2 * dotp O P Q) * (-2 * dotp O P R) * dotp O Q R + + (-2 * dotp O P Q) * (-2 * dotp O P S) * dotp O Q S + + (-2 * dotp O P R) * (-2 * dotp O P S) * dotp O R S) = -2 * c ^ 3 := by + linear_combination 8 * tPQR + 8 * tPQS + 8 * tPRS + rw [hval] at hkey + have hc3 : (0 : ℝ) < c ^ 3 := by positivity + linarith + + +/-- **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. -/ +theorem 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 := by + have hne : (3 : ℝ) * c ≠ c := by intro h; linarith + have qCD := pair_classification hc hAB hAC hBC hAD hBD hCD + have qCE := pair_classification hc hAB hAC hBC hAE hBE hCE + have qDE := pair_classification hc hAB hAD hBD hAE hBE hDE + have posC := qCD.posC + have posD := qCD.posD + have posE := qCE.posD + have centreB : sqDist B C = c → sqDist B D = c → sqDist B E = c → False := by + intro hbc hbd hbe + exact no_four_on_circle hc hAB (by rw [sqDist_comm C B]; exact hbc) + (by rw [sqDist_comm D B]; exact hbd) (by rw [sqDist_comm E B]; exact hbe) + posC.fromLeft posD.fromLeft posE.fromLeft qCD.distCD qCE.distCD qDE.distCD + rcases posC.fromLeft with hac | hac + · rcases posD.fromLeft with had | had + · rcases posE.fromLeft with hae | hae + · exact no_four_on_circle hc (by rw [sqDist_comm B A]; exact hAB) + (by rw [sqDist_comm C A]; exact hac) (by rw [sqDist_comm D A]; exact had) + (by rw [sqDist_comm E A]; exact hae) posC.fromRight posD.fromRight posE.fromRight + qCD.distCD qCE.distCD qDE.distCD + · exact centreB (qCE.sharedRight.resolve_right (by rw [hae]; exact hne)) + (qDE.sharedRight.resolve_right (by rw [hae]; exact hne)) (posE.nearEnd.resolve_left (by + rw [hae]; exact hne)) + · exact centreB (qCD.sharedRight.resolve_right (by rw [had]; exact hne)) + (posD.nearEnd.resolve_left (by rw [had]; exact hne)) + (qDE.sharedLeft.resolve_left (by rw [had]; exact hne)) + · exact centreB (posC.nearEnd.resolve_left (by rw [hac]; exact hne)) + (qCD.sharedLeft.resolve_left (by rw [hac]; exact hne)) + (qCE.sharedLeft.resolve_left (by rw [hac]; exact hne)) + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/FourPoints.lean b/LeanPool/Erdos132ThreeChain/FourPoints.lean new file mode 100644 index 0000000000..4d989129d2 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/FourPoints.lean @@ -0,0 +1,336 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.Plane +import LeanPool.Erdos132ThreeChain.PowerThree + +/-! +# 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. +-/ + +namespace Erdos132ThreeChain + +/-- Relative to a shortest edge `A B`, every further point is isoceles or spanning. -/ +theorem 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) := by + obtain ⟨x, hx⟩ := hAP + obtain ⟨y, hy⟩ := hBP + rcases le_total x y with hxy | hxy + · have htri := sq_le_four_mul A B P + rw [hAB, hx, hy] at htri + have h' : (c * 3 ^ y - c * 3 ^ (0 : ℕ) - c * 3 ^ x) ^ 2 + ≤ 4 * (c * 3 ^ (0 : ℕ)) * (c * 3 ^ x) := by simpa using htri + rcases exp_tri hc (Nat.zero_le x) hxy h' with h | ⟨h1, h2⟩ + · exact Or.inl ⟨x, hx, by rw [hy, h]⟩ + · refine Or.inr (Or.inl ⟨by rw [hx, ← h1, pow_zero, mul_one], by rw [hy, h2]; ring⟩) + · have htri := sq_le_four_mul B A P + rw [sqDist_comm B A, hAB, hx, hy] at htri + have h' : (c * 3 ^ x - c * 3 ^ (0 : ℕ) - c * 3 ^ y) ^ 2 + ≤ 4 * (c * 3 ^ (0 : ℕ)) * (c * 3 ^ y) := by simpa using htri + rcases exp_tri hc (Nat.zero_le y) hxy h' with h | ⟨h1, h2⟩ + · exact Or.inl ⟨x, hx, by rw [hy, ← h]⟩ + · refine Or.inr (Or.inr ⟨by rw [hx, h2]; ring, by rw [hy, ← h1, pow_zero, mul_one]⟩) + +theorem 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) := by + simp only [gramDet]; ring + +theorem gramDet_mixed (c r t : ℝ) : + gramDet c r c r (3 * c) t = -2 * c * ((r - t) ^ 2 - 3 * c * t + 3 * c ^ 2) := by + simp only [gramDet]; ring + +theorem gramDet_mixed' (c r t : ℝ) : + gramDet c r (3 * c) r c t = -2 * c * ((r - t) ^ 2 - 3 * c * t + 3 * c ^ 2) := by + simp only [gramDet]; ring + +theorem gramDet_spanning (c t : ℝ) : + gramDet c c c (3 * c) (3 * c) t = 2 * t * c * (3 * c - t) := by + simp only [gramDet]; ring + +theorem gramDet_spanning' (c t : ℝ) : + gramDet c (3 * c) (3 * c) c c t = 2 * t * c * (3 * c - t) := by + simp only [gramDet]; ring + +theorem gramDet_opposite (c t : ℝ) : + gramDet c c (3 * c) (3 * c) c t = -2 * c * (4 * c - t) * (7 * c - t) := by + simp only [gramDet]; ring + + +/-- 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 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 := by + have hdet := gramDet_eq_zero A B C D + rw [hAB, hAC, hAD, hBC, hBD, hCD, gramDet_isoceles] at hdet + have hbr : (c * 3 ^ x) ^ 2 + (c * 3 ^ y) ^ 2 + (c * 3 ^ l) ^ 2 - 2 * (c * 3 ^ x) * (c * 3 ^ y) + - 2 * (c * 3 ^ x) * (c * 3 ^ l) - 2 * (c * 3 ^ y) * (c * 3 ^ l) + c * (c * 3 ^ l) = 0 := + (mul_eq_zero.mp hdet).resolve_left (by intro h; nlinarith) + have hkey : (c : ℝ) ^ 2 * ((3 : ℝ) ^ x * 3 ^ x + 3 ^ y * 3 ^ y + 3 ^ l * 3 ^ l + - 2 * (3 ^ x * 3 ^ y) - 2 * (3 ^ x * 3 ^ l) - 2 * (3 ^ y * 3 ^ l) + 3 ^ l) = 0 := by + linear_combination hbr + have hR : (3 : ℝ) ^ x * 3 ^ x + 3 ^ y * 3 ^ y + 3 ^ l * 3 ^ l - 2 * (3 ^ x * 3 ^ y) + - 2 * (3 ^ x * 3 ^ l) - 2 * (3 ^ y * 3 ^ l) + 3 ^ l = 0 := + (mul_eq_zero.mp hkey).resolve_left (by positivity) + have hZ : (3 : ℤ) ^ x * 3 ^ x + 3 ^ y * 3 ^ y + 3 ^ l * 3 ^ l - 2 * (3 ^ x * 3 ^ y) + - 2 * (3 ^ x * 3 ^ l) - 2 * (3 ^ y * 3 ^ l) + 3 ^ l = 0 := by + have hcast : (((3 : ℤ) ^ x * 3 ^ x + 3 ^ y * 3 ^ y + 3 ^ l * 3 ^ l - 2 * (3 ^ x * 3 ^ y) + - 2 * (3 ^ x * 3 ^ l) - 2 * (3 ^ y * 3 ^ l) + 3 ^ l : ℤ) : ℝ) = 0 := by + push_cast; linarith [hR] + exact_mod_cast hcast + have htri1 : (c * 3 ^ y - c * 3 ^ x - c * 3 ^ l) ^ 2 ≤ 4 * (c * 3 ^ x) * (c * 3 ^ l) := by + have h := sq_le_four_mul C A D + rwa [sqDist_comm C A, hAC, hAD, hCD] at h + have htri2 : (c * 3 ^ l - c * 3 ^ x - c * 3 ^ y) ^ 2 ≤ 4 * (c * 3 ^ x) * (c * 3 ^ y) := by + have h := sq_le_four_mul A C D + rwa [hAC, hAD, hCD] at h + have hcase : x = y ∨ (l = x ∧ y = x + 1) ∨ l = y := by + rcases le_total l x with hlx | hxl + · have h : (c * 3 ^ y - c * 3 ^ l - c * 3 ^ x) ^ 2 ≤ 4 * (c * 3 ^ l) * (c * 3 ^ x) := by + calc (c * 3 ^ y - c * 3 ^ l - c * 3 ^ x) ^ 2 + = (c * 3 ^ y - c * 3 ^ x - c * 3 ^ l) ^ 2 := by ring + _ ≤ 4 * (c * 3 ^ x) * (c * 3 ^ l) := htri1 + _ = 4 * (c * 3 ^ l) * (c * 3 ^ x) := by ring + rcases exp_tri hc hlx hxy h with h1 | ⟨h1, h2⟩ + · exact Or.inl (by omega) + · exact Or.inr (Or.inl ⟨by omega, by omega⟩) + · rcases le_total l y with hly | hyl + · rcases exp_tri hc hxl hly htri1 with h1 | ⟨h1, h2⟩ + · exact Or.inr (Or.inr (by omega)) + · exact Or.inr (Or.inl ⟨by omega, h2⟩) + · rcases exp_tri hc hxy hyl htri2 with h1 | ⟨h1, h2⟩ + · exact Or.inr (Or.inr h1) + · exact Or.inl h1 + exact isoceles_pair_solution hxy hcase hZ + +/-- 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 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 := by + rcases le_total x y with h | h + · exact pair_isoceles_aux hc h hAB hAC hBC hAD hBD hCD + · obtain ⟨hy0, hx0, hl1⟩ := + pair_isoceles_aux hc h hAB hAD hBD hAC hBC (by rw [sqDist_comm D C]; exact hCD) + exact ⟨hx0, hy0, hl1⟩ + +/-- One isoceles point and one spanning point: the isoceles radius is `c` and the two points +are `c` apart. -/ +theorem 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 := by + have hdet := gramDet_eq_zero A B C D + have hbr : (c * 3 ^ x - c * 3 ^ l) ^ 2 - 3 * c * (c * 3 ^ l) + 3 * c ^ 2 = 0 := by + rcases hD with ⟨h1, h2⟩ | ⟨h1, h2⟩ + · rw [hAB, hAC, h1, hBC, h2, hCD, gramDet_mixed] at hdet + exact (mul_eq_zero.mp hdet).resolve_left (by intro hz; nlinarith) + · rw [hAB, hAC, h1, hBC, h2, hCD, gramDet_mixed'] at hdet + exact (mul_eq_zero.mp hdet).resolve_left (by intro hz; nlinarith) + have hkey : (c : ℝ) ^ 2 * (((3 : ℝ) ^ x - 3 ^ l) ^ 2 - 3 * 3 ^ l + 3) = 0 := by + linear_combination hbr + have hR : ((3 : ℝ) ^ x - 3 ^ l) ^ 2 - 3 * 3 ^ l + 3 = 0 := + (mul_eq_zero.mp hkey).resolve_left (by positivity) + have hZ : ((3 : ℤ) ^ x - 3 ^ l) ^ 2 - 3 * 3 ^ l + 3 = 0 := by + have hcast : ((((3 : ℤ) ^ x - 3 ^ l) ^ 2 - 3 * 3 ^ l + 3 : ℤ) : ℝ) = 0 := by + push_cast; linarith [hR] + exact_mod_cast hcast + exact mixed_pair_solution hZ + +/-- Two spanning points of the same sense are `3 * c` apart. -/ +theorem 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 := by + have hcne : (c : ℝ) ≠ 0 := ne_of_gt hc + have hdet := gramDet_eq_zero A B C D + have hfac : 2 * (c * 3 ^ l) * c * (3 * c - c * 3 ^ l) = 0 := by + rcases h with ⟨h1, h2, h3, h4⟩ | ⟨h1, h2, h3, h4⟩ + · rwa [hAB, h1, h3, h2, h4, hCD, gramDet_spanning] at hdet + · rwa [hAB, h1, h3, h2, h4, hCD, gramDet_spanning'] at hdet + have hpos : (0 : ℝ) < 2 * (c * 3 ^ l) * c := by positivity + have hlin := (mul_eq_zero.mp hfac).resolve_left (ne_of_gt hpos) + have hT : (3 : ℝ) ^ l = 3 := by + have hz : c * (3 ^ l - 3) = 0 := by linear_combination -hlin + have := (mul_eq_zero.mp hz).resolve_left hcne + linarith + have hZ : (3 : ℤ) ^ l = 3 ^ 1 := by + have hcast : (((3 : ℤ) ^ l : ℤ) : ℝ) = (((3 : ℤ) ^ 1 : ℤ) : ℝ) := by + push_cast; linarith [hT] + exact_mod_cast hcast + exact pow3_inj hZ + +/-- Two spanning points of opposite senses cannot both occur. -/ +theorem 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 := by + have hcne : (c : ℝ) ≠ 0 := ne_of_gt hc + have hdet := gramDet_eq_zero A B C D + rw [hAB, hAC, hAD, hBC, hBD, hCD, gramDet_opposite] at hdet + have h2 : (-2 : ℝ) * c ≠ 0 := by intro hz; nlinarith + have hfac : (4 * c - c * 3 ^ l) * (7 * c - c * 3 ^ l) = 0 := by + rcases mul_eq_zero.mp hdet with hu | hu + · rcases mul_eq_zero.mp hu with hv | hv + · exact absurd hv h2 + · rw [hv]; ring + · rw [hu]; ring + rcases mul_eq_zero.mp hfac with hu | hu + · have hR : (3 : ℝ) ^ l = 4 := by + have hz : c * (3 ^ l - 4) = 0 := by linear_combination -hu + have := (mul_eq_zero.mp hz).resolve_left hcne + linarith + have hZ : (3 : ℤ) ^ l = 4 := by + have hcast : (((3 : ℤ) ^ l : ℤ) : ℝ) = ((4 : ℤ) : ℝ) := by push_cast; linarith [hR] + exact_mod_cast hcast + exact pow3_ne_four hZ + · have hR : (3 : ℝ) ^ l = 7 := by + have hz : c * (3 ^ l - 7) = 0 := by linear_combination -hu + have := (mul_eq_zero.mp hz).resolve_left hcne + linarith + have hZ : (3 : ℤ) ^ l = 7 := by + have hcast : (((3 : ℤ) ^ l : ℤ) : ℝ) = ((7 : ℤ) : ℝ) := by push_cast; linarith [hR] + exact_mod_cast hcast + exact pow3_ne_seven hZ + + +/-- 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`. -/ +structure ChainPos (A B P : Point) (c : ℝ) : Prop where + /-- `P` is at squared distance `c` or `3 * c` from `A`. -/ + fromLeft : sqDist A P = c ∨ sqDist A P = 3 * c + /-- `P` is at squared distance `c` or `3 * c` from `B`. -/ + fromRight : sqDist B P = c ∨ sqDist B P = 3 * c + /-- At least one endpoint of the shortest edge is at squared distance exactly `c` from `P`. -/ + nearEnd : sqDist A P = c ∨ sqDist B P = c + +/-- 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. -/ +inductive ChainPattern (A B C D : Point) (c : ℝ) : Prop + /-- Rhombus whose single long edge is `C D`. -/ + | longCD : 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 `B D`. -/ + | longBD : 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 `A D`. -/ + | longAD : 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 `B C`. -/ + | longBC : 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 `A C`. -/ + | longAC : 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 + /-- Equilateral triangle `B C D` of long edges with centroid `A`. -/ + | centreA : 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 `A C D` of long edges with centroid `B`. -/ + | centreB : 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 + +/-- The conclusion of the four-point catalogue: everything the shortest edge `A B` forces on a +chain quadruple `A`, `B`, `C`, `D`. -/ +structure ChainQuadruple (A B C D : Point) (c : ℝ) : Prop where + /-- `C` sits in the adjacent pair `{c, 3 * c}` relative to `A B`. -/ + posC : ChainPos A B C c + /-- `D` sits in the adjacent pair `{c, 3 * c}` relative to `A B`. -/ + posD : ChainPos A B D c + /-- `C` and `D` are `c` or `3 * c` apart. -/ + distCD : sqDist C D = c ∨ sqDist C D = 3 * c + /-- `C` and `D` never span `A B` in opposite senses, first half. -/ + sharedLeft : sqDist A C = c ∨ sqDist B D = c + /-- `C` and `D` never span `A B` in opposite senses, second half. -/ + sharedRight : sqDist B C = c ∨ sqDist A D = c + /-- The labelling is one of the seven patterns of the catalogue. -/ + pattern : ChainPattern 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`. -/ +theorem 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 := by + obtain ⟨l, hl⟩ := hCD + have hlDC : sqDist D C = c * 3 ^ l := by rw [sqDist_comm D C]; exact hl + have h1 : (c : ℝ) * 3 ^ (0 : ℕ) = c := by norm_num + have h3 : (c : ℝ) * 3 ^ (1 : ℕ) = 3 * c := by ring + rcases classify_point hc hAB hAC hBC with ⟨x, hx1, hx2⟩ | ⟨hc1, hc2⟩ | ⟨hc1, hc2⟩ <;> + rcases classify_point hc hAB hAD hBD with ⟨y, hy1, hy2⟩ | ⟨hd1, hd2⟩ | ⟨hd1, hd2⟩ + · obtain ⟨hx0, hy0, hl1⟩ := pair_isoceles hc hAB hx1 hx2 hy1 hy2 hl + subst hx0; subst hy0; subst hl1 + rw [h1] at hx1 hx2 hy1 hy2; rw [h3] at hl + exact ⟨⟨Or.inl hx1, Or.inl hx2, Or.inl hx1⟩, ⟨Or.inl hy1, Or.inl hy2, Or.inl hy1⟩, + Or.inr hl, Or.inl hx1, Or.inl hx2, .longCD hx1 hx2 hy1 hy2 hl⟩ + · obtain ⟨hx0, hl0⟩ := pair_mixed hc hAB hx1 hx2 (Or.inl ⟨hd1, hd2⟩) hl + subst hx0; subst hl0 + rw [h1] at hx1 hx2 hl + exact ⟨⟨Or.inl hx1, Or.inl hx2, Or.inl hx1⟩, ⟨Or.inl hd1, Or.inr hd2, Or.inl hd1⟩, + Or.inl hl, Or.inl hx1, Or.inl hx2, .longBD hx1 hx2 hd1 hd2 hl⟩ + · obtain ⟨hx0, hl0⟩ := pair_mixed hc hAB hx1 hx2 (Or.inr ⟨hd1, hd2⟩) hl + subst hx0; subst hl0 + rw [h1] at hx1 hx2 hl + exact ⟨⟨Or.inl hx1, Or.inl hx2, Or.inl hx1⟩, ⟨Or.inr hd1, Or.inl hd2, Or.inr hd2⟩, + Or.inl hl, Or.inl hx1, Or.inl hx2, .longAD hx1 hx2 hd1 hd2 hl⟩ + · obtain ⟨hy0, hl0⟩ := pair_mixed hc hAB hy1 hy2 (Or.inl ⟨hc1, hc2⟩) hlDC + subst hy0; subst hl0 + rw [h1] at hy1 hy2 hl + exact ⟨⟨Or.inl hc1, Or.inr hc2, Or.inl hc1⟩, ⟨Or.inl hy1, Or.inl hy2, Or.inl hy1⟩, + Or.inl hl, Or.inl hc1, Or.inr hy1, .longBC hc1 hc2 hy1 hy2 hl⟩ + · have hl1 := pair_spanning hc hAB hl (Or.inl ⟨hc1, hc2, hd1, hd2⟩) + subst hl1; rw [h3] at hl + exact ⟨⟨Or.inl hc1, Or.inr hc2, Or.inl hc1⟩, ⟨Or.inl hd1, Or.inr hd2, Or.inl hd1⟩, + Or.inr hl, Or.inl hc1, Or.inr hd1, .centreA hc1 hc2 hd1 hd2 hl⟩ + · exact absurd (pair_opposite hc hAB hl hc1 hc2 hd1 hd2) (by simp) + · obtain ⟨hy0, hl0⟩ := pair_mixed hc hAB hy1 hy2 (Or.inr ⟨hc1, hc2⟩) hlDC + subst hy0; subst hl0 + rw [h1] at hy1 hy2 hl + exact ⟨⟨Or.inr hc1, Or.inl hc2, Or.inr hc2⟩, ⟨Or.inl hy1, Or.inl hy2, Or.inl hy1⟩, + Or.inl hl, Or.inr hy2, Or.inl hc2, .longAC hc1 hc2 hy1 hy2 hl⟩ + · exact absurd (pair_opposite hc hAB hlDC hd1 hd2 hc1 hc2) (by simp) + · have hl1 := pair_spanning hc hAB hl (Or.inr ⟨hc1, hc2, hd1, hd2⟩) + subst hl1; rw [h3] at hl + exact ⟨⟨Or.inr hc1, Or.inl hc2, Or.inr hc2⟩, ⟨Or.inr hd1, Or.inl hd2, Or.inr hd2⟩, + Or.inr hl, Or.inr hd2, Or.inl hc2, .centreB hc1 hc2 hd1 hd2 hl⟩ + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean b/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean new file mode 100644 index 0000000000..ab46d78785 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean @@ -0,0 +1,303 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.Plane +import LeanPool.Erdos132ThreeChain.CaroWei + +/-! +# The Hopf--Pannwitz diameter bound + +Hopf and Pannwitz (1934): a set of `n` points of the plane realises its diameter at most `n` +times. This file proves the bound in the form the main theorem consumes, and in fact proves +slightly more: only *maximality* of `D` is used, never that `D` is attained. + +Nothing here is claimed as new. The same bound is already in the pool as +`LeanPool.Erdos132N14.diameterEdges_card_le`, proved by Perles charging over an injective map +from a linearly ordered index type into `ℂ` and stated as a bound on the cardinality of a +`Finset` of unordered pairs. This file reproves it over a `Finset (ℝ × ℝ)`, in squared +distances and handshake degree-sum form, because pool projects do not import one another; it is +a supporting lemma of this development rather than one of its results. + +The classical argument deletes a pendant vertex. If a point `v` has three points of `X` at +squared distance exactly `D`, then one of the three — the one lying angularly between the other +two, seen from `v` — has no other such partner, so it can be deleted and induction applies. + +The angular step is entirely algebraic here. Write `A`, `B`, `C` for the vectors from `v` to +the three points and let `X`, `Y`, `Z` be the cross products `A × B`, `B × C`, `A × C`. Cramer's +rule in the plane is the identity `Z • B = Y • A + X • C`, and comparing squared lengths turns +maximality of `D` into the strict inequality `Z < X + Y`. A partner `w` of the middle point +satisfies `⟪B, w - v⟫ = |w - v|² / 2` while `⟪A, w - v⟫` and `⟪C, w - v⟫` are at least that, so +pairing Cramer's identity with `w - v` forces `|w - v|² ≤ 0`, i.e. `w = v`. +-/ + +namespace Erdos132ThreeChain + +open Finset + +/-- Adjacency in the diameter graph: distinct points at squared distance exactly `D`. -/ +def DiameterAdj (D : ℝ) (p q : Point) : Prop := p ≠ q ∧ sqDist p q = D + +noncomputable instance decidableDiameterAdj (D : ℝ) : DecidableRel (DiameterAdj D) := fun _ _ => + inferInstanceAs (Decidable (_ ∧ _)) + +theorem diameterAdj_symm (D : ℝ) (p q : Point) : DiameterAdj D p q → DiameterAdj D q p := + fun h => ⟨h.1.symm, by rw [sqDist_comm q p]; exact h.2⟩ + +theorem diameterAdj_irrefl (D : ℝ) (p : Point) : ¬ DiameterAdj D p p := fun h => h.1 rfl + +theorem IsSqDiameter.pos {X : Finset Point} {D : ℝ} (h : IsSqDiameter X D) : 0 < D := by + obtain ⟨⟨p, _, q, _, hpq, rfl⟩, -⟩ := h + exact sqDist_pos hpq + +/-! ### The plane geometry -/ + +/-- The squared distance between two points expanded around a third. -/ +theorem sqDist_expand (v a w : Point) : + sqDist a w = sqDist v a + sqDist v w - 2 * dotp v a w := by + simp only [sqDist, dotp]; ring + +/-- Lagrange's identity in the plane. -/ +theorem dotp_sq_add_cross_sq (v a b : Point) : + dotp v a b ^ 2 + cross v a b ^ 2 = sqDist v a * sqDist v b := by + simp only [dotp, cross, sqDist]; ring + +/-- Cramer's rule in the plane, paired with a fourth point. -/ +theorem cross_dotp_identity (v a b c w : Point) : + cross v a c * dotp v b w = cross v b c * dotp v a w + cross v a b * dotp v c w := by + simp only [cross, dotp]; ring + +/-- Cramer's rule in the plane, in squared-length form. -/ +theorem cross_sq_identity (v a b c : Point) : + cross v a c ^ 2 * sqDist v b + = cross v b c ^ 2 * sqDist v a + cross v a b ^ 2 * sqDist v c + + 2 * (cross v b c * cross v a b) * dotp v a c := by + simp only [cross, dotp, sqDist]; ring + +/-- Two distinct points at squared distance `D` from `v`, no farther than `D` from each other, +are not collinear with `v`. -/ +theorem cross_ne_zero {v a b : Point} {D : ℝ} (hD : 0 < D) + (hva : sqDist v a = D) (hvb : sqDist v b = D) (hab : sqDist a b ≤ D) (hne : a ≠ b) : + cross v a b ≠ 0 := by + intro hzero + have hlag := dotp_sq_add_cross_sq v a b + rw [hzero, hva, hvb] at hlag + have hexp := sqDist_expand v a b + rw [hva, hvb] at hexp + have hpos : 0 < sqDist a b := sqDist_pos hne + nlinarith [hlag, hexp, hpos, hab, hD] + +/-- **The pendant lemma.** Let `a`, `b`, `c` sit at squared distance `D` from `v`, with `b` +strictly between `a` and `c` as seen from `v` (both cross products positive). If no squared +distance among the points involved exceeds `D`, then the only point at squared distance `D` +from `b` is `v` itself. -/ +theorem middle_no_other_neighbour {v a b c w : Point} {D : ℝ} (hD : 0 < D) + (hva : sqDist v a = D) (hvb : sqDist v b = D) (hvc : sqDist v c = D) (hac : a ≠ c) + (hX : 0 < cross v a b) (hY : 0 < cross v b c) + (hbw : sqDist b w = D) (haw : sqDist a w ≤ D) (hcw : sqDist c w ≤ D) : w = v := by + have hB : 2 * dotp v b w = sqDist v w := by + have h := sqDist_expand v b w + rw [hvb, hbw] at h + linarith + have hA : sqDist v w ≤ 2 * dotp v a w := by + have h := sqDist_expand v a w + rw [hva] at h + linarith + have hC : sqDist v w ≤ 2 * dotp v c w := by + have h := sqDist_expand v c w + rw [hvc] at h + linarith + have hdac : dotp v a c < D := by + have h := sqDist_expand v a c + rw [hva, hvc] at h + have := sqDist_pos hac + linarith + have hZ : cross v a c < cross v a b + cross v b c := by + have hid := cross_sq_identity v a b c + rw [hva, hvb, hvc] at hid + have hsq : cross v a c ^ 2 < (cross v a b + cross v b c) ^ 2 := by + nlinarith [hid, hdac, mul_pos hX hY, hD] + nlinarith [hsq, hX, hY] + have hid2 := cross_dotp_identity v a b c w + have h1 : 0 ≤ cross v b c * (2 * dotp v a w - sqDist v w) := + mul_nonneg hY.le (by linarith) + have h2 : 0 ≤ cross v a b * (2 * dotp v c w - sqDist v w) := + mul_nonneg hX.le (by linarith) + have hkey : (cross v a b + cross v b c - cross v a c) * sqDist v w ≤ 0 := by nlinarith [hid2, hB] + have hnn := sqDist_nonneg v w + have hzero : sqDist v w = 0 := by nlinarith [hkey, hZ, hnn] + exact (sqDist_eq_zero_iff.mp hzero).symm + +/-- Of three points seen from `v` with no two collinear with `v`, one lies strictly between the +other two. The six alternatives are the three choices of middle point, each in the two possible +orientations. -/ +theorem exists_middle (v a b c : Point) (hab : cross v a b ≠ 0) (hbc : cross v b c ≠ 0) + (hac : cross v a c ≠ 0) : + (0 < cross v a b ∧ 0 < cross v b c) ∨ (0 < cross v c b ∧ 0 < cross v b a) ∨ + (0 < cross v b a ∧ 0 < cross v a c) ∨ (0 < cross v c a ∧ 0 < cross v a b) ∨ + (0 < cross v a c ∧ 0 < cross v c b) ∨ (0 < cross v b c ∧ 0 < cross v c a) := by + have eba : cross v b a = -cross v a b := by simp only [cross]; ring + have ecb : cross v c b = -cross v b c := by simp only [cross]; ring + have eca : cross v c a = -cross v a c := by simp only [cross]; ring + rcases lt_or_gt_of_ne hab with h1 | h1 <;> rcases lt_or_gt_of_ne hbc with h2 | h2 <;> + rcases lt_or_gt_of_ne hac with h3 | h3 + · exact Or.inr (Or.inl ⟨by rw [ecb]; linarith, by rw [eba]; linarith⟩) + · exact Or.inr (Or.inl ⟨by rw [ecb]; linarith, by rw [eba]; linarith⟩) + · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨h2, by rw [eca]; linarith⟩)))) + · exact Or.inr (Or.inr (Or.inl ⟨by rw [eba]; linarith, h3⟩)) + · exact Or.inr (Or.inr (Or.inr (Or.inl ⟨by rw [eca]; linarith, h1⟩))) + · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨h3, by rw [ecb]; linarith⟩)))) + · exact Or.inl ⟨h1, h2⟩ + · exact Or.inl ⟨h1, h2⟩ + +/-- Three points at squared distance `D` from `v` inside a set of diameter `D` force one of the +three to have `v` as its only partner at squared distance `D`. -/ +theorem exists_pendant {X : Finset Point} {D : ℝ} (hD : 0 < D) + (hmax : ∀ p ∈ X, ∀ q ∈ X, sqDist p q ≤ D) + {v a b c : Point} (haX : a ∈ X) (hbX : b ∈ X) (hcX : c ∈ X) + (hva : sqDist v a = D) (hvb : sqDist v b = D) (hvc : sqDist v c = D) + (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : + (∀ w ∈ X, sqDist a w = D → w = v) ∨ (∀ w ∈ X, sqDist b w = D → w = v) + ∨ (∀ w ∈ X, sqDist c w = D → w = v) := by + have kab : cross v a b ≠ 0 := cross_ne_zero hD hva hvb (hmax a haX b hbX) hab + have kbc : cross v b c ≠ 0 := cross_ne_zero hD hvb hvc (hmax b hbX c hcX) hbc + have kac : cross v a c ≠ 0 := cross_ne_zero hD hva hvc (hmax a haX c hcX) hac + rcases exists_middle v a b c kab kbc kac with + ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ + · exact Or.inr (Or.inl fun w hw hbw => + middle_no_other_neighbour hD hva hvb hvc hac h1 h2 hbw (hmax a haX w hw) (hmax c hcX w hw)) + · exact Or.inr (Or.inl fun w hw hbw => + middle_no_other_neighbour hD hvc hvb hva hac.symm h1 h2 hbw (hmax c hcX w hw) + (hmax a haX w hw)) + · exact Or.inl fun w hw haw => + middle_no_other_neighbour hD hvb hva hvc hbc h1 h2 haw (hmax b hbX w hw) (hmax c hcX w hw) + · exact Or.inl fun w hw haw => + middle_no_other_neighbour hD hvc hva hvb hbc.symm h1 h2 haw (hmax c hcX w hw) + (hmax b hbX w hw) + · exact Or.inr (Or.inr fun w hw hcw => + middle_no_other_neighbour hD hva hvc hvb hab h1 h2 hcw (hmax a haX w hw) + (hmax b hbX w hw)) + · exact Or.inr (Or.inr fun w hw hcw => + middle_no_other_neighbour hD hvb hvc hva hab.symm h1 h2 hcw (hmax b hbX w hw) + (hmax a haX w hw)) + +/-! ### Counting -/ + +/-- Deleting a pendant vertex removes exactly one edge, i.e. two from the degree sum. -/ +theorem sum_degree_erase {X : Finset Point} {D : ℝ} {b v : Point} (hbX : b ∈ X) (hvX : v ∈ X) + (hbv : b ≠ v) (hstar : X.filter (DiameterAdj D b) = {v}) : + ∑ u ∈ X, degree (DiameterAdj D) X u + = (∑ u ∈ X.erase b, degree (DiameterAdj D) (X.erase b) u) + 2 := by + classical + have hdegb : degree (DiameterAdj D) X b = 1 := by + rw [degree, hstar, Finset.card_singleton] + have hstep : ∀ u ∈ X.erase b, degree (DiameterAdj D) X u + = degree (DiameterAdj D) (X.erase b) u + (if DiameterAdj D u b then 1 else 0) := by + intro u _ + have hfil : (X.erase b).filter (DiameterAdj D u) = (X.filter (DiameterAdj D u)).erase b := by + ext x + simp only [Finset.mem_filter, Finset.mem_erase] + tauto + by_cases h : DiameterAdj D u b + · have hif : (if DiameterAdj D u b then (1 : ℕ) else 0) = 1 := by simp [h] + have hmem : b ∈ X.filter (DiameterAdj D u) := Finset.mem_filter.mpr ⟨hbX, h⟩ + rw [hif, degree, degree, hfil, Finset.card_erase_add_one hmem] + · have hif : (if DiameterAdj D u b then (1 : ℕ) else 0) = 0 := by simp [h] + have hnot : b ∉ X.filter (DiameterAdj D u) := by + simp only [Finset.mem_filter] + exact fun hc => h hc.2 + rw [hif, degree, degree, hfil, Finset.erase_eq_of_notMem hnot, add_zero] + have hnbr : (X.erase b).filter (fun u => DiameterAdj D u b) = {v} := by + ext x + simp only [Finset.mem_filter, Finset.mem_erase, Finset.mem_singleton] + constructor + · rintro ⟨⟨hxb, hxX⟩, hadj⟩ + have : x ∈ X.filter (DiameterAdj D b) := + Finset.mem_filter.mpr ⟨hxX, diameterAdj_symm D x b hadj⟩ + rw [hstar] at this + exact Finset.mem_singleton.mp this + · rintro rfl + have hv : x ∈ X.filter (DiameterAdj D b) := by rw [hstar]; simp + exact ⟨⟨fun hc => hbv hc.symm, hvX⟩, diameterAdj_symm D b x (Finset.mem_filter.mp hv).2⟩ + calc ∑ u ∈ X, degree (DiameterAdj D) X u + = degree (DiameterAdj D) X b + ∑ u ∈ X.erase b, degree (DiameterAdj D) X u := + (Finset.add_sum_erase _ _ hbX).symm + _ = 1 + ∑ u ∈ X.erase b, (degree (DiameterAdj D) (X.erase b) u + + (if DiameterAdj D u b then 1 else 0)) := by + rw [hdegb, Finset.sum_congr rfl hstep] + _ = 1 + ((∑ u ∈ X.erase b, degree (DiameterAdj D) (X.erase b) u) + + ((X.erase b).filter (fun u => DiameterAdj D u b)).card) := by + rw [Finset.sum_add_distrib, Finset.sum_boole] + norm_cast + _ = (∑ u ∈ X.erase b, degree (DiameterAdj D) (X.erase b) u) + 2 := by + rw [hnbr, Finset.card_singleton]; omega + +/-- The induction step packaged: a pendant vertex `b` whose only partner is `v`. -/ +theorem sum_degree_le_of_pendant {X : Finset Point} {D : ℝ} {b v : Point} + (hbX : b ∈ X) (hvX : v ∈ X) (hbv : b ≠ v) (hvb : sqDist v b = D) + (hstar : ∀ w ∈ X, sqDist b w = D → w = v) + (ih : ∑ u ∈ X.erase b, degree (DiameterAdj D) (X.erase b) u ≤ 2 * (X.erase b).card) : + ∑ u ∈ X, degree (DiameterAdj D) X u ≤ 2 * X.card := by + classical + have hfil : X.filter (DiameterAdj D b) = {v} := by + ext x + simp only [Finset.mem_filter, Finset.mem_singleton] + constructor + · rintro ⟨hxX, hadj⟩ + exact hstar x hxX hadj.2 + · rintro rfl + exact ⟨hvX, hbv, by rw [sqDist_comm b x]; exact hvb⟩ + have hcard : (X.erase b).card = X.card - 1 := Finset.card_erase_of_mem hbX + have hpos : 1 ≤ X.card := Finset.card_pos.mpr ⟨b, hbX⟩ + rw [sum_degree_erase hbX hvX hbv hfil] + omega + +/-- **Hopf--Pannwitz.** If every squared distance inside `X` is at most `D > 0`, then the graph +joining points of `X` at squared distance exactly `D` has degree sum at most `2 * #X`, that is, +at most `#X` edges. -/ +theorem sum_degree_le {D : ℝ} (hD : 0 < D) (X : Finset Point) + (hmax : ∀ p ∈ X, ∀ q ∈ X, sqDist p q ≤ D) : + ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card := by + classical + induction X using Finset.strongInduction with + | _ X ih => + by_cases hdeg : ∀ v ∈ X, degree (DiameterAdj D) X v ≤ 2 + · calc ∑ v ∈ X, degree (DiameterAdj D) X v ≤ ∑ _v ∈ X, 2 := Finset.sum_le_sum hdeg + _ = 2 * X.card := by rw [Finset.sum_const, smul_eq_mul, mul_comm] + · rw [not_forall] at hdeg + obtain ⟨v, hdeg⟩ := hdeg + rw [Classical.not_imp] at hdeg + obtain ⟨hvX, hvdeg⟩ := hdeg + rw [not_le] at hvdeg + simp only [degree] at hvdeg + obtain ⟨T, hTsub, hTcard⟩ := + Finset.exists_subset_card_eq (n := 3) (s := X.filter (DiameterAdj D v)) (by omega) + obtain ⟨a, b, c, hab, hac, hbc, hTeq⟩ := Finset.card_eq_three.mp hTcard + have hmemT : ∀ x ∈ T, x ∈ X ∧ DiameterAdj D v x := by + intro x hx + exact Finset.mem_filter.mp (hTsub hx) + obtain ⟨haX, hvaAdj⟩ := hmemT a (by rw [hTeq]; simp) + obtain ⟨hbX, hvbAdj⟩ := hmemT b (by rw [hTeq]; simp) + obtain ⟨hcX, hvcAdj⟩ := hmemT c (by rw [hTeq]; simp) + have hsubX : ∀ x ∈ X, X.erase x ⊂ X := fun x hx => Finset.erase_ssubset hx + rcases exists_pendant hD hmax haX hbX hcX hvaAdj.2 hvbAdj.2 hvcAdj.2 hab hac hbc with + hp | hp | hp + · exact sum_degree_le_of_pendant haX hvX (Ne.symm hvaAdj.1) hvaAdj.2 hp + (ih _ (hsubX a haX) fun p hp' q hq' => + hmax p (Finset.mem_of_mem_erase hp') q (Finset.mem_of_mem_erase hq')) + · exact sum_degree_le_of_pendant hbX hvX (Ne.symm hvbAdj.1) hvbAdj.2 hp + (ih _ (hsubX b hbX) fun p hp' q hq' => + hmax p (Finset.mem_of_mem_erase hp') q (Finset.mem_of_mem_erase hq')) + · exact sum_degree_le_of_pendant hcX hvX (Ne.symm hvcAdj.1) hvcAdj.2 hp + (ih _ (hsubX c hcX) fun p hp' q hq' => + hmax p (Finset.mem_of_mem_erase hp') q (Finset.mem_of_mem_erase hq')) + +/-- **Hopf--Pannwitz for a diameter.** The diameter graph of a finite planar set has at most as +many edges as the set has points. -/ +theorem hopfPannwitz {X : Finset Point} {D : ℝ} (hD : IsSqDiameter X D) : + ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card := + sum_degree_le hD.pos X hD.2 + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/Plane.lean b/LeanPool/Erdos132ThreeChain/Plane.lean new file mode 100644 index 0000000000..a42ef141f2 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Plane.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.Basic + +/-! +# Planarity constraints on squared distances + +Three exact identities carry all of the geometry in this project. Each is a polynomial +identity in the coordinates of the points involved, so each is proved by `ring`. + +* `four_mul_mul_sub_sq_eq` is Heron's formula in squared-distance form. Its corollary + `sq_le_four_mul` is the triangle inequality written without square roots, and it is the + only inequality the classification of chain triangles needs. +* `gramDet_eq_zero` says that the doubled Gram matrix of three plane vectors anchored at a + fourth point is singular. Expressed in the six squared distances of four points this is the + Cayley--Menger relation, and it is the only equation the four-point catalogue needs. +* `gram3_det_eq_zero` is the same singularity written directly in inner products; together + with `sq_nonneg_combo` it supplies the five-point obstruction. +-/ + +namespace Erdos132ThreeChain + +/-- Twice the signed area of the triangle `p q r`; equivalently the two-dimensional cross +product of `q - p` and `r - p`. -/ +def cross (p q r : Point) : ℝ := (q.1 - p.1) * (r.2 - p.2) - (r.1 - p.1) * (q.2 - p.2) + +/-- Heron's formula in squared-distance form: the Cayley--Menger expression of a triangle is +four times the square of its doubled signed area. -/ +theorem four_mul_mul_sub_sq_eq (p q r : Point) : + 4 * sqDist p q * sqDist p r - (sqDist q r - sqDist p q - sqDist p r) ^ 2 + = 4 * cross p q r ^ 2 := by + simp only [sqDist, cross]; ring + +/-- The triangle inequality for three plane points, stated without square roots. -/ +theorem sq_le_four_mul (p q r : Point) : + (sqDist q r - sqDist p q - sqDist p r) ^ 2 ≤ 4 * sqDist p q * sqDist p r := by + have h := four_mul_mul_sub_sq_eq p q r + nlinarith [sq_nonneg (cross p q r)] + +/-- The inner product of `p - o` and `q - o`. -/ +def dotp (o p q : Point) : ℝ := (p.1 - o.1) * (q.1 - o.1) + (p.2 - o.2) * (q.2 - o.2) + +theorem dotp_self (o p : Point) : dotp o p p = sqDist p o := by + simp only [dotp, sqDist]; ring + +theorem two_mul_dotp (o p q : Point) : + 2 * dotp o p q = sqDist p o + sqDist q o - sqDist p q := by + simp only [dotp, sqDist]; ring + +/-- The determinant of the doubled Gram matrix of `b - a`, `c - a`, `d - a`, written in the six +squared distances of `a`, `b`, `c`, `d`. -/ +def gramDet (dab dac dad dbc dbd dcd : ℝ) : ℝ := + 2 * dab * (2 * dac * (2 * dad) - (dac + dad - dcd) ^ 2) + - (dab + dac - dbc) * ((dab + dac - dbc) * (2 * dad) + - (dac + dad - dcd) * (dab + dad - dbd)) + + (dab + dad - dbd) * ((dab + dac - dbc) * (dac + dad - dcd) + - 2 * dac * (dab + dad - dbd)) + +/-- Three vectors of the plane are linearly dependent, so the anchored Gram determinant of any +four plane points vanishes. This is the Cayley--Menger relation for four coplanar points. -/ +theorem gramDet_eq_zero (a b c d : Point) : + gramDet (sqDist a b) (sqDist a c) (sqDist a d) (sqDist b c) (sqDist b d) (sqDist c d) = 0 := by + simp only [gramDet, sqDist]; ring + +/-- The Gram determinant of three plane vectors vanishes. -/ +theorem gram3_det_eq_zero (o p q r : Point) : + dotp o p p * (dotp o q q * dotp o r r - dotp o q r ^ 2) + - dotp o p q * (dotp o p q * dotp o r r - dotp o q r * dotp o p r) + + dotp o p r * (dotp o p q * dotp o q r - dotp o q q * dotp o p r) = 0 := by + simp only [dotp]; ring + +/-- The squared length of a linear combination of four plane vectors is nonnegative, expanded +in inner products. -/ +theorem sq_nonneg_combo (o p q r s : Point) (x y z w : ℝ) : + 0 ≤ x ^ 2 * dotp o p p + y ^ 2 * dotp o q q + z ^ 2 * dotp o r r + w ^ 2 * dotp o s s + + 2 * (x * y * dotp o p q + x * z * dotp o p r + x * w * dotp o p s + + y * z * dotp o q r + y * w * dotp o q s + z * w * dotp o r s) := by + calc (0 : ℝ) + ≤ (x * (p.1 - o.1) + y * (q.1 - o.1) + z * (r.1 - o.1) + w * (s.1 - o.1)) ^ 2 + + (x * (p.2 - o.2) + y * (q.2 - o.2) + z * (r.2 - o.2) + w * (s.2 - o.2)) ^ 2 := by + positivity + _ = _ := by simp only [dotp]; ring + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/PowerThree.lean b/LeanPool/Erdos132ThreeChain/PowerThree.lean new file mode 100644 index 0000000000..3debbf3635 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/PowerThree.lean @@ -0,0 +1,179 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.Basic +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Ring +import Mathlib.Data.Int.GCD +import Mathlib.Tactic.LinearCombination + +/-! +# Arithmetic of powers of three + +The four-point catalogue reduces to a handful of Diophantine facts about powers of three. +This file isolates them. Everything is stated over `ℤ`; the geometric files produce the +corresponding real equations and transfer them by `exact_mod_cast`. +-/ + +namespace Erdos132ThreeChain + +theorem one_le_pow3 (n : ℕ) : (1 : ℤ) ≤ 3 ^ n := one_le_pow₀ (by norm_num) + +theorem pow3_pos (n : ℕ) : (0 : ℤ) < 3 ^ n := by positivity + +theorem three_le_pow3 {n : ℕ} (h : n ≠ 0) : (3 : ℤ) ≤ 3 ^ n := by + obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩ + have h3 : (3 : ℤ) ^ (m + 1) = 3 * 3 ^ m := by ring + nlinarith [one_le_pow3 m] + +theorem three_dvd_pow3 {n : ℕ} (h : n ≠ 0) : (3 : ℤ) ∣ 3 ^ n := by + obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩ + exact ⟨3 ^ m, by ring⟩ + +theorem nine_dvd_pow3 {n : ℕ} (h : 2 ≤ n) : (9 : ℤ) ∣ 3 ^ n := by + obtain ⟨m, rfl⟩ : ∃ m, n = m + 2 := ⟨n - 2, by omega⟩ + exact ⟨3 ^ m, by ring⟩ + +theorem pow3_inj {m n : ℕ} (h : (3 : ℤ) ^ m = 3 ^ n) : m = n := by + have : (3 : ℕ) ^ m = 3 ^ n := by exact_mod_cast h + exact Nat.pow_right_injective (by norm_num) this + +/-- A power of three is `1`, is `3`, or is at least `9`. -/ +theorem pow3_trichotomy (n : ℕ) : (3 : ℤ) ^ n = 1 ∨ (3 : ℤ) ^ n = 3 ∨ 9 ≤ (3 : ℤ) ^ n := by + match n with + | 0 => left; norm_num + | 1 => right; left; norm_num + | (m + 2) => + right; right + have h : (3 : ℤ) ^ (m + 2) = 9 * 3 ^ m := by ring + nlinarith [one_le_pow3 m] + +/-- `4 * 3 ^ j - 1` is a power of three only in the trivial instance `4 - 1 = 3`. -/ +theorem pow3_eq_four_mul_pow3_sub_one {j l : ℕ} (h : (3 : ℤ) ^ l = 4 * 3 ^ j - 1) : + j = 0 ∧ l = 1 := by + have hj : j = 0 := by + by_contra hj + obtain ⟨u, hu⟩ := three_dvd_pow3 hj + rcases eq_or_ne l 0 with hl | hl + · subst hl; rw [hu] at h; simp at h; omega + · obtain ⟨v, hv⟩ := three_dvd_pow3 hl + rw [hu, hv] at h; omega + subst hj + refine ⟨rfl, ?_⟩ + have h3 : (3 : ℤ) ^ l = 3 ^ 1 := by simpa using h + exact pow3_inj h3 + + +theorem one_le_pow3R (n : ℕ) : (1 : ℝ) ≤ 3 ^ n := one_le_pow₀ (by norm_num) + +theorem three_le_pow3R {n : ℕ} (h : n ≠ 0) : (3 : ℝ) ≤ 3 ^ n := by + obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩ + have e : (3 : ℝ) ^ (m + 1) = 3 * 3 ^ m := by ring + nlinarith [one_le_pow3R m] + +theorem nine_le_pow3R {n : ℕ} (h : 2 ≤ n) : (9 : ℝ) ≤ 3 ^ n := by + obtain ⟨m, rfl⟩ : ∃ m, n = m + 2 := ⟨n - 2, by omega⟩ + have e : (3 : ℝ) ^ (m + 2) = 9 * 3 ^ m := by ring + nlinarith [one_le_pow3R m] + +/-- **Exponent rigidity of a chain triangle.** If a triangle has squared sides `c * 3 ^ p`, +`c * 3 ^ q`, `c * 3 ^ r` with `p ≤ q ≤ r`, then either the two largest exponents agree, or the +two smallest agree and the largest exceeds them by exactly one. -/ +theorem exp_tri {c : ℝ} (hc : 0 < c) {p q r : ℕ} (hpq : p ≤ q) (hqr : q ≤ r) + (h : (c * 3 ^ r - c * 3 ^ p - c * 3 ^ q) ^ 2 ≤ 4 * (c * 3 ^ p) * (c * 3 ^ q)) : + r = q ∨ (p = q ∧ r = p + 1) := by + obtain ⟨s, rfl⟩ : ∃ s, q = p + s := ⟨q - p, by omega⟩ + obtain ⟨t, rfl⟩ : ∃ t, r = p + s + t := ⟨r - (p + s), by omega⟩ + have hS := one_le_pow3R s + have hT := one_le_pow3R t + have hred : ((3 : ℝ) ^ s * 3 ^ t - 1 - 3 ^ s) ^ 2 ≤ 4 * 3 ^ s := by + have hpos : (0 : ℝ) < (c * 3 ^ p) ^ 2 := by positivity + refine le_of_mul_le_mul_left ?_ hpos + have e1 : (c * 3 ^ p) ^ 2 * (((3 : ℝ) ^ s * 3 ^ t - 1 - 3 ^ s) ^ 2) + = (c * 3 ^ (p + s + t) - c * 3 ^ p - c * 3 ^ (p + s)) ^ 2 := by + rw [pow_add, pow_add]; ring + have e2 : (c * 3 ^ p) ^ 2 * (4 * (3 : ℝ) ^ s) + = 4 * (c * 3 ^ p) * (c * 3 ^ (p + s)) := by rw [pow_add]; ring + rw [e1, e2]; exact h + rcases Nat.eq_zero_or_pos t with ht | ht + · left; omega + have hT3 : (3 : ℝ) ≤ 3 ^ t := three_le_pow3R (by omega) + have hs0 : s = 0 := by + by_contra hs + have hS3 : (3 : ℝ) ≤ 3 ^ s := three_le_pow3R hs + have hX : 2 * (3 : ℝ) ^ s - 1 ≤ 3 ^ s * 3 ^ t - 1 - 3 ^ s := by nlinarith + have hX0 : (0 : ℝ) ≤ 2 * (3 : ℝ) ^ s - 1 := by linarith + nlinarith [mul_self_le_mul_self hX0 hX] + subst hs0 + have hle : (3 : ℝ) ^ t ≤ 4 := by + simp only [pow_zero] at hred + nlinarith [hred, hT3] + have ht1 : t = 1 := by + by_contra htc + have : (9 : ℝ) ≤ 3 ^ t := nine_le_pow3R (by omega) + linarith + right; omega + +/-- The four-point equation for two points equidistant from the ends of the shortest edge. -/ +theorem isoceles_pair_solution {j k l : ℕ} (hjk : j ≤ k) + (hcase : j = k ∨ (l = j ∧ k = j + 1) ∨ l = k) + (heq : (3 : ℤ) ^ j * 3 ^ j + 3 ^ k * 3 ^ k + 3 ^ l * 3 ^ l - 2 * (3 ^ j * 3 ^ k) + - 2 * (3 ^ j * 3 ^ l) - 2 * (3 ^ k * 3 ^ l) + 3 ^ l = 0) : + j = 0 ∧ k = 0 ∧ l = 1 := by + have hjp := pow3_pos j + have hkp := pow3_pos k + have hlp := pow3_pos l + have hj1 := one_le_pow3 j + have hk1 := one_le_pow3 k + have hl1 := one_le_pow3 l + rcases hcase with hc | ⟨hlj, hkj⟩ | hlk + · subst hc + have hfac : (3 : ℤ) ^ l * (3 ^ l - 4 * 3 ^ j + 1) = 0 := by linear_combination heq + have h2 : (3 : ℤ) ^ l = 4 * 3 ^ j - 1 := by + rcases mul_eq_zero.mp hfac with h | h + · exact absurd h (by positivity) + · linarith + obtain ⟨hj0, hl1'⟩ := pow3_eq_four_mul_pow3_sub_one h2 + exact ⟨hj0, hj0, hl1'⟩ + · exfalso + rw [hlj, hkj] at heq + have e : (3 : ℤ) ^ (j + 1) = 3 * 3 ^ j := by ring + rw [e] at heq + nlinarith [heq, hj1, mul_le_mul_of_nonneg_left hj1 hjp.le] + · exfalso + rw [hlk] at heq + have hmono : (3 : ℤ) ^ j ≤ 3 ^ k := pow_le_pow_right₀ (by norm_num) hjk + nlinarith [heq, mul_le_mul_of_nonneg_left hmono hjp.le, + le_mul_of_one_le_left hkp.le hj1, mul_pos hjp hkp] + +/-- The four-point equation for one point equidistant from the ends of the shortest edge and one +point spanning it. -/ +theorem mixed_pair_solution {j l : ℕ} (heq : ((3 : ℤ) ^ j - 3 ^ l) ^ 2 - 3 * 3 ^ l + 3 = 0) : + j = 0 ∧ l = 0 := by + rcases eq_or_ne j 0 with hj | hj + · subst hj + rcases eq_or_ne l 0 with hl | hl + · exact ⟨rfl, hl⟩ + · exfalso + have h3 := three_le_pow3 hl + rcases pow3_trichotomy l with h | h | h <;> nlinarith [heq] + · exfalso + have h3 := three_le_pow3 hj + rcases eq_or_ne l 0 with hl | hl + · subst hl; simp only [pow_zero] at heq; nlinarith [heq] + · obtain ⟨u, hu⟩ := three_dvd_pow3 hj + obtain ⟨v, hv⟩ := three_dvd_pow3 hl + rw [hu, hv] at heq + have : (1 : ℤ) = 3 * (v - (u - v) * (u - v)) := by nlinarith [heq] + omega + +theorem pow3_ne_four {l : ℕ} : (3 : ℤ) ^ l ≠ 4 := by + rcases pow3_trichotomy l with h | h | h <;> omega + +theorem pow3_ne_seven {l : ℕ} : (3 : ℤ) ^ l ≠ 7 := by + rcases pow3_trichotomy l with h | h | h <;> omega + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/Statement.lean b/LeanPool/Erdos132ThreeChain/Statement.lean new file mode 100644 index 0000000000..f9ec76e6ca --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Statement.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.Support +import LeanPool.Erdos132ThreeChain.HopfPannwitz + +/-! +# The 3-chain support theorem + +Let `X` be a finite set of points of the plane with squared diameter `D`. This file forbids the +set of *non-diameter* squared distances of `X` from being a geometric 3-chain +`{a, 3a, 9a, …, 3 ^ (h-1) a}`, once `X` has at least thirteen points. + +The lift from the five-point obstruction to arbitrary `n ≥ 13` runs through the *diameter graph* +of `X`, whose vertices are the points of `X` and whose edges join pairs at squared distance +exactly `D`. Hopf--Pannwitz bounds that graph by `#X` edges, Caro--Wei then produces an +independent set of five points, and those five points have all ten of their squared distances +inside the chain — which `no_five_chain_finset` forbids. + +Every ingredient is proved from first principles in this project: the chain-quadruple +catalogue, the five-point Gram obstruction, Caro--Wei, and Hopf--Pannwitz. The result is +unconditional. Of those, Hopf--Pannwitz is a supporting lemma only: the same bound already +exists in the pool as `LeanPool.Erdos132N14.diameterEdges_card_le`, and it is reproved here in +this project's model for self-containment, not offered as a new result. + +There is no prior write-up to follow. The 3-chain support statement was produced by the +author's automated research pipeline in August 2026; the cited source poses the ambient Erdős +problem and nothing more. Section labels used in the docstrings of this development — +"chain-quadruple theorem", "five-point obstruction" — are internal names, not references to a +numbered result anywhere else. Hopf--Pannwitz (1934) and Caro--Wei are classical statements, +but their Lean proofs here are written from scratch. +-/ + +namespace Erdos132ThreeChain + +open Finset + +/-- **The 3-chain support theorem.** Let `n ≥ 13` and `a > 0`, and let `X` be a set of `n` +points of the plane with squared diameter `D`. Then the set of squared distances realised by +distinct points of `X` other than `D` is never the geometric 3-chain `{a * 3 ^ j | j < h}`, for +any chain length `h`. -/ +theorem nonDiameterSqDists_ne_chain {X : Finset Point} {D a : ℝ} {n h : ℕ} + (hn : 13 ≤ n) (ha : 0 < a) (hcard : X.card = n) (hD : IsSqDiameter X D) : + nonDiameterSqDists X D ≠ chain a h := by + intro hsupport + obtain ⟨S, hSX, hScard, hSind⟩ := exists_independent_five (DiameterAdj D) + (diameterAdj_symm D) (diameterAdj_irrefl D) X (by omega) (hopfPannwitz hD) + refine no_five_chain_finset ha hScard ?_ + intro p hp q hq hpq + have hne : sqDist p q ≠ D := fun hEq => hSind p hp q hq ⟨hpq, hEq⟩ + have hmem : sqDist p q ∈ nonDiameterSqDists X D := + ⟨p, hSX hp, q, hSX hq, hpq, rfl, hne⟩ + rw [hsupport] at hmem + obtain ⟨j, -, hj⟩ := hmem + exact ⟨j, hj⟩ + +/-- The `h ≥ 2` reading of the support theorem, kept so that a statement matching the informal +phrasing "a geometric 3-chain of length at least two" is available directly. It is a wrapper +around `nonDiameterSqDists_ne_chain`, which needs no bound on `h` at all; `_hh` is therefore +unused. -/ +theorem threeChain_support_empty {X : Finset Point} {D a : ℝ} {n h : ℕ} + (hn : 13 ≤ n) (_hh : 2 ≤ h) (ha : 0 < a) (hcard : X.card = n) + (hD : IsSqDiameter X D) + (hsupport : nonDiameterSqDists X D = chain a h) : False := + nonDiameterSqDists_ne_chain hn ha hcard hD hsupport + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/Support.lean b/LeanPool/Erdos132ThreeChain/Support.lean new file mode 100644 index 0000000000..ac417b3e98 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Support.lean @@ -0,0 +1,157 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.FivePoints +import Mathlib.Data.Finset.Card +import Mathlib.Data.Finset.Lattice.Fold +import Mathlib.Data.Finset.Max +import Mathlib.Data.Finset.Prod + +/-! +# 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. +-/ + +namespace Erdos132ThreeChain + +open Finset + +theorem 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 := by + have hj : j₀ ≤ j := by + by_contra hlt + have hlt' : j < j₀ := by omega + have : (3 : ℝ) ^ j < 3 ^ j₀ := by + exact pow_lt_pow_right₀ (by norm_num) hlt' + rw [hc, hx] at hle + nlinarith + refine ⟨j - j₀, ?_⟩ + rw [hx, hc, mul_assoc, ← pow_add] + congr 2 + omega + +/-- 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 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) := by + classical + set U : Finset (Point × Point) := (S ×ˢ S).filter fun x => x.1 ≠ x.2 with hU + have hUne : U.Nonempty := by + obtain ⟨u, hu, v, hv, huv⟩ := Finset.one_lt_card.mp (by omega : 1 < S.card) + exact ⟨(u, v), by simp [hU, Finset.mem_filter, Finset.mem_product, hu, hv, huv]⟩ + obtain ⟨⟨A, B⟩, hABmem, hmin⟩ := Finset.exists_min_image U (fun x => sqDist x.1 x.2) hUne + have hAB : A ∈ S ∧ B ∈ S ∧ A ≠ B := by + have hf := Finset.mem_filter.mp hABmem + exact ⟨(Finset.mem_product.mp hf.1).1, (Finset.mem_product.mp hf.1).2, hf.2⟩ + obtain ⟨j₀, hj₀⟩ := hch A hAB.1 B hAB.2.1 hAB.2.2 + refine ⟨A, hAB.1, B, hAB.2.1, hAB.2.2, fun p hp q hq hpq => ?_⟩ + obtain ⟨j, hj⟩ := hch p hp q hq hpq + exact isChainValue_of_le ha hj₀ hj + (hmin (p, q) (by simp [hU, Finset.mem_filter, Finset.mem_product, hp, hq, hpq])) + +/-- **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 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 := by + classical + obtain ⟨A, hA, B, hB, hAB, hchain⟩ := exists_min_edge ha (by omega) hch + obtain ⟨jbase, hjbase⟩ := hch A hA B hB hAB + set c : ℝ := sqDist A B with hcdef + have hc : 0 < c := sqDist_pos hAB + have hsub : ({A, B} : Finset Point) ⊆ S := by + intro x hx + simp only [Finset.mem_insert, Finset.mem_singleton] at hx + rcases hx with rfl | rfl + · exact hA + · exact hB + have hrest : (S \ {A, B}).card = 2 := by + rw [Finset.card_sdiff, Finset.inter_eq_left.mpr hsub, hcard, + Finset.card_insert_of_notMem (by simpa using hAB), Finset.card_singleton] + obtain ⟨C, D, hCD, hset⟩ := Finset.card_eq_two.mp hrest + have hmemC : C ∈ S \ {A, B} := by rw [hset]; simp + have hmemD : D ∈ S \ {A, B} := by rw [hset]; simp + have hCS : C ∈ S := (Finset.mem_sdiff.mp hmemC).1 + have hDS : D ∈ S := (Finset.mem_sdiff.mp hmemD).1 + have hCA : A ≠ C := fun h => (Finset.mem_sdiff.mp hmemC).2 (by rw [← h]; simp) + have hCB : B ≠ C := fun h => (Finset.mem_sdiff.mp hmemC).2 (by rw [← h]; simp) + have hDA : A ≠ D := fun h => (Finset.mem_sdiff.mp hmemD).2 (by rw [← h]; simp) + have hDB : B ≠ D := fun h => (Finset.mem_sdiff.mp hmemD).2 (by rw [← h]; simp) + have quad := pair_classification hc rfl (hchain A hA C hCS hCA) + (hchain B hB C hCS hCB) (hchain A hA D hDS hDA) (hchain B hB D hDS hDB) + (hchain C hCS D hDS hCD) + have posC := quad.posC + have posD := quad.posD + have hmem : ∀ p ∈ S, p = A ∨ p = B ∨ p = C ∨ p = D := by + intro p hp + by_cases hpm : p ∈ ({A, B} : Finset Point) + · simp only [Finset.mem_insert, Finset.mem_singleton] at hpm; tauto + · have : p ∈ S \ {A, B} := Finset.mem_sdiff.mpr ⟨hp, hpm⟩ + rw [hset] at this + simp only [Finset.mem_insert, Finset.mem_singleton] at this + tauto + refine ⟨c, hc, ⟨jbase, hjbase⟩, fun p hp q hq hpq => ?_⟩ + have eAB : sqDist A B = c ∨ sqDist A B = 3 * c := Or.inl rfl + have eBA : sqDist B A = c ∨ sqDist B A = 3 * c := by rw [sqDist_comm B A]; exact eAB + have eAC : sqDist A C = c ∨ sqDist A C = 3 * c := posC.fromLeft + have eCA : sqDist C A = c ∨ sqDist C A = 3 * c := by rw [sqDist_comm C A]; exact eAC + have eBC : sqDist B C = c ∨ sqDist B C = 3 * c := posC.fromRight + have eCB : sqDist C B = c ∨ sqDist C B = 3 * c := by rw [sqDist_comm C B]; exact eBC + have eAD : sqDist A D = c ∨ sqDist A D = 3 * c := posD.fromLeft + have eDA : sqDist D A = c ∨ sqDist D A = 3 * c := by rw [sqDist_comm D A]; exact eAD + have eBD : sqDist B D = c ∨ sqDist B D = 3 * c := posD.fromRight + have eDB : sqDist D B = c ∨ sqDist D B = 3 * c := by rw [sqDist_comm D B]; exact eBD + have eCD : sqDist C D = c ∨ sqDist C D = 3 * c := quad.distCD + have eDC : sqDist D C = c ∨ sqDist D C = 3 * c := by rw [sqDist_comm D C]; exact eCD + rcases hmem p hp with rfl | rfl | rfl | rfl <;> rcases hmem q hq with rfl | rfl | rfl | rfl <;> + first + | exact absurd rfl hpq + | assumption + +/-- **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. -/ +theorem 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 := by + classical + obtain ⟨A, hA, B, hB, hAB, hchain⟩ := exists_min_edge ha (by omega) hch + have hc : 0 < sqDist A B := sqDist_pos hAB + have hsub : ({A, B} : Finset Point) ⊆ S := by + intro x hx + simp only [Finset.mem_insert, Finset.mem_singleton] at hx + rcases hx with rfl | rfl + · exact hA + · exact hB + have hrest : (S \ {A, B}).card = 3 := by + rw [Finset.card_sdiff, Finset.inter_eq_left.mpr hsub, hcard, + Finset.card_insert_of_notMem (by simpa using hAB), Finset.card_singleton] + obtain ⟨C, D, E, hCD, hCE, hDE, hset⟩ := Finset.card_eq_three.mp hrest + have hmemC : C ∈ S \ {A, B} := by rw [hset]; simp + have hmemD : D ∈ S \ {A, B} := by rw [hset]; simp + have hmemE : E ∈ S \ {A, B} := by rw [hset]; simp + have hCS : C ∈ S := (Finset.mem_sdiff.mp hmemC).1 + have hDS : D ∈ S := (Finset.mem_sdiff.mp hmemD).1 + have hES : E ∈ S := (Finset.mem_sdiff.mp hmemE).1 + have hCA : A ≠ C := fun h => (Finset.mem_sdiff.mp hmemC).2 (by rw [← h]; simp) + have hCB : B ≠ C := fun h => (Finset.mem_sdiff.mp hmemC).2 (by rw [← h]; simp) + have hDA : A ≠ D := fun h => (Finset.mem_sdiff.mp hmemD).2 (by rw [← h]; simp) + have hDB : B ≠ D := fun h => (Finset.mem_sdiff.mp hmemD).2 (by rw [← h]; simp) + have hEA : A ≠ E := fun h => (Finset.mem_sdiff.mp hmemE).2 (by rw [← h]; simp) + have hEB : B ≠ E := fun h => (Finset.mem_sdiff.mp hmemE).2 (by rw [← h]; simp) + exact no_five_chain_points hc rfl (hchain A hA C hCS hCA) (hchain A hA D hDS hDA) + (hchain A hA E hES hEA) (hchain B hB C hCS hCB) (hchain B hB D hDS hDB) + (hchain B hB E hES hEB) (hchain C hCS D hDS hCD) (hchain C hCS E hES hCE) + (hchain D hDS E hES hDE) + +end Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/Witnesses.lean b/LeanPool/Erdos132ThreeChain/Witnesses.lean new file mode 100644 index 0000000000..5509c944fb --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Witnesses.lean @@ -0,0 +1,115 @@ +/- +Copyright (c) 2026 Egor Lyfar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egor Lyfar +-/ + +import LeanPool.Erdos132ThreeChain.Basic +import Mathlib.Analysis.SpecialFunctions.Sqrt + +/-! +# 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}`. +-/ + +namespace Erdos132ThreeChain + +/-- 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 rhombus_chain_config : + ∃ A B C 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 := by + have h3 : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num) + have hpos : 0 < Real.sqrt 3 := Real.sqrt_pos.mpr (by norm_num) + refine ⟨(-(1 / 2), 0), (1 / 2, 0), (0, Real.sqrt 3 / 2), (0, -(Real.sqrt 3 / 2)), ?_, ?_, ?_, + ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> + simp only [sqDist, Prod.mk.injEq, ne_eq, not_and] <;> intros <;> nlinarith [h3, hpos] + +/-- 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 centroid_chain_config : + ∃ A B C 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 := by + have h3 : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num) + have hpos : 0 < Real.sqrt 3 := Real.sqrt_pos.mpr (by norm_num) + refine ⟨(0, 0), (1, 0), (-(1 / 2), Real.sqrt 3 / 2), (-(1 / 2), -(Real.sqrt 3 / 2)), ?_, ?_, + ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> + simp only [sqDist, Prod.mk.injEq, ne_eq, not_and] <;> intros <;> nlinarith [h3, hpos] + + +/-- 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 chainTwo_config : + ∃ A B C E 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 := by + have h3 : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num) + have hpos : 0 < Real.sqrt 3 := Real.sqrt_pos.mpr (by norm_num) + refine ⟨(0, 0), (1, 0), (-(1 / 2), Real.sqrt 3 / 2), (1 / 2, Real.sqrt 3 / 2), + (0, Real.sqrt 3), ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, + ?_, ?_⟩ <;> + simp only [sqDist, Prod.mk.injEq, ne_eq, not_and] <;> intros <;> nlinarith [h3, hpos] + +/-- **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. -/ +theorem chainTwo_nonDiameter_support : + ∃ X : Finset Point, X.card = 5 ∧ IsSqDiameter X 4 ∧ nonDiameterSqDists X 4 = chain 1 2 := by + classical + obtain ⟨A, B, C, E, F, hAB, hAC, hAE, hAF, hBC, hBE, hBF, hCE, hCF, hEF, + dAB, dAC, dAE, dAF, dBC, dBE, dBF, dCE, dCF, dEF⟩ := chainTwo_config + have eBA : sqDist B A = 1 := by rw [sqDist_comm B A]; exact dAB + have eCA : sqDist C A = 1 := by rw [sqDist_comm C A]; exact dAC + have eEA : sqDist E A = 1 := by rw [sqDist_comm E A]; exact dAE + have eFA : sqDist F A = 3 := by rw [sqDist_comm F A]; exact dAF + have eCB : sqDist C B = 3 := by rw [sqDist_comm C B]; exact dBC + have eEB : sqDist E B = 1 := by rw [sqDist_comm E B]; exact dBE + have eFB : sqDist F B = 4 := by rw [sqDist_comm F B]; exact dBF + have eEC : sqDist E C = 1 := by rw [sqDist_comm E C]; exact dCE + have eFC : sqDist F C = 1 := by rw [sqDist_comm F C]; exact dCF + have eFE : sqDist F E = 1 := by rw [sqDist_comm F E]; exact dEF + have hmem : ∀ p ∈ ({A, B, C, E, F} : Finset Point), p = A ∨ p = B ∨ p = C ∨ p = E ∨ p = F := by + intro p hp + simp only [Finset.mem_insert, Finset.mem_singleton] at hp + tauto + have hvals : ∀ p ∈ ({A, B, C, E, F} : Finset Point), ∀ q ∈ ({A, B, C, E, F} : Finset Point), + sqDist p q = 0 ∨ sqDist p q = 1 ∨ sqDist p q = 3 ∨ sqDist p q = 4 := by + intro p hp q hq + rcases hmem p hp with rfl | rfl | rfl | rfl | rfl <;> + rcases hmem q hq with rfl | rfl | rfl | rfl | rfl <;> + simp only [sqDist_self, dAB, dAC, dAE, dAF, dBC, dBE, dBF, dCE, dCF, dEF, + eBA, eCA, eEA, eFA, eCB, eEB, eFB, eEC, eFC, eFE, true_or, or_true] + refine ⟨{A, B, C, E, F}, ?_, ⟨⟨B, by simp, F, by simp, hBF, dBF⟩, ?_⟩, ?_⟩ + · rw [Finset.card_insert_of_notMem (by simp [hAB, hAC, hAE, hAF]), + Finset.card_insert_of_notMem (by simp [hBC, hBE, hBF]), + Finset.card_insert_of_notMem (by simp [hCE, hCF]), + Finset.card_insert_of_notMem (by simp [hEF]), Finset.card_singleton] + · intro p hp q hq + rcases hvals p hp q hq with h | h | h | h <;> rw [h] <;> norm_num + · ext x + constructor + · rintro ⟨p, hp, q, hq, hpq, rfl, hne⟩ + rcases hvals p hp q hq with h | h | h | h + · exact absurd (sqDist_eq_zero_iff.mp h) hpq + · exact ⟨0, by norm_num, by rw [h]; norm_num⟩ + · exact ⟨1, by norm_num, by rw [h]; norm_num⟩ + · exact absurd h hne + · rintro ⟨j, hj, rfl⟩ + have hj2 : j = 0 ∨ j = 1 := by omega + rcases hj2 with rfl | rfl + · exact ⟨A, by simp, B, by simp, hAB, by rw [dAB]; norm_num, by norm_num⟩ + · exact ⟨A, by simp, F, by simp, hAF, by rw [dAF]; norm_num, by norm_num⟩ + +end Erdos132ThreeChain diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 0716f9ddb1..8fbd18dbd5 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -6043,3 +6043,165 @@ projects: msc: - "57K20" - "57N05" + - slug: erdos132-three-chain + title: Planar Point Sets Whose Non-Diameter Distances Form a Geometric 3-Chain + summary: >- + Formalizes a support theorem about planar point sets whose non-diameter squared + distances are confined to a geometric progression of ratio three. The chain-quadruple + theorem shows that no planar quadruple with all six squared distances in such a chain + can span two chain steps, and classifies the seven labelled patterns that do occur: the + rhombus of two glued equilateral triangles, in five positions of its long edge, and the + equilateral triangle with its centroid, in two. A Gram obstruction then rules out any + five-point chain configuration. The lift to n at least thirteen runs through the + diameter graph: the Caro--Wei independence bound, proved here, produces an independent + five-set once the diameter graph is known to have at most as many edges as the set has + points. That edge bound is the Hopf--Pannwitz theorem of 1934, and it already exists in + the pool; this project reproves it in its own model as a supporting lemma, claiming no + novelty for it, and the overlap is set out in full below. The result is + unconditional. + + There is no prior write-up behind this development. The restriction to ratio 3 is ad hoc: + the 3-chain statement was produced by the author's automated research pipeline in August + 2026, while the cited source poses the ambient Erdos problem and does not state this + restriction or result. This theorem does not resolve Erdos 132, whose distance spectra need + not be geometric 3-chains. The descriptive labels used in the Lean docstrings are internal + to this development and refer to no numbered result elsewhere. + + Overlap disclosure. Erdos132ThreeChain.hopfPannwitz is NOT offered as a new result. The + pooled project Erdos132N14 already contains the same diameter bound, and the version + here exists only so that this project is self-contained. Its statement, verbatim from + LeanPool/Erdos132N14/HopfPannwitz.lean, is + + theorem diameterEdges_card_le + (P : Configuration ι) (S : Finset ι) {d : ℝ} + (hd : 0 < d) + (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) : + (diameterEdges P S d).card ≤ S.card + + where, from LeanPool/Erdos132N14/Basic.lean, `Configuration ι` is a structure carrying + an injective `point : ι → ℂ`, `pairs S = (S ×ˢ S).filter fun e ↦ e.1 < e.2` for a + `LinearOrder ι`, `pairDistance P e = dist (P.point e.1) (P.point e.2)`, and + `diameterEdges P S d = (pairs S).filter fun e ↦ P.pairDistance e = d`. The corresponding + statement here is + + theorem hopfPannwitz {X : Finset Point} {D : ℝ} (hD : IsSqDiameter X D) : + ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card + + with `Point = ℝ × ℝ`, `sqDist` the squared Euclidean distance, + `DiameterAdj D p q = (p ≠ q ∧ sqDist p q = D)`, `degree adj X v = (X.filter (adj v)).card`, + and `IsSqDiameter X D` asserting that `D` is realised by two distinct points of `X` and + dominates every squared distance inside `X`. The two are the same mathematical theorem — + a positive maximal distance is realised at most as often as there are points — carried + by different models: an injective map from a linearly ordered index type into the + complex plane, counting a Finset of unordered pairs, against a Finset of points of the + real plane, in squared distances and degree-sum form. Neither statement is an instance + of the other without a model bridge: a LinearOrder on ℝ × ℝ, a dist-to-sqDist transfer, + and a handshake lemma. The proofs differ too, Perles charging there against pendant + deletion driven by Cramer's rule here. No project in the pool imports another, and + CONTRIBUTING.md records that independence as the property the fast per-project build + relies on, so this project reproves the bound rather than importing it. It is a + supporting lemma of this development, not one of its results, and it is therefore not + listed among the main results below. + + Two supporting identities also exist elsewhere in the pool. From + LeanPool/Erdos97ConvexOctagon/CayleyMenger.lean, + + theorem cm4_sqDist_eq_zero (a b c d : Plane) : + cm4 (sqDist a b) (sqDist a c) (sqDist a d) + (sqDist b c) (sqDist b d) (sqDist c d) = 0 + + over `Plane = EuclideanSpace ℝ (Fin 2)` is the same four-point Cayley--Menger vanishing + as this project's + + theorem gramDet_eq_zero (a b c d : Point) : + gramDet (sqDist a b) (sqDist a c) (sqDist a d) (sqDist b c) (sqDist b d) (sqDist c d) = 0 + + over `Point = ℝ × ℝ`; both are one-line `ring` identities in the coordinates. From + LeanPool/DistanceGeometry/SchoenbergHard.lean, + + theorem schoenberg {D : Matrix (Fin n) (Fin n) ℝ} (hD : IsPreDistMatrix D) : + EmbedsIn D k ↔ (centeredGram D).PosSemidef ∧ (centeredGram D).rank ≤ k + + characterizes Euclidean distance matrices in general dimension. This project never + invokes it: the four-point condition is used directly as a `ring` identity and the + five-point obstruction is a sum-of-squares contradiction, so no positive-semidefiniteness + criterion is needed. + branch: discrete geometry + entry_module: LeanPool.Erdos132ThreeChain + authors: + - Egor Lyfar + source: + title: "Erdős Problem #132" + authors: + - Paul Erdős + - János Pach + url: https://www.erdosproblems.com/132 + github_repo: lyfar/lean-pool + license: Apache-2.0 + status: verified + provenance: AI + main_declarations: + - Erdos132ThreeChain.nonDiameterSqDists_ne_chain + main_results: + - declaration: Erdos132ThreeChain.nonDiameterSqDists_ne_chain + informal: >- + Let n be at least thirteen, let a be positive, and let X be a finite set of points of + the real plane with exactly n elements. Suppose D is the squared diameter of X, + meaning that D is realised by two distinct points of X and dominates every squared + distance inside X. Then for every natural number h, the set of squared distances + realised by distinct points of X and different from D is not equal to the geometric + 3-chain consisting of a times 3^j for j below h. + - declaration: Erdos132ThreeChain.four_chain_adjacent + informal: >- + Let a be positive and let S be a four-element set of points of the real plane such + that every squared distance between distinct points of S equals a times a + nonnegative power of three. Then there is a positive r, itself equal to a times a + nonnegative power of three, for which every squared distance between distinct points + of S equals r or 3r. + - declaration: Erdos132ThreeChain.pair_classification + informal: >- + Let c be positive and let A, B, C, D be points of the real plane with the squared + distance from A to B equal to c and every other pairwise squared distance equal to c + times a nonnegative power of three. Then each of the four squared distances from A + and B to C and to D equals c or 3c, at least one of the two squared distances from A + and B to C equals c, likewise for D, the squared distance from C to D equals c or 3c, + the squared distance from A to C equals c or that from B to D equals c, the squared + distance from B to C equals c or that from A to D equals c, and the whole labelling + is one of exactly seven explicit patterns: five with a single edge of squared length + 3c, and two in which the three edges of squared length 3c form a triangle. + - declaration: Erdos132ThreeChain.no_five_chain_finset + informal: >- + Let a be positive. There is no five-element set of points of the real plane in which + every squared distance between distinct points equals a times a nonnegative power of + three. + - declaration: Erdos132ThreeChain.no_four_on_circle + informal: >- + Let c be positive. There are no four points of the real plane, each at squared + distance c from a common point, whose six pairwise squared distances all equal c or + 3c. + - declaration: Erdos132ThreeChain.carowei + informal: >- + Let adj be a symmetric irreflexive relation with decidable adjacency on a type, and + let V be a finite set of vertices. Then V has a subset S, no two elements of which + are adjacent, whose cardinality is at least the sum over v in V of one divided by + one plus the number of neighbours of v inside V. + - declaration: Erdos132ThreeChain.exists_independent_five + informal: >- + Let adj be a symmetric irreflexive relation with decidable adjacency on a type, and + let V be a finite set of at least thirteen vertices whose degrees inside V sum to at + most twice the cardinality of V. Then V has a five-element subset no two elements of + which are adjacent. + - declaration: Erdos132ThreeChain.chainTwo_nonDiameter_support + informal: >- + There is a five-element set of points of the real plane whose squared diameter is 4 + and whose set of non-diameter squared distances is exactly the two-term geometric + 3-chain consisting of 1 and 3. The configuration that the headline forbids for at + least thirteen points is therefore realisable at five points with chain length two. + tags: + - discrete-geometry + - distance-geometry + - erdos-problems + msc: + - "52C10" + - "52C35" + - "05C69"