From 7581200d429415ca8aecf5da2520707702513514 Mon Sep 17 00:00:00 2001 From: Egor Lyfar Date: Fri, 21 Aug 2026 17:46:05 +0800 Subject: [PATCH 1/4] feat: formalize the geometric 3-chain support theorem Adds LeanPool/Erdos132ThreeChain, a self-contained formalization about finite planar point sets whose non-diameter squared distances are confined to a geometric progression of ratio three. - nonDiameterSqDists_ne_chain: the main declaration. For n >= 13 and a > 0, an n-point planar set with squared diameter D never has its set of non-diameter squared distances equal to {a * 3^j : j < h}, for any chain length h. threeChain_support_empty is the thin 2 <= h wrapper kept for statement fidelity. - four_chain_adjacent: the chain-quadruple theorem. The six pairwise squared distances of a planar chain quadruple all lie in one adjacent pair {r, 3r} of the chain, with r itself in the chain, so no such quadruple spans two chain steps. pair_classification refines this to the seven labelled patterns of the inductive ChainPattern, which are the 6 + 4 = 10 labelled assignments per adjacent pair once the choice of shortest edge is dropped. - no_five_chain_finset: the five-point obstruction. No five-element planar set has all ten of its pairwise squared distances inside such a chain. The obstruction is a Gram/PSD failure written as a sum of squares equal to -2c^3, the scale-free form of the -27r^4 determinant recorded in symDet4_chain_five. - carowei and exists_independent_five: the Caro-Wei independence bound by minimum-degree induction, plus the tangent-line estimate that turns a degree-sum bound into an independent five-set at n >= 13. - hopfPannwitz: a supporting lemma, not a result of this project. The same diameter bound already exists in the pool as LeanPool.Erdos132N14.diameterEdges_card_le, proved by Perles charging over an injective map from a linearly ordered index type into the complex plane and stated as a bound on the cardinality of a Finset of unordered pairs. It is reproved here over a Finset of points of the real plane, in squared distances and handshake degree-sum form, only because pool projects do not import one another; the card discloses the overlap with both statements verbatim and does not list it among the main results. The proof needs neither segment crossings nor angular betweenness: Cramer's rule in the plane, Z * B = Y * A + X * C for the cross products of the vectors to three points at squared distance D, turns maximality of D into Z < X + Y, and pairing that identity with a candidate partner of the middle point forces the partner to be the centre. sum_degree_le proves the bound for any D that dominates the squared distances of X, without needing D to be attained. - Witnesses: chainTwo_nonDiameter_support exhibits a five-point set whose squared diameter is 4 and whose non-diameter squared-distance support is exactly chain 1 2 = {1, 3}, so the forbidden configuration is realisable below the n >= 13 threshold at chain length two; rhombus_nonDiameter_support is the same at chain length one; rhombus_chain_config and centroid_chain_config exhibit the two planar patterns of the catalogue; symDet4_chain_five records the exact -27r^4 determinant. All planar input is polynomial: Heron's formula as (z-x-y)^2 <= 4xy, the anchored Cayley-Menger determinant for coplanarity, the singular Gram matrices, and Cramer's rule, each proved by ring from coordinates. No square roots enter the arguments and no principal-minor enumeration is needed. There is no prior write-up behind the 3-chain statement; it was produced by the author's automated research pipeline in August 2026. The cited source poses the ambient Erdos problem and states nothing about geometric 3-chains, and this does not resolve that problem. Descriptive labels in the docstrings are internal names for results of this development. --- LeanPool.lean | 11 + LeanPool/Erdos132ThreeChain.lean | 20 ++ LeanPool/Erdos132ThreeChain/Basic.lean | 80 +++++ LeanPool/Erdos132ThreeChain/CaroWei.lean | 152 ++++++++ LeanPool/Erdos132ThreeChain/FivePoints.lean | 125 +++++++ LeanPool/Erdos132ThreeChain/FourPoints.lean | 336 ++++++++++++++++++ LeanPool/Erdos132ThreeChain/HopfPannwitz.lean | 308 ++++++++++++++++ LeanPool/Erdos132ThreeChain/Plane.lean | 88 +++++ LeanPool/Erdos132ThreeChain/PowerThree.lean | 179 ++++++++++ LeanPool/Erdos132ThreeChain/Statement.lean | 75 ++++ LeanPool/Erdos132ThreeChain/Support.lean | 157 ++++++++ LeanPool/Erdos132ThreeChain/Witnesses.lean | 202 +++++++++++ LeanPool/projects.yml | 161 +++++++++ 13 files changed, 1894 insertions(+) create mode 100644 LeanPool/Erdos132ThreeChain.lean create mode 100644 LeanPool/Erdos132ThreeChain/Basic.lean create mode 100644 LeanPool/Erdos132ThreeChain/CaroWei.lean create mode 100644 LeanPool/Erdos132ThreeChain/FivePoints.lean create mode 100644 LeanPool/Erdos132ThreeChain/FourPoints.lean create mode 100644 LeanPool/Erdos132ThreeChain/HopfPannwitz.lean create mode 100644 LeanPool/Erdos132ThreeChain/Plane.lean create mode 100644 LeanPool/Erdos132ThreeChain/PowerThree.lean create mode 100644 LeanPool/Erdos132ThreeChain/Statement.lean create mode 100644 LeanPool/Erdos132ThreeChain/Support.lean create mode 100644 LeanPool/Erdos132ThreeChain/Witnesses.lean diff --git a/LeanPool.lean b/LeanPool.lean index d406245f8e..b590018978 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -767,6 +767,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..0a6814eeb7 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Basic.lean @@ -0,0 +1,80 @@ +/- +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 two elementary objects used throughout the project: points of the +Euclidean plane together with their squared distance, 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) + +/-- 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⟩ + +/-- `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..0628369ef6 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/FivePoints.lean @@ -0,0 +1,125 @@ +/- +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. The equivalent determinant +statement, whose value is `-27 * r ^ 4`, is recorded as `symDet4_chain_five` in +`LeanPool/Erdos132ThreeChain/Witnesses.lean`. +-/ + +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..d6742763da --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean @@ -0,0 +1,308 @@ +/- +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 + +/-- `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 + +/-- 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..43a8b36a20 --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Statement.lean @@ -0,0 +1,75 @@ +/- +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 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} + +/-- **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..36c96be25d --- /dev/null +++ b/LeanPool/Erdos132ThreeChain/Witnesses.lean @@ -0,0 +1,202 @@ +/- +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.Statement +import Mathlib.Analysis.SpecialFunctions.Sqrt + +/-! +# Witnesses and the determinant form of the five-point obstruction + +Two things are recorded here. + +First, 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}`. + +Second, `symDet4_chain_five` records the determinant form of the five-point obstruction. The +doubled anchored Gram matrix of the only assignment that survives the four-point catalogue has +determinant `-27 * r ^ 4`, whereas `symDet4_dotp_eq_zero` shows that the Gram matrix of four +plane vectors is singular. `no_four_on_circle` proves the same obstruction in the +equivalent sum-of-squares form, which avoids having to enumerate principal minors at all. +-/ + +namespace Erdos132ThreeChain + +/-- The determinant of the symmetric `4 × 4` matrix with diagonal `d₁ d₂ d₃ d₄` and +off-diagonal entries `eᵢⱼ`. -/ +def symDet4 (d₁ d₂ d₃ d₄ e₁₂ e₁₃ e₁₄ e₂₃ e₂₄ e₃₄ : ℝ) : ℝ := + d₁ * d₂ * d₃ * d₄ - d₁ * d₂ * e₃₄ ^ 2 - d₁ * d₃ * e₂₄ ^ 2 - d₁ * d₄ * e₂₃ ^ 2 + + 2 * d₁ * e₂₃ * e₂₄ * e₃₄ - d₂ * d₃ * e₁₄ ^ 2 - d₂ * d₄ * e₁₃ ^ 2 + + 2 * d₂ * e₁₃ * e₁₄ * e₃₄ - d₃ * d₄ * e₁₂ ^ 2 + 2 * d₃ * e₁₂ * e₁₄ * e₂₄ + + 2 * d₄ * e₁₂ * e₁₃ * e₂₃ + e₁₂ ^ 2 * e₃₄ ^ 2 - 2 * e₁₂ * e₁₃ * e₂₄ * e₃₄ + - 2 * e₁₂ * e₁₄ * e₂₃ * e₃₄ + e₁₃ ^ 2 * e₂₄ ^ 2 - 2 * e₁₃ * e₁₄ * e₂₃ * e₂₄ + + e₁₄ ^ 2 * e₂₃ ^ 2 + +/-- The Gram matrix of four vectors of the plane is singular. -/ +theorem symDet4_dotp_eq_zero (o p q r s : Point) : + symDet4 (dotp o p p) (dotp o q q) (dotp o r r) (dotp o s s) (dotp o p q) (dotp o p r) + (dotp o p s) (dotp o q r) (dotp o q s) (dotp o r s) = 0 := by + simp only [symDet4, dotp]; ring + +/-- The doubled anchored Gram determinant of the only five-point assignment that survives the +four-point catalogue — a triangle of `3 * r` edges together with seven `r` edges — equals +`-27 * r ^ 4`. -/ +theorem symDet4_chain_five (r : ℝ) : + symDet4 (2 * r) (2 * r) (2 * r) (2 * r) r r r (-r) (-r) (-r) = -27 * r ^ 4 := by + simp only [symDet4]; ring + +theorem symDet4_chain_five_ne_zero {r : ℝ} (hr : 0 < r) : + symDet4 (2 * r) (2 * r) (2 * r) (2 * r) r r r (-r) (-r) (-r) ≠ 0 := by + rw [symDet4_chain_five] + have : (0 : ℝ) < r ^ 4 := by positivity + linarith + +/-- 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] + + +/-- The rhombus witnesses that the definitions in the headline theorem are not vacuous: it is a +four-point set whose squared diameter is `3` and whose set of non-diameter squared distances is +exactly the one-term geometric 3-chain `{1}`. Thus `IsSqDiameter`, `nonDiameterSqDists` and +`chain` do realise the configuration that `threeChain_support_empty` forbids for `n ≥ 13`. -/ +theorem rhombus_nonDiameter_support : + ∃ X : Finset Point, X.card = 4 ∧ IsSqDiameter X 3 ∧ nonDiameterSqDists X 3 = chain 1 1 := by + classical + obtain ⟨A, B, C, D, hAB, hAC, hAD, hBC, hBD, hCD, dAB, dAC, dAD, dBC, dBD, dCD⟩ := + rhombus_chain_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 eDA : sqDist D A = 1 := by rw [sqDist_comm D A]; exact dAD + have eCB : sqDist C B = 1 := by rw [sqDist_comm C B]; exact dBC + have eDB : sqDist D B = 1 := by rw [sqDist_comm D B]; exact dBD + have eDC : sqDist D C = 3 := by rw [sqDist_comm D C]; exact dCD + have hmem : ∀ p ∈ ({A, B, C, D} : Finset Point), p = A ∨ p = B ∨ p = C ∨ p = D := by + intro p hp + simp only [Finset.mem_insert, Finset.mem_singleton] at hp + tauto + have hvals : ∀ p ∈ ({A, B, C, D} : Finset Point), ∀ q ∈ ({A, B, C, D} : Finset Point), + sqDist p q = 0 ∨ sqDist p q = 1 ∨ sqDist p q = 3 := by + intro p hp q hq + rcases hmem p hp with rfl | rfl | rfl | rfl <;> + rcases hmem q hq with rfl | rfl | rfl | rfl <;> + first + | exact Or.inl (sqDist_self _) + | exact Or.inr (Or.inl (by assumption)) + | exact Or.inr (Or.inr (by assumption)) + refine ⟨{A, B, C, D}, ?_, ⟨⟨C, by simp, D, by simp, hCD, dCD⟩, ?_⟩, ?_⟩ + · rw [Finset.card_insert_of_notMem (by simp [hAB, hAC, hAD]), + Finset.card_insert_of_notMem (by simp [hBC, hBD]), + Finset.card_insert_of_notMem (by simp [hCD]), Finset.card_singleton] + · intro p hp q hq + rcases hvals p hp q hq with 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 + · exact absurd (sqDist_eq_zero_iff.mp h) hpq + · exact ⟨0, by norm_num, by rw [h]; norm_num⟩ + · exact absurd h hne + · rintro ⟨j, hj, rfl⟩ + have hj0 : j = 0 := by omega + subst hj0 + exact ⟨A, by simp, B, by simp, hAB, by rw [dAB]; norm_num, by norm_num⟩ + + +/-- 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 <;> + first + | exact Or.inl (sqDist_self _) + | exact Or.inr (Or.inl (by assumption)) + | exact Or.inr (Or.inr (Or.inl (by assumption))) + | exact Or.inr (Or.inr (Or.inr (by assumption))) + 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 37f54eb169..3f9a66d261 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -5778,3 +5778,164 @@ projects: - "14H40" - "30F30" - "32G20" + - 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 3-chain statement was produced + by the author's automated research pipeline in August 2026; the cited source poses the + ambient Erdos problem and states nothing about geometric 3-chains, and the result does + not resolve that problem, 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: "Erdos Problem #132" + authors: + - Paul Erdos + 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" From 3e2457661fc4a511eabd2bb3008386b79866d0c1 Mon Sep 17 00:00:00 2001 From: Egor Lyfar Date: Mon, 24 Aug 2026 16:55:30 +0800 Subject: [PATCH 2/4] fix: address Erdos 132 three-chain review --- LeanPool/Erdos132ThreeChain/FivePoints.lean | 4 +- LeanPool/Erdos132ThreeChain/Witnesses.lean | 50 +++------------------ LeanPool/projects.yml | 12 ++--- 3 files changed, 14 insertions(+), 52 deletions(-) diff --git a/LeanPool/Erdos132ThreeChain/FivePoints.lean b/LeanPool/Erdos132ThreeChain/FivePoints.lean index 0628369ef6..def828b378 100644 --- a/LeanPool/Erdos132ThreeChain/FivePoints.lean +++ b/LeanPool/Erdos132ThreeChain/FivePoints.lean @@ -19,9 +19,7 @@ every three-vector Gram matrix in the plane forces each triple product `⟪u i, ⟪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. The equivalent determinant -statement, whose value is `-27 * r ^ 4`, is recorded as `symDet4_chain_five` in -`LeanPool/Erdos132ThreeChain/Witnesses.lean`. +This is the five-point Gram obstruction in its scale-free form. -/ namespace Erdos132ThreeChain diff --git a/LeanPool/Erdos132ThreeChain/Witnesses.lean b/LeanPool/Erdos132ThreeChain/Witnesses.lean index 36c96be25d..5952518054 100644 --- a/LeanPool/Erdos132ThreeChain/Witnesses.lean +++ b/LeanPool/Erdos132ThreeChain/Witnesses.lean @@ -8,54 +8,17 @@ import LeanPool.Erdos132ThreeChain.Statement import Mathlib.Analysis.SpecialFunctions.Sqrt /-! -# Witnesses and the determinant form of the five-point obstruction +# Witnesses for the chain configurations -Two things are recorded here. - -First, the four-point catalogue is not vacuous: `rhombus_chain_config` and +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}`. - -Second, `symDet4_chain_five` records the determinant form of the five-point obstruction. The -doubled anchored Gram matrix of the only assignment that survives the four-point catalogue has -determinant `-27 * r ^ 4`, whereas `symDet4_dotp_eq_zero` shows that the Gram matrix of four -plane vectors is singular. `no_four_on_circle` proves the same obstruction in the -equivalent sum-of-squares form, which avoids having to enumerate principal minors at all. -/ namespace Erdos132ThreeChain -/-- The determinant of the symmetric `4 × 4` matrix with diagonal `d₁ d₂ d₃ d₄` and -off-diagonal entries `eᵢⱼ`. -/ -def symDet4 (d₁ d₂ d₃ d₄ e₁₂ e₁₃ e₁₄ e₂₃ e₂₄ e₃₄ : ℝ) : ℝ := - d₁ * d₂ * d₃ * d₄ - d₁ * d₂ * e₃₄ ^ 2 - d₁ * d₃ * e₂₄ ^ 2 - d₁ * d₄ * e₂₃ ^ 2 - + 2 * d₁ * e₂₃ * e₂₄ * e₃₄ - d₂ * d₃ * e₁₄ ^ 2 - d₂ * d₄ * e₁₃ ^ 2 - + 2 * d₂ * e₁₃ * e₁₄ * e₃₄ - d₃ * d₄ * e₁₂ ^ 2 + 2 * d₃ * e₁₂ * e₁₄ * e₂₄ - + 2 * d₄ * e₁₂ * e₁₃ * e₂₃ + e₁₂ ^ 2 * e₃₄ ^ 2 - 2 * e₁₂ * e₁₃ * e₂₄ * e₃₄ - - 2 * e₁₂ * e₁₄ * e₂₃ * e₃₄ + e₁₃ ^ 2 * e₂₄ ^ 2 - 2 * e₁₃ * e₁₄ * e₂₃ * e₂₄ - + e₁₄ ^ 2 * e₂₃ ^ 2 - -/-- The Gram matrix of four vectors of the plane is singular. -/ -theorem symDet4_dotp_eq_zero (o p q r s : Point) : - symDet4 (dotp o p p) (dotp o q q) (dotp o r r) (dotp o s s) (dotp o p q) (dotp o p r) - (dotp o p s) (dotp o q r) (dotp o q s) (dotp o r s) = 0 := by - simp only [symDet4, dotp]; ring - -/-- The doubled anchored Gram determinant of the only five-point assignment that survives the -four-point catalogue — a triangle of `3 * r` edges together with seven `r` edges — equals -`-27 * r ^ 4`. -/ -theorem symDet4_chain_five (r : ℝ) : - symDet4 (2 * r) (2 * r) (2 * r) (2 * r) r r r (-r) (-r) (-r) = -27 * r ^ 4 := by - simp only [symDet4]; ring - -theorem symDet4_chain_five_ne_zero {r : ℝ} (hr : 0 < r) : - symDet4 (2 * r) (2 * r) (2 * r) (2 * r) r r r (-r) (-r) (-r) ≠ 0 := by - rw [symDet4_chain_five] - have : (0 : ℝ) < r ^ 4 := by positivity - linarith - /-- 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. -/ @@ -82,10 +45,11 @@ theorem centroid_chain_config : simp only [sqDist, Prod.mk.injEq, ne_eq, not_and] <;> intros <;> nlinarith [h3, hpos] -/-- The rhombus witnesses that the definitions in the headline theorem are not vacuous: it is a -four-point set whose squared diameter is `3` and whose set of non-diameter squared distances is -exactly the one-term geometric 3-chain `{1}`. Thus `IsSqDiameter`, `nonDiameterSqDists` and -`chain` do realise the configuration that `threeChain_support_empty` forbids for `n ≥ 13`. -/ +/-- The rhombus is a four-point set whose squared diameter is `3` and whose non-diameter squared +distances form the one-term geometric 3-chain `{1}`, so it has `h = 1`. It therefore cannot +witness `threeChain_support_empty`, whose wrapper assumes `2 ≤ h`. Instead, it witnesses the +`h = 1` diameter and support data targeted by `nonDiameterSqDists_ne_chain`, while its four-point +cardinality deliberately fails that theorem's separate `n ≥ 13` hypothesis. -/ theorem rhombus_nonDiameter_support : ∃ X : Finset Point, X.card = 4 ∧ IsSqDiameter X 3 ∧ nonDiameterSqDists X 3 = chain 1 1 := by classical diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 3f9a66d261..df35872948 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -5795,12 +5795,12 @@ projects: 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 3-chain statement was produced - by the author's automated research pipeline in August 2026; the cited source poses the - ambient Erdos problem and states nothing about geometric 3-chains, and the result does - not resolve that problem, 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. + 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 From 3f1ae7b1372c7874eefb0cda9a6f1d4b7cf484b9 Mon Sep 17 00:00:00 2001 From: Egor Lyfar Date: Mon, 24 Aug 2026 18:22:57 +0800 Subject: [PATCH 3/4] docs: reword rhombus docstring to avoid naming the headline wrapper --- LeanPool/Erdos132ThreeChain/Witnesses.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanPool/Erdos132ThreeChain/Witnesses.lean b/LeanPool/Erdos132ThreeChain/Witnesses.lean index 5952518054..8a634024db 100644 --- a/LeanPool/Erdos132ThreeChain/Witnesses.lean +++ b/LeanPool/Erdos132ThreeChain/Witnesses.lean @@ -46,9 +46,9 @@ theorem centroid_chain_config : /-- The rhombus is a four-point set whose squared diameter is `3` and whose non-diameter squared -distances form the one-term geometric 3-chain `{1}`, so it has `h = 1`. It therefore cannot -witness `threeChain_support_empty`, whose wrapper assumes `2 ≤ h`. Instead, it witnesses the -`h = 1` diameter and support data targeted by `nonDiameterSqDists_ne_chain`, while its four-point +distances form the one-term geometric 3-chain `{1}`, so it has `h = 1`. The headline wrapper +assumes `2 ≤ h`, so the rhombus is not a witness for it. What it witnesses is the `h = 1` +diameter and support data targeted by `nonDiameterSqDists_ne_chain`, while its four-point cardinality deliberately fails that theorem's separate `n ≥ 13` hypothesis. -/ theorem rhombus_nonDiameter_support : ∃ X : Finset Point, X.card = 4 ∧ IsSqDiameter X 3 ∧ nonDiameterSqDists X 3 = chain 1 1 := by From e817c23b6fac12c5787f541498c4c26f10b8c139 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 24 Aug 2026 23:10:26 -0700 Subject: [PATCH 4/4] Optimize Erdos132ThreeChain witnesses --- LeanPool/Erdos132ThreeChain/Basic.lean | 15 ++++- LeanPool/Erdos132ThreeChain/HopfPannwitz.lean | 5 -- LeanPool/Erdos132ThreeChain/Statement.lean | 5 -- LeanPool/Erdos132ThreeChain/Witnesses.lean | 57 +------------------ LeanPool/projects.yml | 5 +- 5 files changed, 19 insertions(+), 68 deletions(-) diff --git a/LeanPool/Erdos132ThreeChain/Basic.lean b/LeanPool/Erdos132ThreeChain/Basic.lean index 0a6814eeb7..0bed03a21e 100644 --- a/LeanPool/Erdos132ThreeChain/Basic.lean +++ b/LeanPool/Erdos132ThreeChain/Basic.lean @@ -12,8 +12,9 @@ import Mathlib.Tactic.Ring /-! # Planar squared distances and geometric 3-chains -This file sets up the two elementary objects used throughout the project: points of the -Euclidean plane together with their squared distance, and the geometric 3-chain +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}` @@ -57,6 +58,11 @@ theorem sqDist_eq_zero_iff {p q : Point} : sqDist p q = 0 ↔ p = q := by 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} @@ -68,6 +74,11 @@ theorem base_mem_chain {a : ℝ} {h : ℕ} (hh : 0 < h) : a ∈ chain a h := 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 : ℕ`. -/ diff --git a/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean b/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean index d6742763da..ab46d78785 100644 --- a/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean +++ b/LeanPool/Erdos132ThreeChain/HopfPannwitz.lean @@ -37,11 +37,6 @@ namespace Erdos132ThreeChain open Finset -/-- `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 - /-- 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 diff --git a/LeanPool/Erdos132ThreeChain/Statement.lean b/LeanPool/Erdos132ThreeChain/Statement.lean index 43a8b36a20..f9ec76e6ca 100644 --- a/LeanPool/Erdos132ThreeChain/Statement.lean +++ b/LeanPool/Erdos132ThreeChain/Statement.lean @@ -38,11 +38,6 @@ namespace Erdos132ThreeChain open Finset -/-- 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} - /-- **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 diff --git a/LeanPool/Erdos132ThreeChain/Witnesses.lean b/LeanPool/Erdos132ThreeChain/Witnesses.lean index 8a634024db..5509c944fb 100644 --- a/LeanPool/Erdos132ThreeChain/Witnesses.lean +++ b/LeanPool/Erdos132ThreeChain/Witnesses.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Egor Lyfar -/ -import LeanPool.Erdos132ThreeChain.Statement +import LeanPool.Erdos132ThreeChain.Basic import Mathlib.Analysis.SpecialFunctions.Sqrt /-! @@ -45,54 +45,6 @@ theorem centroid_chain_config : simp only [sqDist, Prod.mk.injEq, ne_eq, not_and] <;> intros <;> nlinarith [h3, hpos] -/-- The rhombus is a four-point set whose squared diameter is `3` and whose non-diameter squared -distances form the one-term geometric 3-chain `{1}`, so it has `h = 1`. The headline wrapper -assumes `2 ≤ h`, so the rhombus is not a witness for it. What it witnesses is the `h = 1` -diameter and support data targeted by `nonDiameterSqDists_ne_chain`, while its four-point -cardinality deliberately fails that theorem's separate `n ≥ 13` hypothesis. -/ -theorem rhombus_nonDiameter_support : - ∃ X : Finset Point, X.card = 4 ∧ IsSqDiameter X 3 ∧ nonDiameterSqDists X 3 = chain 1 1 := by - classical - obtain ⟨A, B, C, D, hAB, hAC, hAD, hBC, hBD, hCD, dAB, dAC, dAD, dBC, dBD, dCD⟩ := - rhombus_chain_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 eDA : sqDist D A = 1 := by rw [sqDist_comm D A]; exact dAD - have eCB : sqDist C B = 1 := by rw [sqDist_comm C B]; exact dBC - have eDB : sqDist D B = 1 := by rw [sqDist_comm D B]; exact dBD - have eDC : sqDist D C = 3 := by rw [sqDist_comm D C]; exact dCD - have hmem : ∀ p ∈ ({A, B, C, D} : Finset Point), p = A ∨ p = B ∨ p = C ∨ p = D := by - intro p hp - simp only [Finset.mem_insert, Finset.mem_singleton] at hp - tauto - have hvals : ∀ p ∈ ({A, B, C, D} : Finset Point), ∀ q ∈ ({A, B, C, D} : Finset Point), - sqDist p q = 0 ∨ sqDist p q = 1 ∨ sqDist p q = 3 := by - intro p hp q hq - rcases hmem p hp with rfl | rfl | rfl | rfl <;> - rcases hmem q hq with rfl | rfl | rfl | rfl <;> - first - | exact Or.inl (sqDist_self _) - | exact Or.inr (Or.inl (by assumption)) - | exact Or.inr (Or.inr (by assumption)) - refine ⟨{A, B, C, D}, ?_, ⟨⟨C, by simp, D, by simp, hCD, dCD⟩, ?_⟩, ?_⟩ - · rw [Finset.card_insert_of_notMem (by simp [hAB, hAC, hAD]), - Finset.card_insert_of_notMem (by simp [hBC, hBD]), - Finset.card_insert_of_notMem (by simp [hCD]), Finset.card_singleton] - · intro p hp q hq - rcases hvals p hp q hq with 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 - · exact absurd (sqDist_eq_zero_iff.mp h) hpq - · exact ⟨0, by norm_num, by rw [h]; norm_num⟩ - · exact absurd h hne - · rintro ⟨j, hj, rfl⟩ - have hj0 : j = 0 := by omega - subst hj0 - exact ⟨A, by simp, B, by simp, hAB, by rw [dAB]; norm_num, by norm_num⟩ - - /-- 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. -/ @@ -137,11 +89,8 @@ theorem chainTwo_nonDiameter_support : 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 <;> - first - | exact Or.inl (sqDist_self _) - | exact Or.inr (Or.inl (by assumption)) - | exact Or.inr (Or.inr (Or.inl (by assumption))) - | exact Or.inr (Or.inr (Or.inr (by assumption))) + 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]), diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 0fc2f3e0f1..8fbd18dbd5 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -6131,9 +6131,10 @@ projects: authors: - Egor Lyfar source: - title: "Erdos Problem #132" + title: "Erdős Problem #132" authors: - - Paul Erdos + - Paul Erdős + - János Pach url: https://www.erdosproblems.com/132 github_repo: lyfar/lean-pool license: Apache-2.0