From 902d0aa05768062df076469a95d15f8ae99732b6 Mon Sep 17 00:00:00 2001 From: Egor Lyfar Date: Tue, 8 Sep 2026 13:16:46 +0800 Subject: [PATCH] Add rare-distance bounds over specified coordinate fields --- LeanPool.lean | 21 ++ LeanPool/RareDistanceFields.lean | 63 ++++++ .../RareDistanceFields/BinaryDescent.lean | 178 +++++++++++++++ .../RareDistanceFields/BinaryPalette.lean | 110 +++++++++ LeanPool/RareDistanceFields/BinarySize.lean | 135 +++++++++++ .../RareDistanceFields/BipartiteDiameter.lean | 186 +++++++++++++++ .../RareDistanceFields/DistancePattern.lean | 109 +++++++++ .../RareDistanceFields/DyadicCoordinates.lean | 106 +++++++++ LeanPool/RareDistanceFields/DyadicLevels.lean | 178 +++++++++++++++ LeanPool/RareDistanceFields/DyadicNorm.lean | 138 ++++++++++++ LeanPool/RareDistanceFields/DyadicSize.lean | 135 +++++++++++ .../RareDistanceFields/IntegerDivergence.lean | 105 +++++++++ LeanPool/RareDistanceFields/IntegerPlane.lean | 117 ++++++++++ .../RareDistanceFields/OctagonalDescent.lean | 58 +++++ .../RareDistanceFields/OctagonalNorm.lean | 211 ++++++++++++++++++ .../RareDistanceFields/OctagonalRational.lean | 154 +++++++++++++ .../RareDistanceFields/OrderedColors.lean | 118 ++++++++++ .../PolynomialSpecialization.lean | 148 ++++++++++++ .../PureTranscendental.lean | 144 ++++++++++++ .../RationalDivergence.lean | 168 ++++++++++++++ .../RareDistanceFields/RationalPlane.lean | 175 +++++++++++++++ LeanPool/RareDistanceFields/SplitCounts.lean | 80 +++++++ LeanPool/projects.yml | 85 +++++++ 23 files changed, 2922 insertions(+) create mode 100644 LeanPool/RareDistanceFields.lean create mode 100644 LeanPool/RareDistanceFields/BinaryDescent.lean create mode 100644 LeanPool/RareDistanceFields/BinaryPalette.lean create mode 100644 LeanPool/RareDistanceFields/BinarySize.lean create mode 100644 LeanPool/RareDistanceFields/BipartiteDiameter.lean create mode 100644 LeanPool/RareDistanceFields/DistancePattern.lean create mode 100644 LeanPool/RareDistanceFields/DyadicCoordinates.lean create mode 100644 LeanPool/RareDistanceFields/DyadicLevels.lean create mode 100644 LeanPool/RareDistanceFields/DyadicNorm.lean create mode 100644 LeanPool/RareDistanceFields/DyadicSize.lean create mode 100644 LeanPool/RareDistanceFields/IntegerDivergence.lean create mode 100644 LeanPool/RareDistanceFields/IntegerPlane.lean create mode 100644 LeanPool/RareDistanceFields/OctagonalDescent.lean create mode 100644 LeanPool/RareDistanceFields/OctagonalNorm.lean create mode 100644 LeanPool/RareDistanceFields/OctagonalRational.lean create mode 100644 LeanPool/RareDistanceFields/OrderedColors.lean create mode 100644 LeanPool/RareDistanceFields/PolynomialSpecialization.lean create mode 100644 LeanPool/RareDistanceFields/PureTranscendental.lean create mode 100644 LeanPool/RareDistanceFields/RationalDivergence.lean create mode 100644 LeanPool/RareDistanceFields/RationalPlane.lean create mode 100644 LeanPool/RareDistanceFields/SplitCounts.lean diff --git a/LeanPool.lean b/LeanPool.lean index aa0c8e6567..6c2efa3b16 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -3613,6 +3613,27 @@ import LeanPool.RamanujanNagell.Basic import LeanPool.RamanujanNagell.Helpers import LeanPool.RamanujanTauMissesPrimes import LeanPool.RamanujanTauMissesPrimes.Solution +import LeanPool.RareDistanceFields +import LeanPool.RareDistanceFields.BinaryDescent +import LeanPool.RareDistanceFields.BinaryPalette +import LeanPool.RareDistanceFields.BinarySize +import LeanPool.RareDistanceFields.BipartiteDiameter +import LeanPool.RareDistanceFields.DistancePattern +import LeanPool.RareDistanceFields.DyadicCoordinates +import LeanPool.RareDistanceFields.DyadicLevels +import LeanPool.RareDistanceFields.DyadicNorm +import LeanPool.RareDistanceFields.DyadicSize +import LeanPool.RareDistanceFields.IntegerDivergence +import LeanPool.RareDistanceFields.IntegerPlane +import LeanPool.RareDistanceFields.OctagonalDescent +import LeanPool.RareDistanceFields.OctagonalNorm +import LeanPool.RareDistanceFields.OctagonalRational +import LeanPool.RareDistanceFields.OrderedColors +import LeanPool.RareDistanceFields.PolynomialSpecialization +import LeanPool.RareDistanceFields.PureTranscendental +import LeanPool.RareDistanceFields.RationalDivergence +import LeanPool.RareDistanceFields.RationalPlane +import LeanPool.RareDistanceFields.SplitCounts import LeanPool.Redhill import LeanPool.Redhill.BB94 import LeanPool.Redhill.Common.Conjectures diff --git a/LeanPool/RareDistanceFields.lean b/LeanPool/RareDistanceFields.lean new file mode 100644 index 0000000000..0e6fd97f49 --- /dev/null +++ b/LeanPool/RareDistanceFields.lean @@ -0,0 +1,63 @@ +/- +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.RareDistanceFields.OctagonalRational +import LeanPool.RareDistanceFields.PureTranscendental + +/-! +# Rare-distance bounds over specified coordinate fields + +Source: url:https://www.erdosproblems.com/132 +Authors: Egor Lyfar +Status: verified +Main declarations: `LeanPool.RareDistanceFields.bounds` +Tags: discrete-geometry, distance-multiplicity, arithmetic-coordinates +MSC: 52C10, 11R11, 05C35 +-/ + +/-! +# Quantitative rare-distance bounds over specified coordinate fields + +For `n` distinct planar points, a rare distance is a positive occurring Euclidean +length with at most `n` unordered realizing pairs. This project proves `n ≤ 2^r`, +where `r` counts all such distances, for coordinates in `ℚ(√2)` and, separately, +in a real purely transcendental extension `ℚ(T)` of the rationals. The two +settings are not combined into an arbitrary algebraic extension of `ℚ(T)`. + +The quadratic-field proof constructs a binary descent model with a decreasing +integer height separate from actual Euclidean length. Exact polynomial +specialization transfers all distance equalities for the transcendental case. +The resulting bounds give two rare distances for `n ≥ 3` and at least `k` +when `n ≥ 2^k`. All multiplicities count complete unordered distance classes. + +## Source roles and formal dependencies + +Erdős problem 132 (https://www.erdosproblems.com/132) motivates these restricted +statements; the unrestricted conjecture is not proved here. Woodall +(DOI 10.1016/0097-3165(73)90020-4) and Madore (arXiv:1509.07023) provide +rational and quadratic-field coloring background, not the claimed +rare-distance bounds. The bounds and specialization are proved in this +project, without a claim that they are new mathematics. The Euclidean +angular-order lemmas are reused from `LeanPool.Erdos132N14.HopfPannwitzGeometry`; +no published-input hypothesis or conditional n=14 theorem is imported. +-/ + +namespace LeanPool.RareDistanceFields + +open Classical in +/-- The common quantitative bound, with the two coordinate regimes stated separately. -/ +theorem bounds {σ V : Type*} [Fintype V] : + (∀ x : V → ℂ, Function.Injective x → OctagonalRational.QuadraticCoordinates x → + Fintype.card V ≤ 2 ^ (OctagonalRational.rareDistances x).card) ∧ + (∀ (f : PureTranscendental.Functions σ →ₐ[ℚ] ℝ) + (x : V → PureTranscendental.Functions σ × PureTranscendental.Functions σ), + Function.Injective (PureTranscendental.point f x) → + Fintype.card V ≤ 2 ^ (DistancePattern.rareDistances + (PureTranscendental.point f x)).card) := + ⟨fun x hx h => OctagonalRational.card_le_pow_rareDistances x hx h, + fun f x hx => PureTranscendental.card_le_pow_rare f x hx⟩ + +end LeanPool.RareDistanceFields diff --git a/LeanPool/RareDistanceFields/BinaryDescent.lean b/LeanPool/RareDistanceFields/BinaryDescent.lean new file mode 100644 index 0000000000..6820219ce1 --- /dev/null +++ b/LeanPool/RareDistanceFields/BinaryDescent.lean @@ -0,0 +1,178 @@ +/- +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.RareDistanceFields.DyadicLevels + +/-! +# Binary descent with a height independent of Euclidean length + +See the project entry module for the exact coordinate restrictions and source roles. +The height controls termination and labels distance classes. The maximum +at each height valuation is taken in actual Euclidean distance. +-/ + +namespace LeanPool.RareDistanceFields.BinaryDescent + +open SplitCounts DyadicCoordinates +noncomputable section +universe u + +open Classical in +/-- A planar embedding with binary partitions and a height halved by descent. -/ +structure Model (P : Type*) where + /-- The complex embedding of the model. -/ + point : P → ℂ + point_injective : Function.Injective point + /-- An integer pair height determined by Euclidean distance. -/ + height : P → P → ℤ + height_nonneg : ∀ p q, 0 ≤ height p q + height_zero : ∀ p q, height p q = 0 ↔ p = q + distance_height : ∀ p q r s, dist (point p) (point q) = dist (point r) (point s) → + height p q = height r s + /-- The binary class assigned to each point. -/ + parity : P → ℤ + parity_values : ∀ p, parity p = 0 ∨ parity p = 1 + even_iff : ∀ p q, 2∣height p q ↔ parity p = parity q + /-- The descent map within a chosen binary class. -/ + half : ℤ → P → P + /-- The positive factor relating distances before and after descent. -/ + scale : ℝ + scale_pos : 0 < scale + half_height : ∀ e p q, parity p = e → parity q = e → height p q = 2 * height (half e p) (half e q) + half_distance : ∀ e p q, parity p = e → parity q = e → + dist (point p) (point q) = scale * dist (point (half e p)) (point (half e q)) + +namespace Model + +variable {P : Type*} (S : Model P) + +open Classical in +/-- Euclidean distance between the embedded model points. -/ +abbrev distance (p q : P) : ℝ := dist (S.point p) (S.point q) + +open Classical in +theorem height_pos (p q : P) (h : p ≠ q) : 0 < S.height p q := by + have hn := (S.height_zero p q).not.mpr h + have hp := S.height_nonneg p q + omega + +open Classical in +theorem bichromatic_count {A B : Type*} [Fintype A] [Fintype B] + (x : A → P) (y : B → P) (hx : Function.Injective x) (hy : Function.Injective y) + (d : ℝ) (hd : 0 < d) (hmax : ∀ a b, S.distance (x a) (y b) ≤ d) : + count (fun a b => S.distance (x a) (y b)) d ≤ Fintype.card A + Fintype.card B := by + have h := BipartiteDiameter.edges_card_le + (S.point ∘ x) (S.point ∘ y) (S.point_injective.comp hx) (S.point_injective.comp hy) hd hmax + simpa only [BipartiteDiameter.edges, Finset.card_filter, Fintype.sum_prod_type, count, + Function.comp_apply] using h + +open Classical in +theorem level_count (N : ℕ) : ∀ {V : Type u} [Fintype V] (x : V → P), + Function.Injective x → 0 < N → ∀ d : ℝ, 0 < d → + (∀ a b, S.distance (x a) (x b) = d → S.height (x a) (x b) = N) → + (∀ a b, a ≠ b → padicValInt 2 (S.height (x a) (x b)) = padicValInt 2 (N : ℤ) → + S.distance (x a) (x b) ≤ d) → + count (fun a b => S.distance (x a) (x b)) d ≤ 2 * Fintype.card V := by + induction N using Nat.strong_induction_on with + | h N ih => + intro V inst x hx hN d hd hclass hmax + let p : V → Prop := fun a => S.parity (x a) = 0 + let x0 : {a // p a} → P := fun a => x a.1 + let x1 : {a // ¬p a} → P := fun a => x a.1 + have hp0 (a : {a // p a}) : S.parity (x0 a) = 0 := a.2 + have hp1 (a : {a // ¬p a}) : S.parity (x1 a) = 1 := + (S.parity_values (x1 a)).resolve_left a.2 + have hcross (a : {a // p a}) (b : {a // ¬p a}) : ¬2∣S.height (x0 a) (x1 b) := by + rw [S.even_iff, hp0 a, hp1 b] + norm_num + have hreverse : count (fun a b => S.distance (x1 a) (x0 b)) d = + count (fun a b => S.distance (x0 a) (x1 b)) d := by + rw [count_symm] + simp only [distance, dist_comm] + have hsplit := count_split (fun a b => S.distance (x a) (x b)) d p + change count (fun a b => S.distance (x a) (x b)) d = + count (fun a b => S.distance (x0 a) (x0 b)) d + + count (fun a b => S.distance (x0 a) (x1 b)) d + + count (fun a b => S.distance (x1 a) (x0 b)) d + + count (fun a b => S.distance (x1 a) (x1 b)) d at hsplit + have hcards := card_split p + by_cases h2 : 2∣N + · obtain ⟨M, hNM⟩ := h2 + have hM : 0 < M := by omega + have hMN : M < N := by omega + have hNM' : (N : ℤ) = 2 * M := by exact_mod_cast hNM + have hc0 : count (fun a b => S.distance (x0 a) (x1 b)) d = 0 := by + apply count_zero + intro a b he + apply hcross a b + rw [hclass a.1 b.1 he, hNM'] + exact dvd_mul_right 2 (M : ℤ) + have hwithin {W : Type u} [Fintype W] (z : W → V) (hz : Function.Injective z) + (e : ℤ) (hpar : ∀ w, S.parity (x (z w)) = e) : + count (fun a b => S.distance (x (z a)) (x (z b))) d ≤ 2 * Fintype.card W := by + let y : W → P := fun w => S.half e (x (z w)) + have hs (a b : W) : S.height (x (z a)) (x (z b)) = 2 * S.height (y a) (y b) := + S.half_height e _ _ (hpar a) (hpar b) + have hdscale (a b : W) : S.distance (x (z a)) (x (z b)) = S.scale * S.distance (y a) (y + b) := + S.half_distance e _ _ (hpar a) (hpar b) + have hy : Function.Injective y := by + intro a b he + apply hz + apply hx + apply (S.height_zero _ _).mp + rw [hs, he, (S.height_zero _ _).mpr rfl, mul_zero] + have heq (a b : W) : S.distance (x (z a)) (x (z b)) = d ↔ + S.distance (y a) (y b) = d / S.scale := by + rw [hdscale, eq_div_iff (ne_of_gt S.scale_pos), mul_comm] + have hcy (a b : W) (he : S.distance (y a) (y b) = d / S.scale) : + S.height (y a) (y b) = M := by + have hh := hclass (z a) (z b) ((heq a b).mpr he) + rw [hs, hNM'] at hh + omega + have hby (a b : W) (hab : a ≠ b) + (hv : padicValInt 2 (S.height (y a) (y b)) = padicValInt 2 (M : ℤ)) : + S.distance (y a) (y b) ≤ d / S.scale := by + have hn := (S.height_zero _ _).not.mpr (hy.ne hab) + have hnM : (M : ℤ) ≠ 0 := by exact_mod_cast ne_of_gt hM + have hh := hmax (z a) (z b) (hz.ne hab) (by + rw [hs, hNM', valuation_double _ hn, valuation_double _ hnM, hv]) + rw [hdscale] at hh + apply (le_div_iff₀ S.scale_pos).mpr + simpa only [mul_comm] using hh + have hh := ih M hMN y hy hM (d / S.scale) (div_pos hd S.scale_pos) hcy hby + exact (count_congr _ _ d (d / S.scale) heq) ▸ hh + have h0 := hwithin (fun a : {a // p a} => a.1) Subtype.val_injective 0 hp0 + have h1 := hwithin (fun a : {a // ¬p a} => a.1) Subtype.val_injective 1 hp1 + change count (fun a b => S.distance (x0 a) (x0 b)) d ≤ + 2 * Fintype.card {a // p a} at h0 + change count (fun a b => S.distance (x1 a) (x1 b)) d ≤ + 2 * Fintype.card {a // ¬p a} at h1 + rw [hreverse, hc0] at hsplit + omega + · have hnN : (N : ℤ) ≠ 0 := by exact_mod_cast ne_of_gt hN + have h2' : ¬(2 : ℤ)∣N := by exact_mod_cast h2 + have hvN := (valuation_zero_iff (N : ℤ) hnN).mpr h2' + have hwithin {W : Type u} [Fintype W] (z : W → V) (e : ℤ) + (he : ∀ w, S.parity (x (z w)) = e) : + count (fun a b => S.distance (x (z a)) (x (z b))) d = 0 := by + apply count_zero + intro a b hab + apply h2' + rw [←hclass (z a) (z b) hab, S.even_iff, he a, he b] + have h0 := hwithin (fun a : {a // p a} => a.1) 0 hp0 + have h1 := hwithin (fun a : {a // ¬p a} => a.1) 1 hp1 + have hbound (a : {a // p a}) (b : {a // ¬p a}) : S.distance (x0 a) (x1 b) ≤ d := by + have hab : a.1 ≠ b.1 := by intro h; exact b.2 (h ▸ a.2) + have hn := (S.height_zero _ _).not.mpr (hx.ne hab) + exact hmax a.1 b.1 hab (by rw [(valuation_zero_iff _ hn).mpr (hcross a b), hvN]) + have hc := S.bichromatic_count x0 x1 (hx.comp Subtype.val_injective) + (hx.comp Subtype.val_injective) d hd hbound + rw [hreverse, h0, h1] at hsplit + omega + +end Model +end +end LeanPool.RareDistanceFields.BinaryDescent diff --git a/LeanPool/RareDistanceFields/BinaryPalette.lean b/LeanPool/RareDistanceFields/BinaryPalette.lean new file mode 100644 index 0000000000..9b95681bf8 --- /dev/null +++ b/LeanPool/RareDistanceFields/BinaryPalette.lean @@ -0,0 +1,110 @@ +/- +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.RareDistanceFields.BinarySize + +/-! +# Actual rare distances from binary descent heights + +See the project entry module for the exact coordinate restrictions and source roles. +Every occupied height valuation supplies a different actual Euclidean rare +class. Together with binary size descent this gives n <= 2^r. +-/ + +namespace LeanPool.RareDistanceFields.BinaryPalette + +open BinaryDescent BinarySize SplitCounts +noncomputable section + +variable {P V : Type*} [Fintype V] (S : Model P) + +open Classical in +/-- The simple graph joining distinct labels at the specified model distance. -/ +def graph (x : V → P) (d : ℝ) : SimpleGraph V := + OrderedColors.colorGraph (fun a b => S.distance (x a) (x b)) + (fun _ _ => dist_comm _ _) d + +open Classical in +/-- Occurring model distances whose full edge counts are at most the label count. -/ +def rareDistances (x : V → P) : Finset ℝ := + (OrderedColors.palette (fun a b => S.distance (x a) (x b))).filter + fun d => (graph S x d).edgeFinset.card ≤ Fintype.card V + +open Classical in +/-- The 2-adic height level of a realizing pair, or zero when the distance is absent. -/ +def distanceLevel (x : V → P) (d : ℝ) : ℕ := + if h : ∃ e : V × V, S.distance (x e.1) (x e.2) = d then + padicValInt 2 (S.height (x (Classical.choose h).1) (x (Classical.choose h).2)) else 0 + +open Classical in +theorem distanceLevel_eq (x : V → P) (a b : V) : + distanceLevel S x (S.distance (x a) (x b)) = padicValInt 2 (S.height (x a) (x b)) := by + have h : ∃ e : V × V, S.distance (x e.1) (x e.2) = S.distance (x a) (x b) := ⟨(a, b), rfl⟩ + rw [distanceLevel, dite_eq_left h] + rw [S.distance_height _ _ _ _ (Classical.choose_spec h)] + +open Classical in +theorem level_max_rare (x : V → P) (hx : Function.Injective x) (i j : V) (hij : i ≠ j) + (hmax : ∀ a b, a ≠ b → padicValInt 2 (S.height (x a) (x b)) = + padicValInt 2 (S.height (x i) (x j)) → S.distance (x a) (x b) ≤ S.distance (x i) (x j)) : + S.distance (x i) (x j) ∈ rareDistances S x := by + have hp := S.height_pos _ _ (hx.ne hij) + have hcast : ((S.height (x i) (x j)).toNat : ℤ) = S.height (x i) (x j) := Int.toNat_of_nonneg + hp.le + have hd : 0 < S.distance (x i) (x j) := dist_pos.mpr (S.point_injective.ne (hx.ne hij)) + have hc := S.level_count (S.height (x i) (x j)).toNat x hx (by omega) + (S.distance (x i) (x j)) hd + (fun a b he => (S.distance_height _ _ _ _ he).trans hcast.symm) + (by simpa only [hcast] using hmax) + have he := count_eq_twice_edges (fun a b => S.distance (x a) (x b)) + (fun _ _ => dist_comm _ _) (S.distance (x i) (x j)) (fun _ => by simpa using ne_of_lt hd) + change _ = 2 * (graph S x (S.distance (x i) (x j))).edgeFinset.card at he + apply Finset.mem_filter.mpr + refine ⟨Finset.mem_image.mpr ⟨(i, j), by simp [hij], rfl⟩, ?_⟩ + omega + +open Classical in +theorem rare_at_level (x : V → P) (hx : Function.Injective x) {k : ℕ} + (hk : k ∈ levels S x) : ∃ d ∈ rareDistances S x, distanceLevel S x d = k := by + let pairs := (Finset.univ : Finset (V × V)).filter + fun e => e.1 ≠ e.2 ∧ padicValInt 2 (S.height (x e.1) (x e.2)) = k + have hp : pairs.Nonempty := by + obtain ⟨⟨a, b⟩, hab, he⟩ := Finset.mem_image.mp hk + exact ⟨(a, b), by simpa [pairs] using And.intro (Finset.mem_offDiag.mp hab).2.2 he⟩ + obtain ⟨e, he, hem⟩ := pairs.exists_max_image (fun e => S.distance (x e.1) (x e.2)) hp + have hed := (Finset.mem_filter.mp he).2 + refine ⟨S.distance (x e.1) (x e.2), level_max_rare S x hx _ _ hed.1 ?_, ?_⟩ + · intro a b hab hl + exact hem (a, b) (by simp [pairs, hab, hl, hed.2]) + · rw [distanceLevel_eq, hed.2] + +open Classical in +theorem card_le_pow_rareDistances (x : V → P) (hx : Function.Injective x) : + Fintype.card V ≤ 2 ^ (rareDistances S x).card := by + have hsub : levels S x ⊆ (rareDistances S x).image (distanceLevel S x) := by + intro k hk + obtain ⟨d, hd, hk⟩ := rare_at_level S x hx hk + exact Finset.mem_image.mpr ⟨d, hd, hk⟩ + have hcard : (levels S x).card ≤ (rareDistances S x).card := + (Finset.card_le_card hsub).trans Finset.card_image_le + exact (card_le_pow_levels S x hx).trans (Nat.pow_le_pow_right (by decide) hcard) + +open Classical in +theorem rareDistances_spec (x : V → P) (hx : Function.Injective x) (d : ℝ) : + d ∈ rareDistances S x ↔ 0 < d ∧ (∃ a b, a ≠ b ∧ S.distance (x a) (x b) = d) ∧ + (graph S x d).edgeFinset.card ≤ Fintype.card V := by + constructor + · intro h + obtain ⟨hp, hc⟩ := Finset.mem_filter.mp h + obtain ⟨⟨a, b⟩, hab, he⟩ := Finset.mem_image.mp hp + have hn : a ≠ b := (Finset.mem_offDiag.mp hab).2.2 + refine ⟨?_, ⟨a, b, hn, he⟩, hc⟩ + rw [←he] + exact dist_pos.mpr (S.point_injective.ne (hx.ne hn)) + · rintro ⟨_, ⟨a, b, hab, he⟩, hc⟩ + exact Finset.mem_filter.mpr ⟨Finset.mem_image.mpr ⟨(a, b), by simp [hab], he⟩, hc⟩ + +end +end LeanPool.RareDistanceFields.BinaryPalette diff --git a/LeanPool/RareDistanceFields/BinarySize.lean b/LeanPool/RareDistanceFields/BinarySize.lean new file mode 100644 index 0000000000..d2659323f9 --- /dev/null +++ b/LeanPool/RareDistanceFields/BinarySize.lean @@ -0,0 +1,135 @@ +/- +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.RareDistanceFields.BinaryDescent + +/-! +# Binary size bound for a separate integral descent height + +See the project entry module for the exact coordinate restrictions and source roles. +A binary descent model with k occupied height valuations has at most 2^k points. +The induction height need not equal or increase with Euclidean distance. +-/ + +namespace LeanPool.RareDistanceFields.BinarySize + +open BinaryDescent DyadicCoordinates SplitCounts +noncomputable section +universe u + +variable {P : Type*} (S : Model P) + +open Classical in +theorem card_le_pow_of_bound (M : ℕ) : ∀ {V : Type u} [Fintype V] + (x : V → P), Function.Injective x → ∀ L : Finset ℕ, + (∀ a b, S.height (x a) (x b) ≤ M) → + (∀ a b, a ≠ b → padicValInt 2 (S.height (x a) (x b)) ∈ L) → + Fintype.card V ≤ 2 ^ L.card := by + classical + induction M using Nat.strong_induction_on with + | h M ih => + intro V inst x hx L hbound hL + by_cases hM : M = 0 + · have hc : Fintype.card V ≤ 1 := by + apply Fintype.card_le_one_iff.mpr + intro a b + apply hx + apply (S.height_zero _ _).mp + have hh := hbound a b + have hn : 0 ≤ S.height (x a) (x b) := by + exact S.height_nonneg _ _ + rw [hM] at hh + omega + exact hc.trans (Nat.one_le_pow _ _ (by decide)) + have hMpos : 0 < M := by omega + have hsmaller : M / 2 < M := Nat.div_lt_self hMpos (by decide) + let p : V → Prop := fun a => S.parity (x a) = 0 + let L' : Finset ℕ := (L.erase 0).image Nat.pred + have hcardL : L'.card ≤ (L.erase 0).card := Finset.card_image_le + have hcardL' : L'.card ≤ L.card := hcardL.trans (Finset.card_le_card (Finset.erase_subset _ _)) + have hpow : 2 ^ L'.card ≤ 2 ^ L.card := Nat.pow_le_pow_right (by decide) hcardL' + have hwithin {W : Type u} [Fintype W] (z : W → V) (hz : Function.Injective z) + (e : ℤ) (hpar : ∀ w, S.parity (x (z w)) = e) : Fintype.card W ≤ 2 ^ L'.card := by + let y : W → P := fun w => S.half e (x (z w)) + have hscale (a b : W) : S.height (x (z a)) (x (z b)) = 2 * S.height (y a) (y b) := + S.half_height e _ _ (hpar a) (hpar b) + have hy : Function.Injective y := by + intro a b he + apply hz + apply hx + apply (S.height_zero _ _).mp + rw [hscale, he, (S.height_zero _ _).mpr rfl, mul_zero] + apply ih (M / 2) hsmaller y hy L' + · intro a b + have hh := hbound (z a) (z b) + rw [hscale] at hh + rw [Int.natCast_ediv] + omega + · intro a b hab + have hn := (S.height_zero (y a) (y b)).not.mpr (hy.ne hab) + have hs : padicValInt 2 (S.height (x (z a)) (x (z b))) = + 1 + padicValInt 2 (S.height (y a) (y b)) := by rw [hscale, valuation_double _ hn] + apply Finset.mem_image.mpr + refine ⟨padicValInt 2 (S.height (x (z a)) (x (z b))), ?_, ?_⟩ + · apply Finset.mem_erase.mpr + exact ⟨by omega, hL (z a) (z b) (hz.ne hab)⟩ + · rw [hs] + simp + have h0 := hwithin (fun a : {a // p a} => a.1) Subtype.val_injective 0 (fun a => a.2) + have h1 := hwithin (fun a : {a // ¬p a} => a.1) Subtype.val_injective 1 + (fun a => (S.parity_values (x a.1)).resolve_left a.2) + have hcards := card_split p + by_cases hz : 0 ∈ L + · have hLpos : 0 < L.card := Finset.card_pos.mpr ⟨0, hz⟩ + rw [Finset.card_erase_of_mem hz] at hcardL + have hp : 2 * 2 ^ L'.card ≤ 2 ^ L.card := by + calc + 2 * 2 ^ L'.card = 2 ^ (L'.card + 1) := by rw [pow_succ]; omega + _ ≤ 2 ^ L.card := Nat.pow_le_pow_right (by decide) (by omega) + omega + · by_cases h0empty : Fintype.card {a // p a} = 0 + · omega + · have h0pos : 0 < Fintype.card {a // p a} := by omega + obtain ⟨a⟩ := Fintype.card_pos_iff.mp h0pos + have hempty : IsEmpty {b // ¬p b} := by + constructor + intro b + have hab : a.1 ≠ b.1 := by intro h; exact b.2 (h ▸ a.2) + have hpar : S.parity (x b.1) = 1 := (S.parity_values _).resolve_left b.2 + have hn := (S.height_zero (x a.1) (x b.1)).not.mpr (hx.ne hab) + have hodd : ¬2 ∣ S.height (x a.1) (x b.1) := by + rw [S.even_iff, a.2, hpar] + norm_num + have hv := (valuation_zero_iff _ hn).mpr hodd + exact hz (hv ▸ hL a.1 b.1 hab) + have he : Fintype.card {a // ¬p a} = 0 := Fintype.card_eq_zero + omega + +open Classical in +/-- The 2-adic height levels realized between distinct configuration labels. -/ +def levels {V : Type*} [Fintype V] (x : V → P) : Finset ℕ := + Finset.univ.offDiag.image (fun ab => padicValInt 2 (S.height (x ab.1) (x ab.2))) + +open Classical in +theorem mem_levels {V : Type*} [Fintype V] (x : V → P) (a b : V) (hab : a ≠ b) : + padicValInt 2 (S.height (x a) (x b)) ∈ levels S x := by + exact Finset.mem_image.mpr ⟨(a, b), by simp [hab], rfl⟩ + +open Classical in +theorem card_le_pow_levels {V : Type*} [Fintype V] (x : V → P) + (hx : Function.Injective x) : Fintype.card V ≤ 2 ^ (levels S x).card := by + classical + let M := (Finset.univ : Finset (V × V)).sup (fun ab => (S.height (x ab.1) (x ab.2)).toNat) + apply card_le_pow_of_bound S M x hx (levels S x) + · intro a b + have hn : 0 ≤ S.height (x a) (x b) := by + exact S.height_nonneg _ _ + have hh : (S.height (x a) (x b)).toNat ≤ M := + Finset.le_sup (f := fun ab => (S.height (x ab.1) (x ab.2)).toNat) (Finset.mem_univ (a, b)) + omega + · exact mem_levels S x + +end +end LeanPool.RareDistanceFields.BinarySize diff --git a/LeanPool/RareDistanceFields/BipartiteDiameter.lean b/LeanPool/RareDistanceFields/BipartiteDiameter.lean new file mode 100644 index 0000000000..c0f8f44295 --- /dev/null +++ b/LeanPool/RareDistanceFields/BipartiteDiameter.lean @@ -0,0 +1,186 @@ +/- +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.Erdos132N14.HopfPannwitzGeometry + +/-! +# Bichromatic maximal distances + +See the project entry module for the exact coordinate restrictions and source roles. +For two finite planar point sets, the number of pairs attaining their positive +cross-distance maximum is at most the sum of their cardinalities. The charging +proof treats singleton color classes and antipodal rays explicitly. +-/ + +namespace LeanPool.RareDistanceFields.BipartiteDiameter + +open LeanPool.Erdos132N14 +noncomputable section + +open Classical in +theorem normSq_sub_of_dist_eq {a b : ℂ} {d : ℝ} (h : dist a b = d) : + Complex.normSq (b - a) = d ^ 2 := by + rw [Complex.normSq_eq_norm_sq] + have hn : ‖b - a‖ = d := by simpa [Complex.dist_eq, norm_sub_rev] using h + rw [hn] + +open Classical in +theorem normSq_sub_of_dist_le {a b : ℂ} {d : ℝ} (hd : 0 ≤ d) (h : dist a b ≤ d) : + Complex.normSq (b - a) ≤ d ^ 2 := by + rw [Complex.normSq_eq_norm_sq] + have hn : ‖b - a‖ ≤ d := by simpa [Complex.dist_eq, norm_sub_rev] using h + exact (sq_le_sq₀ (norm_nonneg _) hd).mpr hn + +open Classical in +/-- A second center excludes distinct antipodal equal rays. -/ +theorem equal_rays_of_second_center {u v w a : ℂ} {d : ℝ} + (huv : dist u v = d) (huw : dist u w = d) (hd : 0 < d) + (hav : dist a v ≤ d) (haw : dist a w ≤ d) (hau : a ≠ u) + (hc : planeCross (v - u) (w - u) = 0) : v = w := by + let x := v - u + let y := w - u + let z := a - u + have hx : diameterDot x x = d ^ 2 := by rw [planeDot_self]; exact normSq_sub_of_dist_eq huv + have hy : diameterDot y y = d ^ 2 := by rw [planeDot_self]; exact normSq_sub_of_dist_eq huw + have hxy : (diameterDot x y) ^ 2 = (d ^ 2) ^ 2 := by + have h := plane_lagrange x y y + rw [hc, mul_zero, add_zero, hx, hy] at h + simpa [pow_two] using h.symm + rcases sq_eq_sq_iff_eq_or_eq_neg.mp hxy with hplus|hminus + · have hn : Complex.normSq (y - x) = 0 := by + simp only [Complex.normSq_apply, Complex.sub_re, Complex.sub_im] + simp only [diameterDot] at hx hy hplus + nlinarith + have he := sub_eq_zero.mp (Complex.normSq_eq_zero.mp hn) + dsimp [x, y] at he + exact sub_left_injective he.symm + · have hn : Complex.normSq (y + x) = 0 := by + simp only [Complex.normSq_apply, Complex.add_re, Complex.add_im] + simp only [diameterDot] at hx hy hminus + nlinarith + have he : y = -x := eq_neg_of_add_eq_zero_left (Complex.normSq_eq_zero.mp hn) + have hzv : Complex.normSq (x - z) ≤ d ^ 2 := by + have h := normSq_sub_of_dist_le hd.le hav + convert h using 1; dsimp [x, z]; congr 1; ring + have hzw : Complex.normSq (y - z) ≤ d ^ 2 := by + have h := normSq_sub_of_dist_le hd.le haw + convert h using 1; dsimp [y, z]; congr 1; ring + rw [he] at hzw + have hz : Complex.normSq z = 0 := by + simp only [Complex.normSq_apply, Complex.sub_re, Complex.sub_im, + Complex.neg_re, Complex.neg_im] at hzv hzw ⊢ + simp only [diameterDot] at hx + nlinarith [sq_nonneg z.re, sq_nonneg z.im] + exact False.elim (hau (sub_eq_zero.mp (Complex.normSq_eq_zero.mp hz))) + +variable {A B : Type*} [Fintype A] [Fintype B] + +open Classical in +/-- All cross-color label pairs realizing the specified Euclidean distance. -/ +def edges (a : A → ℂ) (b : B → ℂ) (d : ℝ) : Finset (A × B) := + Finset.univ.filter fun e => dist (a e.1) (b e.2) = d + +open Classical in +/-- All equal-length rays at the left endpoint turn nonnegatively from this edge. -/ +def leftExtreme (a : A → ℂ) (b : B → ℂ) (d : ℝ) (e : A × B) : Prop := + ∀ j, dist (a e.1) (b j) = d → 0 ≤ planeTurn (a e.1) (b e.2) (b j) + +open Classical in +/-- All equal-length rays at the right endpoint turn nonnegatively from this edge. -/ +def rightExtreme (a : A → ℂ) (b : B → ℂ) (d : ℝ) (e : A × B) : Prop := + ∀ i, dist (a i) (b e.2) = d → 0 ≤ planeTurn (b e.2) (a e.1) (a i) + +omit [Fintype A] [Fintype B] in +open Classical in +theorem extreme_at_endpoint (a : A → ℂ) (b : B → ℂ) {d : ℝ} (hd : 0 < d) + (hmax : ∀ i j, dist (a i) (b j) ≤ d) (e : A × B) + (he : dist (a e.1) (b e.2) = d) : + leftExtreme a b d e ∨ rightExtreme a b d e := by + by_contra h + have hl : ¬ leftExtreme a b d e := fun h' => h (Or.inl h') + have hr : ¬ rightExtreme a b d e := fun h' => h (Or.inr h') + simp only [leftExtreme, not_forall, not_le] at hl + simp only [rightExtreme, not_forall, not_le] at hr + obtain ⟨j, hj, htj⟩ := hl + obtain ⟨i, hi, hti⟩ := hr + have hh := opposite_turns_force_longer_pair he hj (by simpa only [dist_comm] using hi) hd htj hti + have hm := hmax i j + rw [dist_comm] at hh + linarith + +omit [Fintype A] [Fintype B] in +open Classical in +theorem left_unique (a : A → ℂ) (b : B → ℂ) (hb : Function.Injective b) + {d : ℝ} (hd : 0 < d) (hmax : ∀ i j, dist (a i) (b j) ≤ d) + (hother : ∀ i, ∃ i', a i' ≠ a i) {i : A} {j k : B} + (hj : dist (a i) (b j) = d) (hk : dist (a i) (b k) = d) + (hle : leftExtreme a b d (i, j)) (hke : leftExtreme a b d (i, k)) : j = k := by + apply hb + obtain ⟨i', hi'⟩ := hother i + apply equal_rays_of_second_center hj hk hd (hmax i' j) (hmax i' k) hi' + have h1 := hle k hk + have h2 := hke j hj + rw [planeTurn_swap] at h2 + change planeTurn (a i) (b j) (b k) = 0 + linarith + +open Classical in +/-- The complete bipartite maximum-distance bound, with no position assumption. -/ +theorem edges_card_le (a : A → ℂ) (b : B → ℂ) + (ha : Function.Injective a) (hb : Function.Injective b) {d : ℝ} + (hd : 0 < d) (hmax : ∀ i j, dist (a i) (b j) ≤ d) : + (edges a b d).card ≤ Fintype.card A + Fintype.card B := by + by_cases hA : Fintype.card A ≤ 1 + · calc + (edges a b d).card ≤ Fintype.card A * Fintype.card B := by + simpa [edges] using Finset.card_le_card (Finset.filter_subset (fun e : A × B => dist (a + e.1) (b e.2) = d) Finset.univ) + _ ≤ Fintype.card B := by nlinarith + _ ≤ _ := Nat.le_add_left _ _ + by_cases hB : Fintype.card B ≤ 1 + · calc + (edges a b d).card ≤ Fintype.card A * Fintype.card B := by + simpa [edges] using Finset.card_le_card (Finset.filter_subset (fun e : A × B => dist (a + e.1) (b e.2) = d) Finset.univ) + _ ≤ Fintype.card A := by nlinarith + _ ≤ _ := Nat.le_add_right _ _ + have hotherA (i : A) : ∃ i', a i' ≠ a i := by + have : Nontrivial A := Fintype.one_lt_card_iff_nontrivial.mp (by omega) + obtain ⟨i', hi'⟩ := exists_ne i + exact ⟨i', ha.ne hi'⟩ + have hotherB (j : B) : ∃ j', b j' ≠ b j := by + have : Nontrivial B := Fintype.one_lt_card_iff_nontrivial.mp (by omega) + obtain ⟨j', hj'⟩ := exists_ne j + exact ⟨j', hb.ne hj'⟩ + let owner : A × B → A ⊕ B := fun e => + if leftExtreme a b d e then Sum.inl e.1 else Sum.inr e.2 + have hinj : Set.InjOn owner (edges a b d) := by + intro e he f hf hef + have he' : dist (a e.1) (b e.2) = d := (Finset.mem_filter.mp he).2 + have hf' : dist (a f.1) (b f.2) = d := (Finset.mem_filter.mp hf).2 + dsimp [owner] at hef + by_cases hl : leftExtreme a b d e <;> by_cases hr : leftExtreme a b d f + all_goals simp only [hl, hr, ite_true, ite_false, Sum.inl.injEq, Sum.inr.injEq, + Sum.inl_ne_inr, Sum.inr_ne_inl] at hef + · have hfirst : e.1 = f.1 := hef + apply Prod.ext hfirst + apply left_unique a b hb hd hmax hotherA he' + · simpa [hfirst] using hf' + · exact hl + · simpa [hfirst] using hr + · have hsecond : e.2 = f.2 := hef + have heR := (extreme_at_endpoint a b hd hmax e he').resolve_left hl + have hfR := (extreme_at_endpoint a b hd hmax f hf').resolve_left hr + apply Prod.ext ?_ hsecond + apply left_unique b a ha hd (fun j i => by simpa [dist_comm] using hmax i j) + hotherB (by simpa [dist_comm] using he') + · simpa [dist_comm, hsecond] using hf' + · simpa [leftExtreme, rightExtreme, dist_comm] using heR + · simpa [leftExtreme, rightExtreme, dist_comm, hsecond] using hfR + have hcard := Finset.card_le_card_of_injOn owner (fun _ _ => Finset.mem_univ _) hinj + simpa using hcard + +end +end LeanPool.RareDistanceFields.BipartiteDiameter diff --git a/LeanPool/RareDistanceFields/DistancePattern.lean b/LeanPool/RareDistanceFields/DistancePattern.lean new file mode 100644 index 0000000000..1c25ac70e0 --- /dev/null +++ b/LeanPool/RareDistanceFields/DistancePattern.lean @@ -0,0 +1,109 @@ +/- +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.RareDistanceFields.RationalDivergence + +/-! +# Transport by the exact distance-equality pattern + +See the project entry module for the exact coordinate restrictions and source roles. +A rational planar realization of the same equality pattern transports each +whole distance class, including its unordered multiplicity. No approximation +argument and no assumption that arbitrary configurations admit such a +realization are used. +-/ + +namespace LeanPool.RareDistanceFields.DistancePattern + +open RationalPlane +noncomputable section + +variable {V : Type*} [Fintype V] + +open Classical in +/-- The simple graph of all distinct label pairs at a given Euclidean distance. -/ +def graph (x : V → ℂ) (d : ℝ) : SimpleGraph V := + OrderedColors.colorGraph (fun a b => dist (x a) (x b)) + (fun _ _ => dist_comm _ _) d + +open Classical in +/-- Occurring distances whose full unordered multiplicities are at most the label count. -/ +def rareDistances (x : V → ℂ) : Finset ℝ := + (OrderedColors.palette (fun a b => dist (x a) (x b))).filter + fun d => (graph x d).edgeFinset.card ≤ Fintype.card V + +open Classical in +/-- Rational squared-distance equality agrees exactly with real distance equality. -/ +def SamePattern (y : V → Point) (x : V → ℂ) : Prop := + ∀ a b c d, sqDist (y a) (y b) = sqDist (y c) (y d) ↔ + dist (x a) (x b) = dist (x c) (x d) + +omit [Fintype V] in +open Classical in +theorem rational_injective (y : V → Point) (x : V → ℂ) + (hx : Function.Injective x) (hp : SamePattern y x) : Function.Injective y := by + intro a b hab + apply hx + have h := (hp a b a a).mp (by rw [hab]) + simpa using h + +open Classical in +theorem rare_card_transport (y : V → Point) (x : V → ℂ) (hp : SamePattern y x) : + (RationalDivergence.rareSquared y).card ≤ (rareDistances x).card := by + classical + let f : ℚ → ℝ := fun r => + if h : ∃ a b, sqDist (y a) (y b) = r then + dist (x h.choose) (x h.choose_spec.choose) else 0 + have hf (a b : V) : f (sqDist (y a) (y b)) = dist (x a) (x b) := by + dsimp [f] + split_ifs with h + · exact (hp _ _ _ _).mp h.choose_spec.choose_spec + · exact False.elim (h ⟨a, b, rfl⟩) + have hg (a b : V) : RationalPlane.graph y (sqDist (y a) (y b)) = + graph x (dist (x a) (x b)) := by + ext c d + simp only [RationalPlane.graph, graph, OrderedColors.colorGraph, hp c d a b] + apply Finset.card_le_card_of_injOn f + · intro r hr + obtain ⟨a, b, hab, rfl⟩ := RationalDivergence.exists_pair_of_mem_rareSquared y hr + rw [hf] + apply Finset.mem_filter.mpr + refine ⟨Finset.mem_image.mpr ⟨(a, b), by simp [hab], rfl⟩, ?_⟩ + exact hg a b ▸ (Finset.mem_filter.mp hr).2 + · intro r hr s hs he + obtain ⟨a, b, _hab, rfl⟩ := RationalDivergence.exists_pair_of_mem_rareSquared y hr + obtain ⟨c, d, _hcd, rfl⟩ := RationalDivergence.exists_pair_of_mem_rareSquared y hs + rw [hf, hf] at he + exact (hp a b c d).mpr he + +open Classical in +theorem card_le_pow_rare (y : V → Point) (x : V → ℂ) + (hx : Function.Injective x) (hp : SamePattern y x) : + Fintype.card V ≤ 2 ^ (rareDistances x).card := + (RationalDivergence.card_le_pow_rareSquared y (rational_injective y x hx hp)).trans + (Nat.pow_le_pow_right (by decide) (rare_card_transport y x hp)) + +open Classical in +theorem rareDistances_spec (x : V → ℂ) (hx : Function.Injective x) + {d : ℝ} (hd : d ∈ rareDistances x) : 0 < d ∧ + (∃ a b, dist (x a) (x b) = d) ∧ (graph x d).edgeFinset.card ≤ Fintype.card V := by + obtain ⟨hp, hm⟩ := Finset.mem_filter.mp hd + obtain ⟨⟨a, b⟩, hab, rfl⟩ := Finset.mem_image.mp hp + exact ⟨dist_pos.mpr (hx.ne (Finset.mem_offDiag.mp hab).2.2), ⟨a, b, rfl⟩, hm⟩ + +open Classical in +theorem two_rare_distances (y : V → Point) (x : V → ℂ) + (hx : Function.Injective x) (hp : SamePattern y x) (hn : 3 ≤ Fintype.card V) : + ∃ d ∈ rareDistances x, ∃ e ∈ rareDistances x, d ≠ e := by + apply Finset.one_lt_card.mp + have h := card_le_pow_rare y x hx hp + by_contra hr + have hp' : 2 ^ (rareDistances x).card ≤ 2 ^ 1 := + Nat.pow_le_pow_right (by decide) (by omega) + norm_num at hp' + omega + +end +end LeanPool.RareDistanceFields.DistancePattern diff --git a/LeanPool/RareDistanceFields/DyadicCoordinates.lean b/LeanPool/RareDistanceFields/DyadicCoordinates.lean new file mode 100644 index 0000000000..f041b915b8 --- /dev/null +++ b/LeanPool/RareDistanceFields/DyadicCoordinates.lean @@ -0,0 +1,106 @@ +/- +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.RareDistanceFields.IntegerPlane +import Mathlib.Analysis.Complex.Basic + +/-! +# Integer coordinate division by 1+i + +See the project entry module for the exact coordinate restrictions and source roles. +Within either parity class, division by 1+i after a fixed translation preserves +integer coordinates and divides every squared distance by two. +-/ + +namespace LeanPool.RareDistanceFields.DyadicCoordinates + +open DyadicNorm IntegerPlane +local instance : Fact (Nat.Prime 2) := ⟨by decide⟩ + +/-- The parity of the sum of the two integer coordinates. -/ +def parity (p : Point) : ℤ := (p.1 + p.2) % 2 +/-- The translated, rotated half-scale coordinates for a chosen parity class. -/ +def halfPoint (e : ℤ) (p : Point) : Point := ((p.1 + p.2 - e) / 2, (p.2 - p.1 + e) / 2) + +theorem parity_zero_or_one (p : Point) : parity p = 0 ∨ parity p = 1 := by + dsimp [parity]; omega + +theorem norm_even_iff (p q : Point) : 2 ∣ sqDist p q ↔ parity p = parity q := by + rw [Int.dvd_iff_emod_eq_zero] + change normSq (p.1 - q.1) (p.2 - q.2) % 2 = 0 ↔ _ + rw [norm_mod_two] + dsimp [parity] + omega + +theorem halfPoint_scale (e : ℤ) (p q : Point) (hp : parity p = e) (hq : parity q = e) : + sqDist p q = 2 * sqDist (halfPoint e p) (halfPoint e q) := by + have h1 : 2 * ((p.1 + p.2 - e) / 2) = p.1 + p.2 - e := by dsimp [parity] at hp; omega + have h2 : 2 * ((p.2 - p.1 + e) / 2) = p.2 - p.1 + e := by dsimp [parity] at hp; omega + have h3 : 2 * ((q.1 + q.2 - e) / 2) = q.1 + q.2 - e := by dsimp [parity] at hq; omega + have h4 : 2 * ((q.2 - q.1 + e) / 2) = q.2 - q.1 + e := by dsimp [parity] at hq; omega + have hx : p.1 - q.1 = (halfPoint e p).1 - (halfPoint e q).1- + ((halfPoint e p).2 - (halfPoint e q).2) := by dsimp [halfPoint]; omega + have hy : p.2 - q.2 = (halfPoint e p).1 - (halfPoint e q).1 + + ((halfPoint e p).2 - (halfPoint e q).2) := by dsimp [halfPoint]; omega + change (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 = + 2 * (((halfPoint e p).1 - (halfPoint e q).1) ^ 2 + ((halfPoint e p).2 - (halfPoint e q).2) ^ 2) + rw [hx, hy] + ring + +theorem halfPoint_injective (e : ℤ) : + Function.Injective (fun p : {p : Point // parity p = e} => halfPoint e p.1) := by + intro p q h + change halfPoint e p.1 = halfPoint e q.1 at h + apply Subtype.ext + apply (sqDist_eq_zero p.1 q.1).mp + rw [halfPoint_scale e p.1 q.1 p.2 q.2, h] + simp [sqDist, normSq] + +theorem valuation_double (r : ℤ) (hr : r ≠ 0) : + padicValInt 2 (2 * r) = 1 + padicValInt 2 r := by + rw [padicValInt.mul (by norm_num) hr] + have hlo := (padicValInt_dvd_iff (p := 2) 1 (2 : ℤ)).mp (by norm_num) + have hhi : ¬2 ≤ padicValInt 2 (2 : ℤ) := by + intro h + have hh := (padicValInt_dvd_iff (p := 2) 2 (2 : ℤ)).mpr (Or.inr h) + norm_num at hh + have := hlo.resolve_left (by norm_num) + omega + +theorem valuation_zero_iff (r : ℤ) (hr : r ≠ 0) : + padicValInt 2 r = 0 ↔ ¬2 ∣ r := by + constructor + · intro h hd + have hv := (padicValInt_dvd_iff (p := 2) 1 r).mp (by simpa using hd) + have := hv.resolve_left hr + omega + · exact padicValInt.eq_zero_of_not_dvd + +theorem sqDist_pos (p q : Point) (h : p ≠ q) : 0 < sqDist p q := by + have hn := (sqDist_eq_zero p q).not.mpr h + have hnonneg : 0 ≤ sqDist p q := by dsimp [sqDist, normSq]; positivity + omega + +/-- The standard embedding of an integer coordinate pair into the complex plane. -/ +noncomputable def complexPoint (p : Point) : ℂ := ⟨p.1, p.2⟩ + +theorem complexPoint_injective : Function.Injective complexPoint := by + intro p q h + apply Prod.ext + · have := congrArg Complex.re h + dsimp [complexPoint] at this + exact_mod_cast this + · have := congrArg Complex.im h + dsimp [complexPoint] at this + exact_mod_cast this + +theorem complex_dist_sq (p q : Point) : + dist (complexPoint p) (complexPoint q) ^ 2 = (sqDist p q : ℝ) := by + rw [Complex.dist_eq, ← Complex.normSq_eq_norm_sq] + simp only [Complex.normSq_apply, Complex.sub_re, Complex.sub_im, complexPoint, sqDist, normSq] + push_cast + ring + +end LeanPool.RareDistanceFields.DyadicCoordinates diff --git a/LeanPool/RareDistanceFields/DyadicLevels.lean b/LeanPool/RareDistanceFields/DyadicLevels.lean new file mode 100644 index 0000000000..26522114e5 --- /dev/null +++ b/LeanPool/RareDistanceFields/DyadicLevels.lean @@ -0,0 +1,178 @@ +/- +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.RareDistanceFields.BipartiteDiameter +import LeanPool.RareDistanceFields.DyadicCoordinates +import LeanPool.RareDistanceFields.SplitCounts + +/-! +# A rare distance at every occurring dyadic level + +See the project entry module for the exact coordinate restrictions and source roles. +For any positive integer squared distance R maximal among distances with its +2-adic valuation, the unordered multiplicity of R is at most n. +-/ + +namespace LeanPool.RareDistanceFields.DyadicLevels + +open IntegerPlane DyadicCoordinates SplitCounts +noncomputable section +universe u + +open Classical in +theorem bichromatic_count_le {A B : Type*} [Fintype A] [Fintype B] + (x : A → Point) (y : B → Point) (hx : Function.Injective x) (hy : Function.Injective y) + (N : ℕ) (hN : 0 < N) (hmax : ∀ a b, sqDist (x a) (y b) ≤ N) : + count (fun a b => sqDist (x a) (y b)) (N : ℤ) ≤ Fintype.card A + Fintype.card B := by + classical + have hpos : (0 : ℝ) < N := by exact_mod_cast hN + have hs := Real.sq_sqrt hpos.le + have hb (a : A) (b : B) : dist (complexPoint (x a)) (complexPoint (y b)) ≤ Real.sqrt N := by + have hh : (sqDist (x a) (y b) : ℝ) ≤ N := by exact_mod_cast hmax a b + rw [← complex_dist_sq] at hh + nlinarith [Real.sqrt_nonneg (N : ℝ)] + have he (a : A) (b : B) : dist (complexPoint (x a)) (complexPoint (y b)) = Real.sqrt N ↔ + sqDist (x a) (y b) = N := by + constructor + · intro h + have hh := complex_dist_sq (x a) (y b) + rw [h, hs] at hh + exact_mod_cast hh.symm + · intro h + have hh := complex_dist_sq (x a) (y b) + rw [h, Int.cast_natCast] at hh + nlinarith [dist_nonneg (x := complexPoint (x a)) (y := complexPoint (y b)), + Real.sqrt_nonneg (N : ℝ)] + have hh := BipartiteDiameter.edges_card_le + (fun a => complexPoint (x a)) (fun b => complexPoint (y b)) + (complexPoint_injective.comp hx) (complexPoint_injective.comp hy) (Real.sqrt_pos.mpr hpos) hb + have hc : (BipartiteDiameter.edges (fun a => complexPoint (x a)) + (fun b => complexPoint (y b)) (Real.sqrt N)).card = + count (fun a b => sqDist (x a) (y b)) (N : ℤ) := by + simp only [BipartiteDiameter.edges, Finset.card_filter, Fintype.sum_prod_type, count] + apply Finset.sum_congr rfl + intro a ha + apply Finset.sum_congr rfl + intro b hb + by_cases hq : sqDist (x a) (y b) = N <;> simp [he, hq] + rw [hc] at hh + exact hh + +open Classical in +/-- Ordered count form; induction divides each parity class by 1+i. -/ +theorem level_max_count_le (N : ℕ) : ∀ {V : Type u} [Fintype V] + (x : V → Point), Function.Injective x → 0 < N → + (∀ p q, p ≠ q → padicValInt 2 (sqDist (x p) (x q)) = padicValInt 2 (N : ℤ) → + sqDist (x p) (x q) ≤ N) → + count (fun p q => sqDist (x p) (x q)) (N : ℤ) ≤ 2 * Fintype.card V := by + classical + induction N using Nat.strong_induction_on with + | h N ih => + intro V inst x hx hN hmax + let p : V → Prop := fun a => parity (x a) = 0 + let x0 : {a // p a} → Point := fun a => x a.1 + let x1 : {a // ¬p a} → Point := fun a => x a.1 + have hx0 : Function.Injective x0 := hx.comp Subtype.val_injective + have hx1 : Function.Injective x1 := hx.comp Subtype.val_injective + have hp0 (a : {a // p a}) : parity (x0 a) = 0 := a.2 + have hp1 (a : {a // ¬p a}) : parity (x1 a) = 1 := + (parity_zero_or_one (x1 a)).resolve_left a.2 + have hcross (a : {a // p a}) (b : {a // ¬p a}) : ¬2 ∣ sqDist (x0 a) (x1 b) := by + rw [norm_even_iff, hp0 a, hp1 b] + norm_num + have hreverse : count (fun a b => sqDist (x1 a) (x0 b)) (N : ℤ) = + count (fun a b => sqDist (x0 a) (x1 b)) (N : ℤ) := by + rw [count_symm] + simp only [sqDist_symm] + have hsplit := count_split (fun a b => sqDist (x a) (x b)) (N : ℤ) p + change count (fun a b => sqDist (x a) (x b)) (N : ℤ) = + count (fun a b => sqDist (x0 a) (x0 b)) (N : ℤ) + + count (fun a b => sqDist (x0 a) (x1 b)) (N : ℤ) + + count (fun a b => sqDist (x1 a) (x0 b)) (N : ℤ) + + count (fun a b => sqDist (x1 a) (x1 b)) (N : ℤ) at hsplit + have hcards := card_split p + by_cases h2 : 2 ∣ N + · obtain ⟨M, hNM⟩ := h2 + have hM : 0 < M := by omega + have hMN : M < N := by omega + have hNM' : (N : ℤ) = 2 * M := by exact_mod_cast hNM + have hc0 : count (fun a b => sqDist (x0 a) (x1 b)) (N : ℤ) = 0 := by + apply count_zero + intro a b he + apply hcross a b + rw [he, hNM'] + exact dvd_mul_right 2 (M : ℤ) + have hwithin {W : Type u} [Fintype W] (z : W → V) (hz : Function.Injective z) + (e : ℤ) (hpar : ∀ w, parity (x (z w)) = e) : + count (fun a b => sqDist (x (z a)) (x (z b))) (N : ℤ) ≤ 2 * Fintype.card W := by + let y : W → Point := fun w => halfPoint e (x (z w)) + have hscale (a b : W) : sqDist (x (z a)) (x (z b)) = 2 * sqDist (y a) (y b) := + halfPoint_scale e _ _ (hpar a) (hpar b) + have hy : Function.Injective y := by + intro a b he + apply hz + apply hx + apply (sqDist_eq_zero _ _).mp + rw [hscale, he] + simp [sqDist, DyadicNorm.normSq] + have hbound (a b : W) (hab : a ≠ b) + (hv : padicValInt 2 (sqDist (y a) (y b)) = padicValInt 2 (M : ℤ)) : + sqDist (y a) (y b) ≤ M := by + have hnq := (sqDist_eq_zero (y a) (y b)).not.mpr (hy.ne hab) + have hnM : (M : ℤ) ≠ 0 := by exact_mod_cast ne_of_gt hM + have hh := hmax (z a) (z b) (hz.ne hab) (by + rw [hscale, hNM', valuation_double _ hnq, valuation_double _ hnM, hv]) + rw [hscale, hNM'] at hh + omega + have hcount := ih M hMN y hy hM hbound + have heq := count_congr (fun a b => sqDist (x (z a)) (x (z b))) + (fun a b => sqDist (y a) (y b)) (N : ℤ) (M : ℤ) (by + intro a b + rw [hscale, hNM'] + omega) + exact heq ▸ hcount + have h0 := hwithin (fun a : {a // p a} => a.1) Subtype.val_injective 0 hp0 + have h1 := hwithin (fun a : {a // ¬p a} => a.1) Subtype.val_injective 1 hp1 + change count (fun a b => sqDist (x0 a) (x0 b)) (N : ℤ) ≤ + 2 * Fintype.card {a // p a} at h0 + change count (fun a b => sqDist (x1 a) (x1 b)) (N : ℤ) ≤ + 2 * Fintype.card {a // ¬p a} at h1 + rw [hreverse, hc0] at hsplit + omega + · have hnN : (N : ℤ) ≠ 0 := by exact_mod_cast ne_of_gt hN + have h2' : ¬(2 : ℤ) ∣ N := by exact_mod_cast h2 + have hvN := (valuation_zero_iff (N : ℤ) hnN).mpr h2' + have hwithin {W : Type u} [Fintype W] (y : W → Point) (e : ℤ) + (he : ∀ w, parity (y w) = e) : count (fun a b => sqDist (y a) (y b)) (N : ℤ) = 0 := by + apply count_zero + intro a b hab + apply h2' + rw [← hab, norm_even_iff, he a, he b] + have h0 := hwithin x0 0 hp0 + have h1 := hwithin x1 1 hp1 + have hbound (a : {a // p a}) (b : {a // ¬p a}) : sqDist (x0 a) (x1 b) ≤ N := by + have hab : a.1 ≠ b.1 := by intro h; exact b.2 (h ▸ a.2) + have hnq := (sqDist_eq_zero (x0 a) (x1 b)).not.mpr (hx.ne hab) + exact hmax a.1 b.1 hab (by rw [(valuation_zero_iff _ hnq).mpr (hcross a b), hvN]) + have hc := bichromatic_count_le x0 x1 hx0 hx1 N hN hbound + rw [hreverse, h0, h1] at hsplit + omega + +open Classical in +theorem level_max_multiplicity_le {V : Type*} [Fintype V] (x : V → Point) + (hx : Function.Injective x) (N : ℕ) (hN : 0 < N) + (hmax : ∀ p q, p ≠ q → padicValInt 2 (sqDist (x p) (x q)) = padicValInt 2 (N : ℤ) → + sqDist (x p) (x q) ≤ N) : (graph x (N : ℤ)).edgeFinset.card ≤ Fintype.card V := by + have hh := level_max_count_le N x hx hN hmax + have he := count_eq_twice_edges (fun p q => sqDist (x p) (x q)) + (fun p q => sqDist_symm (x p) (x q)) (N : ℤ) (by + intro p + have hn : (0 : ℤ) < N := by exact_mod_cast hN + simpa [sqDist, DyadicNorm.normSq] using ne_of_lt hn) + change _ = 2 * (graph x (N : ℤ)).edgeFinset.card at he + omega + +end +end LeanPool.RareDistanceFields.DyadicLevels diff --git a/LeanPool/RareDistanceFields/DyadicNorm.lean b/LeanPool/RareDistanceFields/DyadicNorm.lean new file mode 100644 index 0000000000..1652006a74 --- /dev/null +++ b/LeanPool/RareDistanceFields/DyadicNorm.lean @@ -0,0 +1,138 @@ +/- +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.Algebra.EuclideanDomain.Basic +import Mathlib.Algebra.EuclideanDomain.Int +import Mathlib.Algebra.Order.Ring.Star +import Mathlib.Data.Int.ConditionallyCompleteOrder +import Mathlib.Data.Int.Star +import Mathlib.NumberTheory.Padics.PadicVal.Basic +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# A strict dyadic inequality on an integer circle + +See the project entry module for the exact coordinate restrictions and source roles. +For two distinct integer vectors of the same nonzero squared norm, the squared +norm of their difference has strictly larger 2-adic valuation. +-/ + +namespace LeanPool.RareDistanceFields.DyadicNorm + +local instance : Fact (Nat.Prime 2) := ⟨by decide⟩ + +/-- The squared Euclidean norm of an integer coordinate pair. -/ +def normSq (a b : ℤ) : ℤ := a ^ 2 + b ^ 2 + +theorem square_mod_four (a : ℤ) : a ^ 2 % 4 = (a % 2) ^ 2 := by + have h : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3 := by omega + rcases h with h|h|h|h + all_goals + have h2 : a % 2 = a % 4 % 2 := by omega + rw [pow_two, Int.mul_emod, h, h2, h] + norm_num + +theorem four_dvd_norm_iff (a b : ℤ) : 4 ∣ normSq a b ↔ 2 ∣ a ∧ 2 ∣ b := by + rw [Int.dvd_iff_emod_eq_zero, normSq, Int.add_emod, square_mod_four, square_mod_four] + simp only [Int.dvd_iff_emod_eq_zero] + have ha : a % 2 = 0 ∨ a % 2 = 1 := by omega + have hb : b % 2 = 0 ∨ b % 2 = 1 := by omega + rcases ha with ha|ha <;> rcases hb with hb|hb <;> simp [ha, hb] + +theorem norm_mod_two (a b : ℤ) : normSq a b % 2 = (a + b) % 2 := by + have hs (z : ℤ) : z ^ 2 % 2 = z % 2 := by + rw [pow_two, Int.mul_emod] + have hz : z % 2 = 0 ∨ z % 2 = 1 := by omega + rcases hz with hz|hz <;> simp [hz] + rw [normSq, Int.add_emod, hs, hs, ← Int.add_emod] + +theorem equal_norm_difference_even (a b c d : ℤ) (he : normSq a b = normSq c d) : + 2 ∣ normSq (a - c) (b - d) := by + have h := congrArg (fun z : ℤ => z % 2) he + rw [norm_mod_two, norm_mod_two] at h + rw [Int.dvd_iff_emod_eq_zero, norm_mod_two] + omega + +theorem even_norm_not_four (a b : ℤ) (he : 2 ∣ normSq a b) (hf : ¬ 4 ∣ normSq a b) : + a % 2 = 1 ∧ b % 2 = 1 := by + rw [Int.dvd_iff_emod_eq_zero, norm_mod_two] at he + rw [four_dvd_norm_iff] at hf + simp only [Int.dvd_iff_emod_eq_zero] at hf + omega + +theorem equal_norm_increase_aux (N : ℕ) : + ∀ a b c d : ℤ, normSq a b = N → normSq c d = N → 0 < N → + normSq (a - c) (b - d) ≠ 0 → + padicValInt 2 (N : ℤ) < padicValInt 2 (normSq (a - c) (b - d)) := by + induction N using Nat.strong_induction_on with + | h N ih => + intro a b c d ha hb hN hdiff + by_cases h4 : (4 : ℤ) ∣ N + · obtain ⟨a', rfl⟩ := (four_dvd_norm_iff a b).mp (ha ▸ h4) |>.1 + obtain ⟨b', rfl⟩ := (four_dvd_norm_iff (2 * a') b).mp (ha ▸ h4) |>.2 + obtain ⟨c', rfl⟩ := (four_dvd_norm_iff c d).mp (hb ▸ h4) |>.1 + obtain ⟨d', rfl⟩ := (four_dvd_norm_iff (2 * c') d).mp (hb ▸ h4) |>.2 + have hN4 : 4 ∣ N := by exact_mod_cast h4 + obtain ⟨M, hM⟩ := hN4 + have hMpos : 0 < M := by omega + have hMN : M < N := by omega + have ha' : normSq a' b' = M := by + simp only [normSq] at ha ⊢ + rw [hM, Nat.cast_mul, Nat.cast_ofNat] at ha + nlinarith + have hb' : normSq c' d' = M := by + simp only [normSq] at hb ⊢ + rw [hM, Nat.cast_mul, Nat.cast_ofNat] at hb + nlinarith + have heq : normSq (2 * a'-2 * c') (2 * b'-2 * d') = 4 * normSq (a'-c') (b'-d') := by + simp only [normSq]; ring + rw [heq] at hdiff ⊢ + have hd' : normSq (a'-c') (b'-d') ≠ 0 := by intro h; simp [h] at hdiff + have hm0 : (M : ℤ) ≠ 0 := by exact_mod_cast (ne_of_gt hMpos) + have hi := ih M hMN a' b' c' d' ha' hb' hMpos hd' + rw [hM, Nat.cast_mul, Nat.cast_ofNat, padicValInt.mul (by norm_num) hm0, + padicValInt.mul (by norm_num) hd'] + omega + · by_cases h2 : (2 : ℤ) ∣ N + · have hab := even_norm_not_four a b (ha ▸ h2) (ha ▸ h4) + have hcd := even_norm_not_four c d (hb ▸ h2) (hb ▸ h4) + have hd4 : (4 : ℤ) ∣ normSq (a - c) (b - d) := by + rw [four_dvd_norm_iff] + simp only [Int.dvd_iff_emod_eq_zero] + constructor <;> omega + have hv : 2 ≤ padicValInt 2 (normSq (a - c) (b - d)) := by + have hh := (padicValInt_dvd_iff (p := 2) 2 (normSq (a - c) (b - d))).mp + (by simpa using hd4) + exact hh.resolve_left hdiff + have hvN : padicValInt 2 (N : ℤ) = 1 := by + have hn0 : (N : ℤ) ≠ 0 := by exact_mod_cast (ne_of_gt hN) + have hlo := (padicValInt_dvd_iff (p := 2) 1 (N : ℤ)).mp (by simpa using h2) + have hhi : ¬ 2 ≤ padicValInt 2 (N : ℤ) := by + intro h + apply h4 + simpa using (padicValInt_dvd_iff (p := 2) 2 (N : ℤ)).mpr (Or.inr h) + have := hlo.resolve_left hn0 + omega + omega + · rw [padicValInt.eq_zero_of_not_dvd h2] + have hd2 := equal_norm_difference_even a b c d (ha.trans hb.symm) + have hv := (padicValInt_dvd_iff (p := 2) 1 (normSq (a - c) (b - d))).mp (by simpa using hd2) + have := hv.resolve_left hdiff + omega + +theorem equal_norm_increase (a b c d : ℤ) (hn : normSq a b ≠ 0) + (he : normSq a b = normSq c d) (hd : normSq (a - c) (b - d) ≠ 0) : + padicValInt 2 (normSq a b) < padicValInt 2 (normSq (a - c) (b - d)) := by + have hnonneg : 0 ≤ normSq a b := by dsimp [normSq]; positivity + have hpos : 0 < normSq a b := lt_of_le_of_ne hnonneg (Ne.symm hn) + have ha : normSq a b = ((normSq a b).toNat : ℤ) := (Int.toNat_of_nonneg hnonneg).symm + simpa only [Int.toNat_of_nonneg hnonneg] using + equal_norm_increase_aux (normSq a b).toNat a b c d ha (he.symm.trans ha) + (by omega) hd + +end LeanPool.RareDistanceFields.DyadicNorm diff --git a/LeanPool/RareDistanceFields/DyadicSize.lean b/LeanPool/RareDistanceFields/DyadicSize.lean new file mode 100644 index 0000000000..d7ba3b722d --- /dev/null +++ b/LeanPool/RareDistanceFields/DyadicSize.lean @@ -0,0 +1,135 @@ +/- +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.RareDistanceFields.DyadicCoordinates +import LeanPool.RareDistanceFields.SplitCounts + +/-! +# Binary size bound from the occurring dyadic levels + +See the project entry module for the exact coordinate restrictions and source roles. +If a finite integer-coordinate planar set uses k dyadic valuations among its +positive squared distances, then it contains at most 2^k points. +-/ + +namespace LeanPool.RareDistanceFields.DyadicSize + +open IntegerPlane DyadicCoordinates SplitCounts +noncomputable section +universe u + +open Classical in +theorem card_le_pow_of_bound (M : ℕ) : ∀ {V : Type u} [Fintype V] + (x : V → Point), Function.Injective x → ∀ L : Finset ℕ, + (∀ a b, sqDist (x a) (x b) ≤ M) → + (∀ a b, a ≠ b → padicValInt 2 (sqDist (x a) (x b)) ∈ L) → + Fintype.card V ≤ 2 ^ L.card := by + classical + induction M using Nat.strong_induction_on with + | h M ih => + intro V inst x hx L hbound hL + by_cases hM : M = 0 + · have hc : Fintype.card V ≤ 1 := by + apply Fintype.card_le_one_iff.mpr + intro a b + apply hx + apply (sqDist_eq_zero _ _).mp + have hh := hbound a b + have hn : 0 ≤ sqDist (x a) (x b) := by + dsimp [sqDist, DyadicNorm.normSq]; positivity + rw [hM] at hh + omega + exact hc.trans (Nat.one_le_pow _ _ (by decide)) + have hMpos : 0 < M := by omega + have hsmaller : M / 2 < M := Nat.div_lt_self hMpos (by decide) + let p : V → Prop := fun a => parity (x a) = 0 + let L' : Finset ℕ := (L.erase 0).image Nat.pred + have hcardL : L'.card ≤ (L.erase 0).card := Finset.card_image_le + have hcardL' : L'.card ≤ L.card := hcardL.trans (Finset.card_le_card (Finset.erase_subset _ _)) + have hpow : 2 ^ L'.card ≤ 2 ^ L.card := Nat.pow_le_pow_right (by decide) hcardL' + have hwithin {W : Type u} [Fintype W] (z : W → V) (hz : Function.Injective z) + (e : ℤ) (hpar : ∀ w, parity (x (z w)) = e) : Fintype.card W ≤ 2 ^ L'.card := by + let y : W → Point := fun w => halfPoint e (x (z w)) + have hscale (a b : W) : sqDist (x (z a)) (x (z b)) = 2 * sqDist (y a) (y b) := + halfPoint_scale e _ _ (hpar a) (hpar b) + have hy : Function.Injective y := by + intro a b he + apply hz + apply hx + apply (sqDist_eq_zero _ _).mp + rw [hscale, he] + simp [sqDist, DyadicNorm.normSq] + apply ih (M / 2) hsmaller y hy L' + · intro a b + have hh := hbound (z a) (z b) + rw [hscale] at hh + rw [Int.natCast_ediv] + omega + · intro a b hab + have hn := (sqDist_eq_zero (y a) (y b)).not.mpr (hy.ne hab) + have hs : padicValInt 2 (sqDist (x (z a)) (x (z b))) = + 1 + padicValInt 2 (sqDist (y a) (y b)) := by rw [hscale, valuation_double _ hn] + apply Finset.mem_image.mpr + refine ⟨padicValInt 2 (sqDist (x (z a)) (x (z b))), ?_, ?_⟩ + · apply Finset.mem_erase.mpr + exact ⟨by omega, hL (z a) (z b) (hz.ne hab)⟩ + · rw [hs] + simp + have h0 := hwithin (fun a : {a // p a} => a.1) Subtype.val_injective 0 (fun a => a.2) + have h1 := hwithin (fun a : {a // ¬p a} => a.1) Subtype.val_injective 1 + (fun a => (parity_zero_or_one (x a.1)).resolve_left a.2) + have hcards := card_split p + by_cases hz : 0 ∈ L + · have hLpos : 0 < L.card := Finset.card_pos.mpr ⟨0, hz⟩ + rw [Finset.card_erase_of_mem hz] at hcardL + have hp : 2 * 2 ^ L'.card ≤ 2 ^ L.card := by + calc + 2 * 2 ^ L'.card = 2 ^ (L'.card + 1) := by rw [pow_succ]; omega + _ ≤ 2 ^ L.card := Nat.pow_le_pow_right (by decide) (by omega) + omega + · by_cases h0empty : Fintype.card {a // p a} = 0 + · omega + · have h0pos : 0 < Fintype.card {a // p a} := by omega + obtain ⟨a⟩ := Fintype.card_pos_iff.mp h0pos + have hempty : IsEmpty {b // ¬p b} := by + constructor + intro b + have hab : a.1 ≠ b.1 := by intro h; exact b.2 (h ▸ a.2) + have hpar : parity (x b.1) = 1 := (parity_zero_or_one _).resolve_left b.2 + have hn := (sqDist_eq_zero (x a.1) (x b.1)).not.mpr (hx.ne hab) + have hodd : ¬2 ∣ sqDist (x a.1) (x b.1) := by + rw [norm_even_iff, a.2, hpar] + norm_num + have hv := (valuation_zero_iff _ hn).mpr hodd + exact hz (hv ▸ hL a.1 b.1 hab) + have he : Fintype.card {a // ¬p a} = 0 := Fintype.card_eq_zero + omega + +open Classical in +/-- The 2-adic squared-distance levels realized between distinct labels. -/ +def levels {V : Type*} [Fintype V] (x : V → Point) : Finset ℕ := + Finset.univ.offDiag.image (fun ab => padicValInt 2 (sqDist (x ab.1) (x ab.2))) + +open Classical in +theorem mem_levels {V : Type*} [Fintype V] (x : V → Point) (a b : V) (hab : a ≠ b) : + padicValInt 2 (sqDist (x a) (x b)) ∈ levels x := by + exact Finset.mem_image.mpr ⟨(a, b), by simp [hab], rfl⟩ + +open Classical in +theorem card_le_pow_levels {V : Type*} [Fintype V] (x : V → Point) + (hx : Function.Injective x) : Fintype.card V ≤ 2 ^ (levels x).card := by + classical + let M := (Finset.univ : Finset (V × V)).sup (fun ab => (sqDist (x ab.1) (x ab.2)).toNat) + apply card_le_pow_of_bound M x hx (levels x) + · intro a b + have hn : 0 ≤ sqDist (x a) (x b) := by + dsimp [sqDist, DyadicNorm.normSq]; positivity + have hh : (sqDist (x a) (x b)).toNat ≤ M := + Finset.le_sup (f := fun ab => (sqDist (x ab.1) (x ab.2)).toNat) (Finset.mem_univ (a, b)) + omega + · exact mem_levels x + +end +end LeanPool.RareDistanceFields.DyadicSize diff --git a/LeanPool/RareDistanceFields/IntegerDivergence.lean b/LeanPool/RareDistanceFields/IntegerDivergence.lean new file mode 100644 index 0000000000..9add0bfa56 --- /dev/null +++ b/LeanPool/RareDistanceFields/IntegerDivergence.lean @@ -0,0 +1,105 @@ +/- +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.RareDistanceFields.DyadicLevels +import LeanPool.RareDistanceFields.DyadicSize + +/-! +# Logarithmically many rare distances for integer planar sets + +See the project entry module for the exact coordinate restrictions and source roles. +Each occurring dyadic level contributes its numerically largest squared +distance. Their multiplicities are at most n, and n is at most two to the +number of selected levels. This proves both assertions for integer coordinates. +-/ + +namespace LeanPool.RareDistanceFields.IntegerDivergence + +open IntegerPlane DyadicCoordinates DyadicLevels DyadicSize +noncomputable section + +variable {V : Type*} [Fintype V] + +open Classical in +/-- All squared distances realized between distinct integer-point labels. -/ +def palette (x : V → Point) : Finset ℤ := + OrderedColors.palette (fun a b => sqDist (x a) (x b)) + +open Classical in +/-- Occurring squared distances whose unordered multiplicities are at most the label count. -/ +def rareSquared (x : V → Point) : Finset ℤ := + (palette x).filter fun r => (graph x r).edgeFinset.card ≤ Fintype.card V + +open Classical in +theorem mem_palette (x : V → Point) (a b : V) (hab : a ≠ b) : + sqDist (x a) (x b) ∈ palette x := by + exact Finset.mem_image.mpr ⟨(a, b), by simp [hab], rfl⟩ + +open Classical in +theorem exists_pair_of_mem_palette (x : V → Point) {r : ℤ} (hr : r ∈ palette x) : + ∃ a b, a ≠ b ∧ sqDist (x a) (x b) = r := by + obtain ⟨⟨a, b⟩, hab, he⟩ := Finset.mem_image.mp hr + exact ⟨a, b, (Finset.mem_offDiag.mp hab).2.2, he⟩ + +open Classical in +theorem palette_positive (x : V → Point) (hx : Function.Injective x) + {r : ℤ} (hr : r ∈ palette x) : 0 < r := by + obtain ⟨a, b, hab, rfl⟩ := exists_pair_of_mem_palette x hr + exact DyadicCoordinates.sqDist_pos _ _ (hx.ne hab) + +open Classical in +theorem rare_at_level (x : V → Point) (hx : Function.Injective x) + {v : ℕ} (hv : v ∈ levels x) : ∃ r ∈ rareSquared x, padicValInt 2 r = v := by + classical + let s := (palette x).filter fun r => padicValInt 2 r = v + have hs : s.Nonempty := by + obtain ⟨⟨a, b⟩, hab, he⟩ := Finset.mem_image.mp hv + exact ⟨sqDist (x a) (x b), Finset.mem_filter.mpr + ⟨mem_palette x a b (Finset.mem_offDiag.mp hab).2.2, he⟩⟩ + let r := s.max' hs + have hr : r ∈ s := Finset.max'_mem s hs + have hrP : r ∈ palette x := (Finset.mem_filter.mp hr).1 + have hrv : padicValInt 2 r = v := (Finset.mem_filter.mp hr).2 + have hpos := palette_positive x hx hrP + have hcast : (r.toNat : ℤ) = r := Int.toNat_of_nonneg hpos.le + have hmax (a b : V) (hab : a ≠ b) + (he : padicValInt 2 (sqDist (x a) (x b)) = padicValInt 2 (r.toNat : ℤ)) : + sqDist (x a) (x b) ≤ (r.toNat : ℤ) := by + rw [hcast] + apply Finset.le_max' + apply Finset.mem_filter.mpr + refine ⟨mem_palette x a b hab, ?_⟩ + rwa [hcast, hrv] at he + have hm := level_max_multiplicity_le x hx r.toNat (by omega) hmax + rw [hcast] at hm + exact ⟨r, Finset.mem_filter.mpr ⟨hrP, hm⟩, hrv⟩ + +open Classical in +theorem levels_card_le_rare (x : V → Point) (hx : Function.Injective x) : + (levels x).card ≤ (rareSquared x).card := by + have hs : levels x ⊆ (rareSquared x).image (padicValInt 2) := by + intro v hv + obtain ⟨r, hr, he⟩ := rare_at_level x hx hv + exact Finset.mem_image.mpr ⟨r, hr, he⟩ + exact (Finset.card_le_card hs).trans Finset.card_image_le + +open Classical in +theorem card_le_pow_rare (x : V → Point) (hx : Function.Injective x) : + Fintype.card V ≤ 2 ^ (rareSquared x).card := + (card_le_pow_levels x hx).trans (Nat.pow_le_pow_right (by decide) (levels_card_le_rare x hx)) + +open Classical in +theorem uniform_divergence (k : ℕ) : ∃ N : ℕ, ∀ {V : Type*} [Fintype V] + (x : V → Point), Function.Injective x → N ≤ Fintype.card V → + k ≤ (rareSquared x).card := by + refine ⟨2 ^ k, ?_⟩ + intro V inst x hx hn + have hh := card_le_pow_rare x hx + by_contra h + have hp : 2 ^ (rareSquared x).card < 2 ^ k := Nat.pow_lt_pow_right (by decide) (by omega) + omega + +end +end LeanPool.RareDistanceFields.IntegerDivergence diff --git a/LeanPool/RareDistanceFields/IntegerPlane.lean b/LeanPool/RareDistanceFields/IntegerPlane.lean new file mode 100644 index 0000000000..0b2eeb9c0a --- /dev/null +++ b/LeanPool/RareDistanceFields/IntegerPlane.lean @@ -0,0 +1,117 @@ +/- +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.RareDistanceFields.OrderedColors +import LeanPool.RareDistanceFields.DyadicNorm + +/-! +# Two rare distances in every finite integer-coordinate planar set + +See the project entry module for the exact coordinate restrictions and source roles. +Order squared distances by their 2-adic valuations, breaking ties numerically. +The dyadic circle lemma supplies the increasing-base rule. The two top classes +therefore have unordered multiplicity at most the number of points. +This is a restricted coordinate theorem; arbitrary real coordinates are not assumed rational. +-/ + +namespace LeanPool.RareDistanceFields.IntegerPlane + +open DyadicNorm +noncomputable section + +open Classical in +/-- An integer coordinate pair in the plane. -/ +abbrev Point := ℤ × ℤ + +open Classical in +/-- The integer squared Euclidean distance between two points. -/ +def sqDist (p q : Point) : ℤ := normSq (p.1 - q.1) (p.2 - q.2) + +open Classical in +theorem sqDist_symm (p q : Point) : sqDist p q = sqDist q p := by + dsimp [sqDist, normSq]; ring + +open Classical in +theorem sqDist_eq_zero (p q : Point) : sqDist p q = 0 ↔ p = q := by + constructor + · intro h + dsimp [sqDist, normSq] at h + apply Prod.ext <;> nlinarith [sq_nonneg (p.1 - q.1), sq_nonneg (p.2 - q.2)] + · rintro rfl + simp [sqDist, normSq] + +open Classical in +/-- The lexicographic key of a squared distance: its 2-adic valuation, then its value. -/ +def key (r : ℤ) : Lex (ℕ × ℤ) := toLex (padicValInt 2 r, r) + +open Classical in +theorem key_injective : Function.Injective key := by + intro a b h + exact congrArg (fun r => (ofLex r).2) h + +open Classical in +theorem equal_spokes_increase (p q r : Point) (hpq : p ≠ q) (hqr : q ≠ r) + (he : sqDist p q = sqDist p r) : key (sqDist p q) < key (sqDist q r) := by + have hn : normSq (p.1 - q.1) (p.2 - q.2) ≠ 0 := (sqDist_eq_zero p q).not.mpr hpq + have hd : normSq ((p.1 - q.1) - (p.1 - r.1)) ((p.2 - q.2) - (p.2 - r.2)) ≠ 0 := by + have hn' := (sqDist_eq_zero r q).not.mpr hqr.symm + have heq : normSq ((p.1 - q.1) - (p.1 - r.1)) ((p.2 - q.2) - (p.2 - r.2)) = sqDist r q := by + dsimp [sqDist, normSq]; ring + rw [heq] + exact hn' + have hv := equal_norm_increase (p.1 - q.1) (p.2 - q.2) (p.1 - r.1) (p.2 - r.2) hn he hd + have heq : normSq ((p.1 - q.1) - (p.1 - r.1)) ((p.2 - q.2) - (p.2 - r.2)) = sqDist q r := by + dsimp [sqDist, normSq]; ring + have hv' : padicValInt 2 (sqDist p q) < padicValInt 2 (sqDist q r) := by + rw [heq] at hv + exact hv + exact Prod.Lex.left _ _ hv' + +variable {V : Type*} [Fintype V] + +open Classical in +/-- The simple graph of distinct labels at a specified integer squared distance. -/ +def graph (x : V → Point) (r : ℤ) : SimpleGraph V := + OrderedColors.colorGraph (fun a b => sqDist (x a) (x b)) + (fun a b => sqDist_symm (x a) (x b)) r + +omit [Fintype V] in +open Classical in +theorem graph_key (x : V → Point) + (hsym : ∀ a b, key (sqDist (x a) (x b)) = key (sqDist (x b) (x a))) (r : ℤ) : + OrderedColors.colorGraph (fun a b => key (sqDist (x a) (x b))) + hsym (key r) = graph x r := by + ext p q + simp only [OrderedColors.colorGraph, graph, key_injective.eq_iff] + +open Classical in +/-- An end-to-end statement with actual integer coordinates and occurring distances. -/ +theorem two_rare_distances (x : V → Point) (hx : Function.Injective x) + (hn : 3 ≤ Fintype.card V) : + ∃ a b c d : V, a ≠ b ∧ c ≠ d ∧ sqDist (x a) (x b) ≠ sqDist (x c) (x d) ∧ + (graph x (sqDist (x a) (x b))).edgeFinset.card ≤ Fintype.card V ∧ + (graph x (sqDist (x c) (x d))).edgeFinset.card ≤ Fintype.card V := by + let q := fun a b => key (sqDist (x a) (x b)) + have hs : ∀ a b, q a b = q b a := fun a b => congrArg key (sqDist_symm (x a) (x b)) + have hb : OrderedColors.IncreasingBases q := by + intro a b c hab hac hbc he + exact equal_spokes_increase (x a) (x b) (x c) (hx.ne hab) (hx.ne hbc) (key_injective he) + obtain ⟨r, hr, D, hD, hrD, hrare, hrareD⟩ := OrderedColors.two_rare_colors q hs hb hn + obtain ⟨⟨a, b⟩, hab, rfl⟩ := Finset.mem_image.mp hr + obtain ⟨⟨c, d⟩, hcd, rfl⟩ := Finset.mem_image.mp hD + have hab' : a ≠ b := (Finset.mem_offDiag.mp hab).2.2 + have hcd' : c ≠ d := (Finset.mem_offDiag.mp hcd).2.2 + refine ⟨a, b, c, d, hab', hcd', ?_, ?_, ?_⟩ + · intro he + exact hrD (congrArg key he) + · dsimp only [q] at hrare + rw [graph_key x hs] at hrare + exact hrare + · dsimp only [q] at hrareD + rw [graph_key x hs] at hrareD + exact hrareD + +end +end LeanPool.RareDistanceFields.IntegerPlane diff --git a/LeanPool/RareDistanceFields/OctagonalDescent.lean b/LeanPool/RareDistanceFields/OctagonalDescent.lean new file mode 100644 index 0000000000..2fdd46a057 --- /dev/null +++ b/LeanPool/RareDistanceFields/OctagonalDescent.lean @@ -0,0 +1,58 @@ +/- +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.RareDistanceFields.BinaryPalette +import LeanPool.RareDistanceFields.OctagonalNorm + +/-! +# Logarithmically many rare distances in Z[zeta_8] + +See the project entry module for the exact coordinate restrictions and source roles. +All binary descent hypotheses are discharged by the actual octagonal +embedding. There is no assumed rarity or assumed planar realization. +-/ + +namespace LeanPool.RareDistanceFields.OctagonalDescent + +open OctagonalNorm +noncomputable section + +open Classical in +/-- The binary descent model constructed from octagonal integer coordinates. -/ +def model : BinaryDescent.Model Point where + point := embed + point_injective := embed_injective + height := fun u v => height (u - v) + height_nonneg := fun u v => height_nonneg (u - v) + height_zero := fun u v => by rw [height_eq_zero, sub_eq_zero] + distance_height := distance_height + parity := parity + parity_values := parity_zero_or_one + even_iff := height_even_iff + half := divide + scale := ‖pi‖ + scale_pos := norm_pos_iff.mpr pi_ne_zero + half_height := divide_height + half_distance := divide_distance + +open Classical in +/-- Occurring octagonal distances with unordered multiplicity at most the label count. -/ +abbrev rareDistances {V : Type*} [Fintype V] (x : V → Point) : Finset ℝ := + BinaryPalette.rareDistances model x + +open Classical in +theorem card_le_pow_rareDistances {V : Type*} [Fintype V] (x : V → Point) + (hx : Function.Injective x) : Fintype.card V ≤ 2 ^ (rareDistances x).card := + BinaryPalette.card_le_pow_rareDistances model x hx + +open Classical in +theorem rareDistances_spec {V : Type*} [Fintype V] (x : V → Point) + (hx : Function.Injective x) (d : ℝ) : + d ∈ rareDistances x ↔ 0 < d ∧ (∃ a b, a ≠ b ∧ dist (embed (x a)) (embed (x b)) = d) ∧ + (BinaryPalette.graph model x d).edgeFinset.card ≤ Fintype.card V := + BinaryPalette.rareDistances_spec model x hx d + +end +end LeanPool.RareDistanceFields.OctagonalDescent diff --git a/LeanPool/RareDistanceFields/OctagonalNorm.lean b/LeanPool/RareDistanceFields/OctagonalNorm.lean new file mode 100644 index 0000000000..467ba50de6 --- /dev/null +++ b/LeanPool/RareDistanceFields/OctagonalNorm.lean @@ -0,0 +1,211 @@ +/- +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.Algebra.EuclideanDomain.Int +import Mathlib.Algebra.Order.Ring.Star +import Mathlib.Analysis.CStarAlgebra.Classes +import Mathlib.Data.Int.Star +import Mathlib.NumberTheory.Real.Irrational +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# An integer descent height for octagonal coordinates + +See the project entry module for the exact coordinate restrictions and source roles. +The actual embedding is Z[zeta_8] in the complex plane. The integer height +is the field norm of the squared Euclidean norm, not the squared norm itself. +No arbitrary-real coordinate reduction is claimed. +-/ + +namespace LeanPool.RareDistanceFields.OctagonalNorm + +/-- Four integer coefficients in the octagonal basis, grouped as two pairs. -/ +abbrev Point := (ℤ × ℤ) × (ℤ × ℤ) + +/-- The rational coefficient of the squared norm of the octagonal embedding. -/ +def rationalPart (u : Point) : ℤ := + u.1.1 ^ 2 + u.1.2 ^ 2 + u.2.1 ^ 2 + u.2.2 ^ 2 + +/-- The coefficient of sqrt(2) in the squared norm of the octagonal embedding. -/ +def irrationalPart (u : Point) : ℤ := + u.1.1 * (u.1.2 - u.2.2) + u.2.1 * (u.1.2 + u.2.2) + +/-- The quadratic field norm of the squared Euclidean norm, an integer descent height. -/ +def height (u : Point) : ℤ := rationalPart u ^ 2 - 2 * irrationalPart u ^ 2 + +/-- The complex embedding with basis 1, exp(pi*i/4), i, and exp(3*pi*i/4). -/ +noncomputable def embed (u : Point) : ℂ := + ⟨(u.1.1 : ℝ) + (u.1.2 - u.2.2 : ℤ) * Real.sqrt 2 / 2, + (u.2.1 : ℝ) + (u.1.2 + u.2.2 : ℤ) * Real.sqrt 2 / 2⟩ + +/-- The sum of the four integer coefficients modulo two. -/ +def parity (u : Point) : ℤ := (u.1.1 + u.1.2 + u.2.1 + u.2.2) % 2 + +/-- Coefficient multiplication by the octagonal element `pi`. -/ +def multiplyPi (u : Point) : Point := + ((u.1.1 + u.2.2, u.1.2 - u.1.1), (u.2.1 - u.1.2, u.2.2 - u.2.1)) + +/-- The translated coefficient descent map for a fixed parity class. -/ +def divide (e : ℤ) (u : Point) : Point := + (((u.1.1 - u.1.2 - u.2.1 - u.2.2 - e) / 2, (u.1.1 + u.1.2 - u.2.1 - u.2.2 - e) / 2), + ((u.1.1 + u.1.2 + u.2.1 - u.2.2 - e) / 2, (u.1.1 + u.1.2 + u.2.1 + u.2.2 - e) / 2)) + +theorem sqrt_two_sq : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (by norm_num) + +theorem integer_coefficients (a b : ℤ) (h : (a : ℝ) + (b : ℝ) * Real.sqrt 2 = 0) : + a = 0 ∧ b = 0 := by + by_cases hb : b = 0 + · simp only [hb, Int.cast_zero, zero_mul, add_zero] at h + exact ⟨by exact_mod_cast h, hb⟩ + · have hb' : (b : ℝ) ≠ 0 := by exact_mod_cast hb + exfalso + apply irrational_sqrt_two.ne_rat (-(a : ℚ) / (b : ℚ)) + push_cast + apply (eq_div_iff hb').mpr + nlinarith + +theorem integer_coefficients_equal (a b c d : ℤ) + (h : (a : ℝ) + (b : ℝ) * Real.sqrt 2 = (c : ℝ) + (d : ℝ) * Real.sqrt 2) : a = c ∧ b = d := by + have hh := integer_coefficients (a - c) (b - d) (by push_cast; linarith) + omega + +theorem height_squares (u : Point) : height u = + (u.1.1 ^ 2 + u.2.1 ^ 2 - u.1.2 ^ 2 - u.2.2 ^ 2) ^ 2 + + 2 * (u.1.1 * (u.1.2 + u.2.2) - u.2.1 * (u.1.2 - u.2.2)) ^ 2 := by + simp only [height, rationalPart, irrationalPart] + ring + +theorem height_nonneg (u : Point) : 0 ≤ height u := by + rw [height_squares] + positivity + +theorem height_product (u : Point) : (height u : ℝ) = + ((rationalPart u : ℝ) + (irrationalPart u : ℝ) * Real.sqrt 2)* + ((rationalPart u : ℝ) - (irrationalPart u : ℝ) * Real.sqrt 2) := by + simp only [height] + push_cast + ring_nf + rw [sqrt_two_sq] + +theorem height_eq_zero (u : Point) : height u = 0 ↔ u = 0 := by + constructor + · intro h + have hz : ((rationalPart u : ℝ) + (irrationalPart u : ℝ) * Real.sqrt 2)* + ((rationalPart u : ℝ) - (irrationalPart u : ℝ) * Real.sqrt 2) = 0 := by + rw [←height_product, h, Int.cast_zero] + have ha : rationalPart u = 0 := by + rcases mul_eq_zero.mp hz with h|h + · exact (integer_coefficients _ _ h).1 + · exact (integer_coefficients (rationalPart u) (-irrationalPart u) + (by push_cast; linarith)).1 + dsimp [rationalPart] at ha + have h1 : u.1.1 = 0 := by nlinarith [sq_nonneg u.1.2, sq_nonneg u.2.1, sq_nonneg u.2.2] + have h2 : u.1.2 = 0 := by nlinarith [sq_nonneg u.1.1, sq_nonneg u.2.1, sq_nonneg u.2.2] + have h3 : u.2.1 = 0 := by nlinarith [sq_nonneg u.1.1, sq_nonneg u.1.2, sq_nonneg u.2.2] + have h4 : u.2.2 = 0 := by nlinarith [sq_nonneg u.1.1, sq_nonneg u.1.2, sq_nonneg u.2.1] + exact Prod.ext (Prod.ext h1 h2) (Prod.ext h3 h4) + · rintro rfl + norm_num [height, rationalPart, irrationalPart] + +theorem embed_sub (u v : Point) : embed (u - v) = embed u - embed v := by + apply Complex.ext <;> simp only [embed, Complex.sub_re, Complex.sub_im, Prod.fst_sub, + Prod.snd_sub] + all_goals push_cast; ring + +theorem squared_norm (u : Point) : Complex.normSq (embed u) = + (rationalPart u : ℝ) + (irrationalPart u : ℝ) * Real.sqrt 2 := by + simp only [embed, Complex.normSq_apply, rationalPart, irrationalPart] + push_cast + ring_nf + rw [sqrt_two_sq] + ring + +theorem embed_injective : Function.Injective embed := by + intro u v h + have hh : Complex.normSq (embed (u - v)) = 0 := by rw [embed_sub, h, sub_self]; simp + rw [squared_norm] at hh + have hab := integer_coefficients _ _ hh + apply sub_eq_zero.mp + apply (height_eq_zero _).mp + simp [height, hab.1, hab.2] + +theorem distance_squared (u v : Point) : dist (embed u) (embed v) ^ 2 = + (rationalPart (u - v) : ℝ) + (irrationalPart (u - v) : ℝ) * Real.sqrt 2 := by + rw [Complex.dist_eq, ←Complex.normSq_eq_norm_sq, ←embed_sub, squared_norm] + +theorem distance_height (u v w z : Point) (h : dist (embed u) (embed v) = dist (embed w) (embed + z)) : + height (u - v) = height (w - z) := by + have hh := congrArg (fun r : ℝ => r ^ 2) h + rw [distance_squared, distance_squared] at hh + have hc := integer_coefficients_equal _ _ _ _ hh + simp only [height, hc.1, hc.2] + +theorem parity_zero_or_one (u : Point) : parity u = 0 ∨ parity u = 1 := by + dsimp [parity] + omega + +theorem height_mod_two (u : Point) : height u % 2 = parity u := by + have hs (a : ℤ) : a ^ 2 % 2 = a % 2 := by + have ha : a % 2 = 0 ∨ a % 2 = 1 := by omega + rcases ha with ha|ha <;> simp [pow_two, Int.mul_emod, ha] + rw [height, Int.sub_emod, hs, Int.mul_emod] + norm_num only [zero_mul, sub_zero, Int.emod_emod] + have h1 := hs u.1.1 + have h2 := hs u.1.2 + have h3 := hs u.2.1 + have h4 := hs u.2.2 + dsimp [rationalPart, parity] + omega + +theorem height_even_iff (u v : Point) : 2∣height (u - v) ↔ parity u = parity v := by + rw [Int.dvd_iff_emod_eq_zero, height_mod_two] + dsimp [parity] + omega + +theorem height_multiplyPi (u : Point) : height (multiplyPi u) = 2 * height u := by + simp only [height, rationalPart, irrationalPart, multiplyPi] + ring + +theorem divide_difference (e : ℤ) (u v : Point) (hu : parity u = e) (hv : parity v = e) : + multiplyPi (divide e u - divide e v) = u - v := by + dsimp [parity] at hu hv + apply Prod.ext <;> apply Prod.ext + all_goals dsimp [multiplyPi, divide]; omega + +theorem divide_height (e : ℤ) (u v : Point) (hu : parity u = e) (hv : parity v = e) : + height (u - v) = 2 * height (divide e u - divide e v) := by + rw [←height_multiplyPi, divide_difference e u v hu hv] + +/-- The nonzero octagonal element 1 - exp(pi*i/4) used for descent. -/ +noncomputable def pi : ℂ := embed ((1, -1), (0, 0)) + +theorem embed_zero : embed 0 = 0 := by + apply Complex.ext <;> simp [embed] + +theorem pi_ne_zero : pi ≠ 0 := by + intro h + have hh : (((1, -1), (0, 0)) : Point) = 0 := embed_injective (h.trans embed_zero.symm) + norm_num at hh + +theorem embed_multiplyPi (u : Point) : embed (multiplyPi u) = pi * embed u := by + apply Complex.ext + all_goals simp only [embed, multiplyPi, pi, Complex.mul_re, Complex.mul_im] + all_goals push_cast; ring_nf; rw [sqrt_two_sq] + all_goals ring + +theorem divide_distance (e : ℤ) (u v : Point) (hu : parity u = e) (hv : parity v = e) : + dist (embed u) (embed v) = ‖pi‖ * dist (embed (divide e u)) (embed (divide e v)) := by + rw [Complex.dist_eq, ←embed_sub, ←divide_difference e u v hu hv, embed_multiplyPi, + Complex.norm_mul, embed_sub, ←Complex.dist_eq] + +theorem height_symmetric (u v : Point) : height (u - v) = height (v - u) := by + simp only [height, rationalPart, irrationalPart, Prod.fst_sub, Prod.snd_sub] + ring + +end LeanPool.RareDistanceFields.OctagonalNorm diff --git a/LeanPool/RareDistanceFields/OctagonalRational.lean b/LeanPool/RareDistanceFields/OctagonalRational.lean new file mode 100644 index 0000000000..ab1d77f7ca --- /dev/null +++ b/LeanPool/RareDistanceFields/OctagonalRational.lean @@ -0,0 +1,154 @@ +/- +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.RareDistanceFields.OctagonalDescent +import Mathlib.RingTheory.Localization.Integer +import Mathlib.RingTheory.Localization.FractionRing + +/-! +# Both rare-distance assertions for coordinates in Q(sqrt(2)) + +See the project entry module for the exact coordinate restrictions and source roles. +Integer coefficient clearing is an actual complex similarity. The resulting +rare classes are counted in the original complete unordered distance graph. +-/ + +namespace LeanPool.RareDistanceFields.OctagonalRational + +open OctagonalNorm +noncomputable section + +variable {V : Type*} [Fintype V] + +open Classical in +/-- The complete simple distance graph on distinct configuration labels. -/ +def graph (x : V → ℂ) (d : ℝ) : SimpleGraph V := + OrderedColors.colorGraph (fun a b => dist (x a) (x b)) + (fun _ _ => dist_comm _ _) d + +open Classical in +/-- Occurring distances whose unordered multiplicities are at most the label count. -/ +def rareDistances (x : V → ℂ) : Finset ℝ := + (OrderedColors.palette (fun a b => dist (x a) (x b))).filter + fun d => (graph x d).edgeFinset.card ≤ Fintype.card V + +open Classical in +/-- Both real coordinates of each point have the form a + b*sqrt(2) with rational a, b. -/ +def QuadraticCoordinates (x : V → ℂ) : Prop := + ∀ i, ∃ a b c d : ℚ, (x i).re = (a : ℝ) + (b : ℝ) * Real.sqrt 2 ∧ + (x i).im = (c : ℝ) + (d : ℝ) * Real.sqrt 2 + +omit [Fintype V] in +open Classical in +theorem clear_coordinates [Finite V] (x : V → ℂ) (h : QuadraticCoordinates x) : + ∃ B : ℤ, B ≠ 0 ∧ ∃ y : V → Point, ∀ i, embed (y i) = (B : ℂ) * x i := by + let := Fintype.ofFinite V + choose a b c d hre him using h + let f : V × Fin 4 → ℚ := fun p => ![a p.1, b p.1 + d p.1, c p.1, d p.1 - b p.1] p.2 + obtain ⟨B, hB⟩ := IsLocalization.exist_integer_multiples_of_finite (nonZeroDivisors ℤ) f + choose coeff hcoeff using hB + refine ⟨B, nonZeroDivisors.ne_zero B.property, + (fun i => ((coeff (i, 0), coeff (i, 1)), (coeff (i, 2), coeff (i, 3)))), ?_⟩ + intro i + have h0 : (coeff (i, 0) : ℚ) = (B : ℤ) * a i := by simpa [f, zsmul_eq_mul] using hcoeff (i, 0) + have h1 : (coeff (i, 1) : ℚ) = (B : ℤ) * (b i + d i) := by + simpa [f, zsmul_eq_mul, mul_add] using hcoeff (i, 1) + have h2 : (coeff (i, 2) : ℚ) = (B : ℤ) * c i := by simpa [f, zsmul_eq_mul] using hcoeff (i, 2) + have h3 : (coeff (i, 3) : ℚ) = (B : ℤ) * (d i - b i) := by + simpa [f, zsmul_eq_mul] using hcoeff (i, 3) + have h0R : (coeff (i, 0) : ℝ) = (B : ℤ) * (a i : ℝ) := by exact_mod_cast h0 + have h1R : (coeff (i, 1) : ℝ) = (B : ℤ) * ((b i : ℝ) + (d i : ℝ)) := by exact_mod_cast h1 + have h2R : (coeff (i, 2) : ℝ) = (B : ℤ) * (c i : ℝ) := by exact_mod_cast h2 + have h3R : (coeff (i, 3) : ℝ) = (B : ℤ) * ((d i : ℝ) - (b i : ℝ)) := by exact_mod_cast h3 + apply Complex.ext + · change (coeff (i, 0) : ℝ) + (coeff (i, 1) - coeff (i, 3) : ℤ) * Real.sqrt 2 / 2 = + ((B : ℂ) * x i).re + simp only [Complex.mul_re, Complex.intCast_re, Complex.intCast_im, zero_mul, sub_zero] + push_cast + rw [h0R, h1R, h3R, hre i] + ring + · change (coeff (i, 2) : ℝ) + (coeff (i, 1) + coeff (i, 3) : ℤ) * Real.sqrt 2 / 2 = + ((B : ℂ) * x i).im + simp only [Complex.mul_im, Complex.intCast_re, Complex.intCast_im, zero_mul, add_zero] + push_cast + rw [h2R, h1R, h3R, him i] + ring + +open Classical in +theorem card_le_pow_of_scaled_integer (x : V → ℂ) (hx : Function.Injective x) + (B : ℤ) (hB : B ≠ 0) (y : V → Point) (hy : ∀ i, embed (y i) = (B : ℂ) * x i) : + Fintype.card V ≤ 2 ^ (rareDistances x).card := by + have hB' : (B : ℂ) ≠ 0 := by exact_mod_cast hB + have hnorm : ‖(B : ℂ)‖ ≠ 0 := norm_ne_zero_iff.mpr hB' + have hyinj : Function.Injective y := by + intro a b he + apply hx + apply mul_left_cancel₀ hB' + rw [←hy a, ←hy b, he] + have hscale (a b : V) : dist (embed (y a)) (embed (y b)) = ‖(B : ℂ)‖ * dist (x a) (x b) := by + rw [hy a, hy b, Complex.dist_eq, ←mul_sub, Complex.norm_mul, ←Complex.dist_eq] + let f : ℝ → ℝ := fun d => d / ‖(B : ℂ)‖ + have hf : Function.Injective f := by + intro a b he + exact (div_left_inj' hnorm).mp he + have heq (a b : V) (d : ℝ) : dist (embed (y a)) (embed (y b)) = d ↔ dist (x a) (x b) = f d := by + dsimp [f] + rw [hscale, eq_div_iff hnorm, mul_comm] + have hg (d : ℝ) : BinaryPalette.graph OctagonalDescent.model y d = graph x (f d) := by + ext a b + simp only [BinaryPalette.graph, graph, OrderedColors.colorGraph, + BinaryDescent.Model.distance, OctagonalDescent.model, heq] + have hsub : (OctagonalDescent.rareDistances y).image f ⊆ rareDistances x := by + intro d hd + obtain ⟨r, hr, rfl⟩ := Finset.mem_image.mp hd + obtain ⟨_, ⟨a, b, hab, he⟩, hc⟩ := (OctagonalDescent.rareDistances_spec y hyinj r).mp hr + apply Finset.mem_filter.mpr + exact ⟨Finset.mem_image.mpr ⟨(a, b), by simp [hab], (heq a b r).mp he⟩, hg r ▸ hc⟩ + have hc : (OctagonalDescent.rareDistances y).card ≤ (rareDistances x).card := by + have hh := Finset.card_le_card hsub + rwa [Finset.card_image_of_injective _ hf] at hh + exact (OctagonalDescent.card_le_pow_rareDistances y hyinj).trans + (Nat.pow_le_pow_right (by decide) hc) + +open Classical in +theorem card_le_pow_rareDistances (x : V → ℂ) (hx : Function.Injective x) + (h : QuadraticCoordinates x) : Fintype.card V ≤ 2 ^ (rareDistances x).card := by + obtain ⟨B, hB, y, hy⟩ := clear_coordinates x h + exact card_le_pow_of_scaled_integer x hx B hB y hy + +open Classical in +theorem two_rare_classes (x : V → ℂ) (hx : Function.Injective x) + (h : QuadraticCoordinates x) (hn : 3 ≤ Fintype.card V) : 2 ≤ (rareDistances x).card := by + have hb := card_le_pow_rareDistances x hx h + by_contra hc + have he : (rareDistances x).card = 0 ∨ (rareDistances x).card = 1 := by omega + rcases he with he|he <;> simp [he] at hb <;> omega + +open Classical in +theorem uniform_divergence (k : ℕ) : ∃ N : ℕ, ∀ {V : Type*} [Fintype V] + (x : V → ℂ), Function.Injective x → QuadraticCoordinates x → N ≤ Fintype.card V → + k ≤ (rareDistances x).card := by + refine ⟨2 ^ k, ?_⟩ + intro V inst x hx h hn + have hb := card_le_pow_rareDistances x hx h + by_contra hc + have hp : 2 ^ (rareDistances x).card < 2 ^ k := Nat.pow_lt_pow_right (by decide) (by omega) + omega + +open Classical in +theorem rareDistances_spec (x : V → ℂ) (hx : Function.Injective x) (d : ℝ) : + d ∈ rareDistances x ↔ 0 < d ∧ (∃ a b, a ≠ b ∧ dist (x a) (x b) = d) ∧ + (graph x d).edgeFinset.card ≤ Fintype.card V := by + constructor + · intro h + obtain ⟨hp, hc⟩ := Finset.mem_filter.mp h + obtain ⟨⟨a, b⟩, hab, he⟩ := Finset.mem_image.mp hp + have hn := (Finset.mem_offDiag.mp hab).2.2 + exact ⟨he ▸ dist_pos.mpr (hx.ne hn), ⟨a, b, hn, he⟩, hc⟩ + · rintro ⟨_, ⟨a, b, hab, he⟩, hc⟩ + exact Finset.mem_filter.mpr ⟨Finset.mem_image.mpr ⟨(a, b), by simp [hab], he⟩, hc⟩ + +end +end LeanPool.RareDistanceFields.OctagonalRational diff --git a/LeanPool/RareDistanceFields/OrderedColors.lean b/LeanPool/RareDistanceFields/OrderedColors.lean new file mode 100644 index 0000000000..dce02c32bc --- /dev/null +++ b/LeanPool/RareDistanceFields/OrderedColors.lean @@ -0,0 +1,118 @@ +/- +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.Combinatorics.SimpleGraph.DegreeSum + +/-! +# Two low-multiplicity colors from an increasing isosceles-base rule + +See the project entry module for the exact coordinate restrictions and source roles. +This is an abstract counting theorem. Its geometric application requires a +proved ordering in which two equal spokes always have a larger base color. +-/ + +namespace LeanPool.RareDistanceFields.OrderedColors + +noncomputable section + +variable {V C : Type*} [Fintype V] [LinearOrder C] + +open Classical in +/-- The simple graph of distinct pairs carrying a specified symmetric color. -/ +def colorGraph (q : V → V → C) (hsym : ∀ a b, q a b = q b a) (r : C) : SimpleGraph V where + Adj a b := a ≠ b ∧ q a b = r + symm := ⟨by + intro a b h + exact ⟨h.1.symm, (hsym b a).trans h.2⟩⟩ + +open Classical in +/-- The finite set of colors occurring between distinct labels. -/ +def palette (q : V → V → C) : Finset C := + Finset.univ.offDiag.image (fun p : V × V => q p.1 p.2) + +open Classical in +theorem mem_palette (q : V → V → C) (a b : V) (hab : a ≠ b) : q a b ∈ palette q := by + exact Finset.mem_image.mpr ⟨(a, b), by simp [Finset.mem_offDiag, hab], rfl⟩ + +open Classical in +/-- Equal-colored spokes on three distinct labels force a strictly larger base color. -/ +def IncreasingBases (q : V → V → C) : Prop := + ∀ a b c, a ≠ b → a ≠ c → b ≠ c → q a b = q a c → q a b < q b c + +open Classical in +theorem palette_card_gt_one (q : V → V → C) (h : IncreasingBases q) + (hn : 3 ≤ Fintype.card V) : 1 < (palette q).card := by + have hn' : 2 < (Finset.univ : Finset V).card := by + simp only [Finset.card_univ] + omega + obtain ⟨a, ha, b, hb, c, hc, hab, hac, hbc⟩ := Finset.two_lt_card.mp hn' + by_cases he : q a b = q a c + · exact Finset.one_lt_card.mpr ⟨q a b, mem_palette q a b hab, q b c, + mem_palette q b c hbc, ne_of_lt (h a b c hab hac hbc he)⟩ + · exact Finset.one_lt_card.mpr ⟨q a b, mem_palette q a b hab, q a c, + mem_palette q a c hac, he⟩ + +open Classical in +theorem degree_le_two (q : V → V → C) (hsym : ∀ a b, q a b = q b a) + (h : IncreasingBases q) (r D : C) + (hhigh : ∀ a b, a ≠ b → r < q a b → q a b = D) (p : V) : + (colorGraph q hsym r).degree p ≤ 2 := by + by_contra hn + have hc : 2 < ((colorGraph q hsym r).neighborFinset p).card := by + rw [SimpleGraph.card_neighborFinset_eq_degree] + omega + obtain ⟨a, ha, b, hb, c, hc, hab, hac, hbc⟩ := Finset.two_lt_card.mp hc + have hpa := (SimpleGraph.mem_neighborFinset _ _ _).mp ha + have hpb := (SimpleGraph.mem_neighborFinset _ _ _).mp hb + have hpc := (SimpleGraph.mem_neighborFinset _ _ _).mp hc + have qab : q a b = D := hhigh a b hab (hpa.2 ▸ h p a b hpa.1 hpb.1 hab (hpa.2.trans hpb.2.symm)) + have qac : q a c = D := hhigh a c hac (hpa.2 ▸ h p a c hpa.1 hpc.1 hac (hpa.2.trans hpc.2.symm)) + have qbc : q b c = D := hhigh b c hbc (hpb.2 ▸ h p b c hpb.1 hpc.1 hbc (hpb.2.trans hpc.2.symm)) + have hlt := h a b c hab hac hbc (qab.trans qac.symm) + rw [qab, qbc] at hlt + exact lt_irrefl _ hlt + +open Classical in +theorem multiplicity_le_card (q : V → V → C) (hsym : ∀ a b, q a b = q b a) + (h : IncreasingBases q) (r D : C) + (hhigh : ∀ a b, a ≠ b → r < q a b → q a b = D) : + (colorGraph q hsym r).edgeFinset.card ≤ Fintype.card V := by + have he : ∑ p, (colorGraph q hsym r).degree p ≤ ∑ _p : V, 2 := by + apply Finset.sum_le_sum + intro p hp + exact degree_le_two q hsym h r D hhigh p + rw [SimpleGraph.sum_degrees_eq_twice_card_edges] at he + simp only [Finset.sum_const, Finset.card_univ, smul_eq_mul] at he + omega + +open Classical in +/-- Both selected colors occur; both counts are unordered edge multiplicities. -/ +theorem two_rare_colors (q : V → V → C) (hsym : ∀ a b, q a b = q b a) + (h : IncreasingBases q) (hn : 3 ≤ Fintype.card V) : + ∃ r ∈ palette q, ∃ D ∈ palette q, r ≠ D ∧ + (colorGraph q hsym r).edgeFinset.card ≤ Fintype.card V ∧ + (colorGraph q hsym D).edgeFinset.card ≤ Fintype.card V := by + have hc := palette_card_gt_one q h hn + have hp : (palette q).Nonempty := Finset.card_pos.mp (by omega) + obtain ⟨D, hD, hmax⟩ := Finset.exists_max_image (palette q) id hp + have he : ((palette q).erase D).Nonempty := by + apply Finset.card_pos.mp + rw [Finset.card_erase_of_mem hD] + omega + obtain ⟨r, hr, hrmax⟩ := Finset.exists_max_image ((palette q).erase D) id he + have hrD := (Finset.mem_erase.mp hr).1 + refine ⟨r, (Finset.mem_erase.mp hr).2, D, hD, hrD, ?_, ?_⟩ + · apply multiplicity_le_card q hsym h r D + intro a b hab habr + by_contra heq + have habmem : q a b ∈ (palette q).erase D := + Finset.mem_erase.mpr ⟨heq, mem_palette q a b hab⟩ + exact (not_lt_of_ge (hrmax _ habmem)) habr + · apply multiplicity_le_card q hsym h D D + intro a b hab hlt + exact False.elim ((not_lt_of_ge (hmax _ (mem_palette q a b hab))) hlt) + +end +end LeanPool.RareDistanceFields.OrderedColors diff --git a/LeanPool/RareDistanceFields/PolynomialSpecialization.lean b/LeanPool/RareDistanceFields/PolynomialSpecialization.lean new file mode 100644 index 0000000000..151002cd78 --- /dev/null +++ b/LeanPool/RareDistanceFields/PolynomialSpecialization.lean @@ -0,0 +1,148 @@ +/- +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.RareDistanceFields.DistancePattern +import Mathlib.Algebra.MvPolynomial.Funext +import Mathlib.RingTheory.AlgebraicIndependent.Basic + +/-! +# Exact specialization of polynomial coordinate families + +See the project entry module for the exact coordinate restrictions and source roles. +Rational polynomials evaluated at algebraically independent real parameters +admit a rational specialization preserving every equality and inequality of +distance labels (equality versus disequality, not numerical order). Thus both +rare-distance assertions follow with n <= 2^r for this coordinate regime. +Algebraic dependence of the parameters is not covered. +-/ + +namespace LeanPool.RareDistanceFields.PolynomialSpecialization + +noncomputable section + +variable {σ : Type*} + +open Classical in +/-- A finite family of rational polynomials has an evaluation separating its members. -/ +theorem exists_injective_eval (S : Finset (MvPolynomial σ ℚ)) : + ∃ u : σ → ℚ, Set.InjOn (MvPolynomial.eval u) S := by + classical + let D := S.offDiag + let P : MvPolynomial σ ℚ := ∏ e ∈ D, (e.1 - e.2) + have hP : P ≠ 0 := by + apply Finset.prod_ne_zero_iff.mpr + intro e he + exact sub_ne_zero.mpr (Finset.mem_offDiag.mp he).2.2 + have he : ∃ u : σ → ℚ, (MvPolynomial.eval u) P ≠ 0 := by + by_contra h + push Not at h + apply hP + apply MvPolynomial.funext + intro u + simpa using h u + obtain ⟨u, hu⟩ := he + refine ⟨u, ?_⟩ + intro p hp q hq hpq + by_contra hne + have hmem : (p, q) ∈ D := Finset.mem_offDiag.mpr ⟨hp, hq, hne⟩ + have hh : ∀ e ∈ D, (MvPolynomial.eval u) (e.1 - e.2) ≠ 0 := by + have hz := hu + dsimp [P] at hz + rw [map_prod] at hz + exact Finset.prod_ne_zero_iff.mp hz + apply hh (p, q) hmem + simpa using sub_eq_zero.mpr hpq + +variable {V : Type*} [Fintype V] + +open Classical in +/-- Two rational multivariate polynomials for every configuration label. -/ +abbrev Coordinates (σ V : Type*) := V → MvPolynomial σ ℚ × MvPolynomial σ ℚ + +open Classical in +/-- The polynomial expression for the squared distance of two labeled points. -/ +def sqPolynomial (P : Coordinates σ V) (a b : V) : MvPolynomial σ ℚ := + ((P a).1 - (P b).1) ^ 2 + ((P a).2 - (P b).2) ^ 2 + +open Classical in +/-- The complex point obtained by evaluating the coordinate polynomials over the reals. -/ +def realPoint (P : Coordinates σ V) (t : σ → ℝ) (a : V) : ℂ := + ⟨(MvPolynomial.aeval t) (P a).1, (MvPolynomial.aeval t) (P a).2⟩ + +open Classical in +/-- The rational point obtained by evaluating the coordinate polynomials over the rationals. -/ +def rationalPoint (P : Coordinates σ V) (u : σ → ℚ) (a : V) : ℚ × ℚ := + ⟨(MvPolynomial.eval u) (P a).1, (MvPolynomial.eval u) (P a).2⟩ + +omit [Fintype V] in +open Classical in +theorem real_dist_sq (P : Coordinates σ V) (t : σ → ℝ) (a b : V) : + dist (realPoint P t a) (realPoint P t b) ^ 2 = (MvPolynomial.aeval t) (sqPolynomial P a b) := by + rw [Complex.dist_eq, ← Complex.normSq_eq_norm_sq] + simp [realPoint, sqPolynomial, Complex.normSq_apply, pow_two] + +omit [Fintype V] in +open Classical in +theorem rational_sqDist (P : Coordinates σ V) (u : σ → ℚ) (a b : V) : + RationalPlane.sqDist (rationalPoint P u a) (rationalPoint P u b) = + (MvPolynomial.eval u) (sqPolynomial P a b) := by + simp [RationalPlane.sqDist, rationalPoint, sqPolynomial] + +omit [Fintype V] in +open Classical in +/-- A genuine rational realization of the original whole distance-equality pattern. -/ +theorem exists_rational_pattern [Finite V] (P : Coordinates σ V) (t : σ → ℝ) + (ht : AlgebraicIndependent ℚ t) : + ∃ u : σ → ℚ, DistancePattern.SamePattern (rationalPoint P u) (realPoint P t) := by + let := Fintype.ofFinite V + let S := (Finset.univ : Finset (V × V)).image fun e => sqPolynomial P e.1 e.2 + obtain ⟨u, hu⟩ := exists_injective_eval S + refine ⟨u, ?_⟩ + have hmem (a b : V) : sqPolynomial P a b ∈ S := Finset.mem_image.mpr ⟨(a, b), by simp, rfl⟩ + intro a b c d + rw [rational_sqDist, rational_sqDist] + constructor + · intro h + have he := hu (hmem a b) (hmem c d) h + have hh := congrArg (MvPolynomial.aeval t) he + rw [← real_dist_sq, ← real_dist_sq] at hh + nlinarith [dist_nonneg (x := realPoint P t a) (y := realPoint P t b), + dist_nonneg (x := realPoint P t c) (y := realPoint P t d)] + · intro h + have hh := congrArg (fun r : ℝ => r ^ 2) h + rw [real_dist_sq, real_dist_sq] at hh + exact congrArg (MvPolynomial.eval u) (ht hh) + +open Classical in +theorem card_le_pow_rare (P : Coordinates σ V) (t : σ → ℝ) + (ht : AlgebraicIndependent ℚ t) (hx : Function.Injective (realPoint P t)) : + Fintype.card V ≤ 2 ^ (DistancePattern.rareDistances (realPoint P t)).card := by + obtain ⟨u, hu⟩ := exists_rational_pattern P t ht + exact DistancePattern.card_le_pow_rare (rationalPoint P u) (realPoint P t) hx hu + +open Classical in +theorem two_rare_distances (P : Coordinates σ V) (t : σ → ℝ) + (ht : AlgebraicIndependent ℚ t) (hx : Function.Injective (realPoint P t)) + (hn : 3 ≤ Fintype.card V) : + ∃ d ∈ DistancePattern.rareDistances (realPoint P t), + ∃ e ∈ DistancePattern.rareDistances (realPoint P t), d ≠ e := by + obtain ⟨u, hu⟩ := exists_rational_pattern P t ht + exact DistancePattern.two_rare_distances (rationalPoint P u) (realPoint P t) hx hu hn + +open Classical in +theorem uniform_divergence (k : ℕ) : ∃ N : ℕ, ∀ {σ V : Type*} [Fintype V] (P : Coordinates σ V) + (t : σ → ℝ), + AlgebraicIndependent ℚ t → Function.Injective (realPoint P t) → + N ≤ Fintype.card V → k ≤ (DistancePattern.rareDistances (realPoint P t)).card := by + refine ⟨2 ^ k, ?_⟩ + intro σ V inst P t ht hx hn + have h := card_le_pow_rare P t ht hx + by_contra hr + have hp : 2 ^ (DistancePattern.rareDistances (realPoint P t)).card < 2 ^ k := + Nat.pow_lt_pow_right (by decide) (by omega) + omega + +end +end LeanPool.RareDistanceFields.PolynomialSpecialization diff --git a/LeanPool/RareDistanceFields/PureTranscendental.lean b/LeanPool/RareDistanceFields/PureTranscendental.lean new file mode 100644 index 0000000000..66f2077217 --- /dev/null +++ b/LeanPool/RareDistanceFields/PureTranscendental.lean @@ -0,0 +1,144 @@ +/- +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.RareDistanceFields.PolynomialSpecialization +import Mathlib.Algebra.Algebra.Hom.Rat +import Mathlib.RingTheory.Localization.FractionRing + +/-! +# Planar sets over purely transcendental fields + +See the project entry module for the exact coordinate restrictions and source roles. +For any real embedding of the fraction field of Q[variables], all finite planar +configurations admit rational realizations of exactly the same distance-equality +pattern. Common denominators are cleared before polynomial specialization. +This proves both rare-distance assertions in this regime. Nontrivial algebraic +extensions of the rational function field are not included. +-/ + +namespace LeanPool.RareDistanceFields.PureTranscendental + +noncomputable section + +open Classical in +/-- The rational function field in the specified family of variables over the rationals. -/ +abbrev Functions (σ : Type*) := FractionRing (MvPolynomial σ ℚ) + +variable {σ : Type*} + +open Classical in +/-- Algebraically independent parameters supply the required real field embedding. -/ +def embedding (t : σ → ℝ) (ht : AlgebraicIndependent ℚ t) : Functions σ →ₐ[ℚ] ℝ := + (IsFractionRing.lift + (g := (MvPolynomial.aeval t : MvPolynomial σ ℚ →ₐ[ℚ] ℝ).toRingHom) ht).toRatAlgHom + +open Classical in +theorem embedding_variables (t : σ → ℝ) (ht : AlgebraicIndependent ℚ t) (i : σ) : + embedding t ht (algebraMap (MvPolynomial σ ℚ) (Functions σ) (MvPolynomial.X i)) = t i := by + change (IsFractionRing.lift + (g := (MvPolynomial.aeval t : MvPolynomial σ ℚ →ₐ[ℚ] ℝ).toRingHom) ht) + (algebraMap (MvPolynomial σ ℚ) (Functions σ) (MvPolynomial.X i)) = t i + exact (IsFractionRing.lift_algebraMap + (g := (MvPolynomial.aeval t : MvPolynomial σ ℚ →ₐ[ℚ] ℝ).toRingHom) + ht (MvPolynomial.X i)).trans (MvPolynomial.aeval_X t i) + +open Classical in +theorem real_embedding_exists : Nonempty (Functions Empty →ₐ[ℚ] ℝ) := + ⟨embedding Empty.elim algebraicIndependent_empty_type⟩ + +variable {V : Type*} [Fintype V] + +open Classical in +/-- The planar point obtained from a pair of rational functions under a real embedding. -/ +def point (f : Functions σ →ₐ[ℚ] ℝ) (x : V → Functions σ × Functions σ) (a : V) : ℂ := + ⟨f (x a).1, f (x a).2⟩ + +omit [Fintype V] in +open Classical in +theorem exists_rational_pattern [Finite V] (f : Functions σ →ₐ[ℚ] ℝ) + (x : V → Functions σ × Functions σ) : + ∃ y : V → ℚ × ℚ, DistancePattern.SamePattern y (point f x) := by + let := Fintype.ofFinite V + classical + let R := MvPolynomial σ ℚ + let K := Functions σ + let g : R →ₐ[ℚ] ℝ := (f.toRingHom.comp (algebraMap R K)).toRatAlgHom + have hg : Function.Injective g := + f.injective.comp (IsFractionRing.injective R K) + let t : σ → ℝ := fun i => g (MvPolynomial.X i) + have hgt : g = MvPolynomial.aeval t := MvPolynomial.aeval_unique g + have ht : AlgebraicIndependent ℚ t := by + change Function.Injective (MvPolynomial.aeval t) + rwa [← hgt] + let coordinates : V × Bool → K := fun e => if e.2 then (x e.1).1 else (x e.1).2 + obtain ⟨B, hB⟩ := IsLocalization.exist_integer_multiples_of_finite (nonZeroDivisors R) coordinates + have hc (a : V) : ∃ p q : R, + algebraMap R K p = algebraMap R K (B : R) * (x a).1 ∧ + algebraMap R K q = algebraMap R K (B : R) * (x a).2 := by + obtain ⟨p, hp⟩ := hB (a, true) + obtain ⟨q, hq⟩ := hB (a, false) + exact ⟨p, q, by simpa [coordinates, Algebra.smul_def] using hp, + by simpa [coordinates, Algebra.smul_def] using hq⟩ + choose p q hp hq using hc + let P : PolynomialSpecialization.Coordinates σ V := fun a => (p a, q a) + let d : ℝ := g B + have hBne : (B : R) ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.mp B.property + have hd : d ≠ 0 := by + intro hz + apply hBne + apply hg + simpa [d] using hz + have hpoint (a : V) : PolynomialSpecialization.realPoint P t a = + (d : ℂ) * point f x a := by + have hpa := congrArg f (hp a) + have hqa := congrArg f (hq a) + have hpa' : g (p a) = d * f (x a).1 := by simpa [g, d] using hpa + have hqa' : g (q a) = d * f (x a).2 := by simpa [g, d] using hqa + apply Complex.ext + · simpa [PolynomialSpecialization.realPoint, P, point, ← hgt] using hpa' + · simpa [PolynomialSpecialization.realPoint, P, point, ← hgt] using hqa' + have hscale (a b : V) : + dist (PolynomialSpecialization.realPoint P t a) + (PolynomialSpecialization.realPoint P t b) = + |d| * dist (point f x a) (point f x b) := by + rw [hpoint, hpoint] + simp [Complex.dist_eq, ← mul_sub, Complex.norm_real] + obtain ⟨u, hu⟩ := PolynomialSpecialization.exists_rational_pattern P t ht + refine ⟨PolynomialSpecialization.rationalPoint P u, ?_⟩ + intro a b c e + rw [hu a b c e, hscale, hscale] + exact ⟨mul_left_cancel₀ (abs_ne_zero.mpr hd), congrArg (fun z : ℝ => |d| * z)⟩ + +open Classical in +theorem card_le_pow_rare (f : Functions σ →ₐ[ℚ] ℝ) + (x : V → Functions σ × Functions σ) (hx : Function.Injective (point f x)) : + Fintype.card V ≤ 2 ^ (DistancePattern.rareDistances (point f x)).card := by + obtain ⟨y, hy⟩ := exists_rational_pattern f x + exact DistancePattern.card_le_pow_rare y (point f x) hx hy + +open Classical in +theorem two_rare_distances (f : Functions σ →ₐ[ℚ] ℝ) + (x : V → Functions σ × Functions σ) (hx : Function.Injective (point f x)) + (hn : 3 ≤ Fintype.card V) : + ∃ d ∈ DistancePattern.rareDistances (point f x), + ∃ e ∈ DistancePattern.rareDistances (point f x), d ≠ e := by + obtain ⟨y, hy⟩ := exists_rational_pattern f x + exact DistancePattern.two_rare_distances y (point f x) hx hy hn + +open Classical in +theorem uniform_divergence (k : ℕ) : ∃ N : ℕ, ∀ {σ V : Type*} [Fintype V] + (f : Functions σ →ₐ[ℚ] ℝ) (x : V → Functions σ × Functions σ), + Function.Injective (point f x) → N ≤ Fintype.card V → + k ≤ (DistancePattern.rareDistances (point f x)).card := by + refine ⟨2 ^ k, ?_⟩ + intro σ V inst f x hx hn + have h := card_le_pow_rare f x hx + by_contra hr + have hp : 2 ^ (DistancePattern.rareDistances (point f x)).card < 2 ^ k := + Nat.pow_lt_pow_right (by decide) (by omega) + omega + +end +end LeanPool.RareDistanceFields.PureTranscendental diff --git a/LeanPool/RareDistanceFields/RationalDivergence.lean b/LeanPool/RareDistanceFields/RationalDivergence.lean new file mode 100644 index 0000000000..3cde024195 --- /dev/null +++ b/LeanPool/RareDistanceFields/RationalDivergence.lean @@ -0,0 +1,168 @@ +/- +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.RareDistanceFields.IntegerDivergence +import LeanPool.RareDistanceFields.RationalPlane + +/-! +# Both rare-distance assertions for rational-coordinate planar sets + +See the project entry module for the exact coordinate restrictions and source roles. +Clearing denominators preserves every distance class and its unordered count. +For n rational-coordinate planar points and r occurring positive Euclidean +lengths of multiplicity at most n, the theorem below proves n <= 2^r. +No reduction of arbitrary real planar configurations is claimed. +-/ + +namespace LeanPool.RareDistanceFields.RationalDivergence + +open RationalPlane +noncomputable section + +variable {V : Type*} [Fintype V] + +open Classical in +/-- Occurring rational squared distances with multiplicity at most the label count. -/ +def rareSquared (x : V → Point) : Finset ℚ := + (OrderedColors.palette (fun a b => sqDist (x a) (x b))).filter + fun r => (graph x r).edgeFinset.card ≤ Fintype.card V + +open Classical in +/-- Occurring Euclidean distances with unordered multiplicity at most the label count. -/ +def rareDistances (x : V → Point) : Finset ℝ := + (OrderedColors.palette (fun a b => dist (complexPoint (x a)) (complexPoint (x b)))).filter + fun r => (distanceGraph x r).edgeFinset.card ≤ Fintype.card V + +open Classical in +theorem exists_pair_of_mem_rareSquared (x : V → Point) {r : ℚ} (hr : r ∈ rareSquared x) : + ∃ a b, a ≠ b ∧ sqDist (x a) (x b) = r := by + obtain ⟨⟨a, b⟩, hab, he⟩ := Finset.mem_image.mp (Finset.mem_filter.mp hr).1 + exact ⟨a, b, (Finset.mem_offDiag.mp hab).2.2, he⟩ + +open Classical in +theorem rareSquared_positive (x : V → Point) (hx : Function.Injective x) + {r : ℚ} (hr : r ∈ rareSquared x) : 0 < r := by + obtain ⟨a, b, hab, rfl⟩ := exists_pair_of_mem_rareSquared x hr + exact sqDist_pos _ _ (hx.ne hab) + +open Classical in +theorem card_le_pow_rareSquared (x : V → Point) (hx : Function.Injective x) : + Fintype.card V ≤ 2 ^ (rareSquared x).card := by + classical + obtain ⟨B, hB, y, hy⟩ := clear_denominators x + have hB' : (B : ℚ) ≠ 0 := by exact_mod_cast hB + have hB2 : (B : ℚ) ^ 2 ≠ 0 := pow_ne_zero 2 hB' + have hscale (p q : V) : (IntegerPlane.sqDist (y p) (y q) : ℚ) = + (B : ℚ) ^ 2 * sqDist (x p) (x q) := by + dsimp [IntegerPlane.sqDist, DyadicNorm.normSq, sqDist] + push_cast + rw [(hy p).1, (hy p).2, (hy q).1, (hy q).2] + ring + have hyinj : Function.Injective y := by + intro p q he + apply hx + apply Prod.ext + · apply mul_left_cancel₀ hB' + rw [← (hy p).1, ← (hy q).1, he] + · apply mul_left_cancel₀ hB' + rw [← (hy p).2, ← (hy q).2, he] + let f : ℤ → ℚ := fun r => (r : ℚ) / (B : ℚ) ^ 2 + have hf : Function.Injective f := by + intro r s he + apply Int.cast_injective (α := ℚ) + have hh := congrArg (fun q : ℚ => q * (B : ℚ) ^ 2) he + simpa [f, hB2] using hh + have heq (p q : V) (r : ℤ) : IntegerPlane.sqDist (y p) (y q) = r ↔ + sqDist (x p) (x q) = f r := by + constructor + · intro h + apply (eq_div_iff hB2).mpr + rw [mul_comm, ← hscale, h] + · intro h + apply Int.cast_injective (α := ℚ) + rw [hscale, h] + dsimp [f] + field_simp + have hg (r : ℤ) : IntegerPlane.graph y r = graph x (f r) := by + ext p q + simp only [IntegerPlane.graph, graph, OrderedColors.colorGraph, heq] + have hsub : (IntegerDivergence.rareSquared y).image f ⊆ rareSquared x := by + intro r hr + obtain ⟨s, hs, rfl⟩ := Finset.mem_image.mp hr + have hs' := Finset.mem_filter.mp hs + obtain ⟨a, b, hab, he⟩ := IntegerDivergence.exists_pair_of_mem_palette y hs'.1 + apply Finset.mem_filter.mpr + refine ⟨Finset.mem_image.mpr ⟨(a, b), by simp [hab], (heq a b s).mp he⟩, ?_⟩ + exact hg s ▸ hs'.2 + have hc : (IntegerDivergence.rareSquared y).card ≤ (rareSquared x).card := by + have hh := Finset.card_le_card hsub + rwa [Finset.card_image_of_injective _ hf] at hh + exact (IntegerDivergence.card_le_pow_rare y hyinj).trans + (Nat.pow_le_pow_right (by decide) hc) + +open Classical in +theorem sqrt_sqDist (p q : Point) : + Real.sqrt (sqDist p q : ℝ) = dist (complexPoint p) (complexPoint q) := by + rw [← complex_dist_sq] + exact Real.sqrt_sq (dist_nonneg) + +open Classical in +theorem rareSquared_card_le_rareDistances (x : V → Point) (hx : Function.Injective x) : + (rareSquared x).card ≤ (rareDistances x).card := by + classical + apply Finset.card_le_card_of_injOn (fun r : ℚ => Real.sqrt (r : ℝ)) + · intro r hr + obtain ⟨a, b, hab, he⟩ := exists_pair_of_mem_rareSquared x hr + have hs : Real.sqrt (r : ℝ) = dist (complexPoint (x a)) (complexPoint (x b)) := by + rw [← he, sqrt_sqDist] + apply Finset.mem_filter.mpr + refine ⟨Finset.mem_image.mpr ⟨(a, b), by simp [hab], hs.symm⟩, ?_⟩ + have hm := (Finset.mem_filter.mp hr).2 + rw [← he, graph_eq_distanceGraph] at hm + change (distanceGraph x (Real.sqrt (r : ℝ))).edgeFinset.card ≤ Fintype.card V + rwa [hs] + · intro r hr s hs he + have hrp : (0 : ℝ) ≤ (r : ℝ) := by exact_mod_cast (rareSquared_positive x hx hr).le + have hsp : (0 : ℝ) ≤ (s : ℝ) := by exact_mod_cast (rareSquared_positive x hx hs).le + have hh := congrArg (fun a : ℝ => a ^ 2) he + rw [Real.sq_sqrt hrp, Real.sq_sqrt hsp] at hh + exact_mod_cast hh + +open Classical in +/-- A quantitative bound using actual positive Euclidean distance classes. -/ +theorem card_le_pow_rareDistances (x : V → Point) (hx : Function.Injective x) : + Fintype.card V ≤ 2 ^ (rareDistances x).card := + (card_le_pow_rareSquared x hx).trans + (Nat.pow_le_pow_right (by decide) (rareSquared_card_le_rareDistances x hx)) + +open Classical in +theorem rareDistances_spec (x : V → Point) (hx : Function.Injective x) + {d : ℝ} (hd : d ∈ rareDistances x) : 0 < d ∧ + (∃ a b, dist (complexPoint (x a)) (complexPoint (x b)) = d) ∧ + (distanceGraph x d).edgeFinset.card ≤ Fintype.card V := by + have hd' := Finset.mem_filter.mp hd + obtain ⟨⟨a, b⟩, hab, he⟩ := Finset.mem_image.mp hd'.1 + dsimp only at he + refine ⟨?_, ⟨a, b, he⟩, hd'.2⟩ + have hp := sqDist_pos (x a) (x b) (hx.ne (Finset.mem_offDiag.mp hab).2.2) + have hp' : (0 : ℝ) < (sqDist (x a) (x b) : ℝ) := by exact_mod_cast hp + rw [← complex_dist_sq, he] at hp' + have hn : 0 ≤ d := he ▸ dist_nonneg + nlinarith + +open Classical in +/-- Uniform divergence for rational-coordinate planar sets; N=2^k suffices. -/ +theorem uniform_divergence (k : ℕ) : ∃ N : ℕ, ∀ {V : Type*} [Fintype V] + (x : V → Point), Function.Injective x → N ≤ Fintype.card V → + k ≤ (rareDistances x).card := by + refine ⟨2 ^ k, ?_⟩ + intro V inst x hx hn + have hh := card_le_pow_rareDistances x hx + by_contra h + have hp : 2 ^ (rareDistances x).card < 2 ^ k := Nat.pow_lt_pow_right (by decide) (by omega) + omega + +end +end LeanPool.RareDistanceFields.RationalDivergence diff --git a/LeanPool/RareDistanceFields/RationalPlane.lean b/LeanPool/RareDistanceFields/RationalPlane.lean new file mode 100644 index 0000000000..e4998d8c9f --- /dev/null +++ b/LeanPool/RareDistanceFields/RationalPlane.lean @@ -0,0 +1,175 @@ +/- +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.RareDistanceFields.IntegerPlane +import Mathlib.Analysis.Complex.Basic +import Mathlib.RingTheory.Localization.Integer +import Mathlib.RingTheory.Localization.FractionRing + +/-! +# Two rare distances for finite rational-coordinate planar sets + +See the project entry module for the exact coordinate restrictions and source roles. +A single nonzero integer clears every coordinate denominator. The integer +dyadic theorem then transports both occurring distance classes and their exact +unordered multiplicities back to the original rational points. +Rational coordinates are an explicit restriction, not a reduction of arbitrary +real planar sets or of all sets with rational squared distances. +-/ + +namespace LeanPool.RareDistanceFields.RationalPlane + +noncomputable section + +open Classical in +/-- A rational coordinate pair in the plane. -/ +abbrev Point := ℚ × ℚ +variable {V : Type*} [Fintype V] + +open Classical in +/-- The rational squared Euclidean distance between two points. -/ +def sqDist (p q : Point) : ℚ := (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 + +open Classical in +theorem sqDist_symm (p q : Point) : sqDist p q = sqDist q p := by + dsimp [sqDist]; ring + +open Classical in +theorem sqDist_pos (p q : Point) (hne : p ≠ q) : 0 < sqDist p q := by + dsimp [sqDist] + have hn : p.1 ≠ q.1 ∨ p.2 ≠ q.2 := by + by_contra h + push Not at h + exact hne (Prod.ext h.1 h.2) + rcases hn with hn|hn + · nlinarith [sq_pos_of_ne_zero (sub_ne_zero.mpr hn), sq_nonneg (p.2 - q.2)] + · nlinarith [sq_pos_of_ne_zero (sub_ne_zero.mpr hn), sq_nonneg (p.1 - q.1)] + +open Classical in +/-- The simple graph of distinct labels at a specified rational squared distance. -/ +def graph (x : V → Point) (r : ℚ) : SimpleGraph V := + OrderedColors.colorGraph (fun a b => sqDist (x a) (x b)) + (fun a b => sqDist_symm (x a) (x b)) r + +omit [Fintype V] in +open Classical in +theorem clear_denominators [Finite V] (x : V → Point) : + ∃ B : ℤ, B ≠ 0 ∧ ∃ y : V → IntegerPlane.Point, + ∀ p, ((y p).1 : ℚ) = B * (x p).1 ∧ ((y p).2 : ℚ) = B * (x p).2 := by + let := Fintype.ofFinite V + let f : V × Bool → ℚ := fun p => if p.2 then (x p.1).1 else (x p.1).2 + obtain ⟨B, hB⟩ := IsLocalization.exist_integer_multiples_of_finite (nonZeroDivisors ℤ) f + have hc : ∀ p : V, ∃ a b : ℤ, (a : ℚ) = (B : ℤ) * (x p).1 ∧ (b : ℚ) = (B : ℤ) * (x p).2 := by + intro p + obtain ⟨a, ha⟩ := hB (p, true) + obtain ⟨b, hb⟩ := hB (p, false) + refine ⟨a, b, ?_, ?_⟩ + · simpa [f, zsmul_eq_mul] using ha + · simpa [f, zsmul_eq_mul] using hb + choose a b ha hb using hc + exact ⟨B, nonZeroDivisors.ne_zero B.property, fun p => (a p, b p), fun p => ⟨ha p, hb p⟩⟩ + +open Classical in +theorem two_rare_squared_distances (x : V → Point) (hx : Function.Injective x) + (hn : 3 ≤ Fintype.card V) : + ∃ a b c d : V, a ≠ b ∧ c ≠ d ∧ sqDist (x a) (x b) ≠ sqDist (x c) (x d) ∧ + (graph x (sqDist (x a) (x b))).edgeFinset.card ≤ Fintype.card V ∧ + (graph x (sqDist (x c) (x d))).edgeFinset.card ≤ Fintype.card V := by + obtain ⟨B, hB, y, hy⟩ := clear_denominators x + have hB' : (B : ℚ) ≠ 0 := by exact_mod_cast hB + have hscale (p r : V) : (IntegerPlane.sqDist (y p) (y r) : ℚ) = + (B : ℚ) ^ 2 * sqDist (x p) (x r) := by + dsimp [IntegerPlane.sqDist, DyadicNorm.normSq, sqDist] + push_cast + rw [(hy p).1, (hy p).2, (hy r).1, (hy r).2] + ring + have hyinj : Function.Injective y := by + intro p r h + apply hx + apply Prod.ext + · apply mul_left_cancel₀ hB' + rw [← (hy p).1, ← (hy r).1, h] + · apply mul_left_cancel₀ hB' + rw [← (hy p).2, ← (hy r).2, h] + have heq (p r a b : V) : + IntegerPlane.sqDist (y p) (y r) = IntegerPlane.sqDist (y a) (y b) ↔ + sqDist (x p) (x r) = sqDist (x a) (x b) := by + constructor + · intro h + have hh := congrArg (fun z : ℤ => (z : ℚ)) h + rw [hscale, hscale] at hh + exact mul_left_cancel₀ (pow_ne_zero 2 hB') hh + · intro h + apply Int.cast_injective (α := ℚ) + rw [hscale, hscale, h] + have hg (a b : V) : IntegerPlane.graph y (IntegerPlane.sqDist (y a) (y b)) = + graph x (sqDist (x a) (x b)) := by + ext p r + simp only [IntegerPlane.graph, graph, OrderedColors.colorGraph, heq] + obtain ⟨a, b, c, d, hab, hcd, hne, hr, hs⟩ := IntegerPlane.two_rare_distances y hyinj hn + exact ⟨a, b, c, d, hab, hcd, fun h => hne ((heq a b c d).mpr h), hg a b ▸ hr, hg c d ▸ hs⟩ + +open Classical in +/-- The standard complex embedding of a rational coordinate pair. -/ +noncomputable def complexPoint (p : Point) : ℂ := ⟨p.1, p.2⟩ + +open Classical in +theorem complex_dist_sq (p q : Point) : + dist (complexPoint p) (complexPoint q) ^ 2 = (sqDist p q : ℝ) := by + rw [Complex.dist_eq, ← Complex.normSq_eq_norm_sq] + simp only [Complex.normSq_apply, Complex.sub_re, Complex.sub_im, complexPoint, sqDist] + push_cast + ring + +open Classical in +/-- The simple graph of distinct labels at a specified embedded Euclidean distance. -/ +def distanceGraph (x : V → Point) (d : ℝ) : SimpleGraph V := + OrderedColors.colorGraph (fun p q => dist (complexPoint (x p)) (complexPoint (x q))) + (fun _ _ => dist_comm _ _) d + +omit [Fintype V] in +open Classical in +theorem graph_eq_distanceGraph (x : V → Point) (a b : V) : + graph x (sqDist (x a) (x b)) = + distanceGraph x (dist (complexPoint (x a)) (complexPoint (x b))) := by + ext p q + simp only [graph, distanceGraph, OrderedColors.colorGraph] + apply and_congr_right + intro _hpq + constructor + · intro h + have hh := congrArg (fun z : ℚ => (z : ℝ)) h + rw [← complex_dist_sq, ← complex_dist_sq] at hh + nlinarith [dist_nonneg (x := complexPoint (x p)) (y := complexPoint (x q)), + dist_nonneg (x := complexPoint (x a)) (y := complexPoint (x b))] + · intro h + apply Rat.cast_injective (α := ℝ) + rw [← complex_dist_sq, ← complex_dist_sq, h] + +open Classical in +/-- Two occurring positive Euclidean lengths, with unordered multiplicities at most n. -/ +theorem two_rare_euclidean_distances (x : V → Point) (hx : Function.Injective x) + (hn : 3 ≤ Fintype.card V) : + ∃ d e : ℝ, 0 < d ∧ 0 < e ∧ d ≠ e ∧ + (∃ a b, dist (complexPoint (x a)) (complexPoint (x b)) = d) ∧ + (∃ a b, dist (complexPoint (x a)) (complexPoint (x b)) = e) ∧ + (distanceGraph x d).edgeFinset.card ≤ Fintype.card V ∧ + (distanceGraph x e).edgeFinset.card ≤ Fintype.card V := by + obtain ⟨a, b, c, d, hab, hcd, hne, hr, hs⟩ := two_rare_squared_distances x hx hn + have hdpos (p q : V) (hpq : p ≠ q) : 0 < dist (complexPoint (x p)) (complexPoint (x q)) := by + have hp := sqDist_pos (x p) (x q) (hx.ne hpq) + have hp' : (0 : ℝ) < (sqDist (x p) (x q) : ℝ) := by exact_mod_cast hp + rw [← complex_dist_sq] at hp' + nlinarith [dist_nonneg (x := complexPoint (x p)) (y := complexPoint (x q))] + refine ⟨_, _, hdpos a b hab, hdpos c d hcd, ?_, ⟨a, b, rfl⟩, ⟨c, d, rfl⟩, ?_, ?_⟩ + · intro he + apply hne + apply Rat.cast_injective (α := ℝ) + rw [← complex_dist_sq, ← complex_dist_sq, he] + · exact graph_eq_distanceGraph x a b ▸ hr + · exact graph_eq_distanceGraph x c d ▸ hs + +end +end LeanPool.RareDistanceFields.RationalPlane diff --git a/LeanPool/RareDistanceFields/SplitCounts.lean b/LeanPool/RareDistanceFields/SplitCounts.lean new file mode 100644 index 0000000000..de67889b9d --- /dev/null +++ b/LeanPool/RareDistanceFields/SplitCounts.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 LeanPool.RareDistanceFields.OrderedColors + +/-! +# Ordered pair counts under a binary partition + +See the project entry module for the exact coordinate restrictions and source roles. +Elementary finite sums used to count distance classes inside and across parity +classes; the final identity converts ordered counts to unordered graph edges. +-/ + +namespace LeanPool.RareDistanceFields.SplitCounts + +noncomputable section + +variable {V A B C : Type*} [Fintype V] [Fintype A] [Fintype B] + +open Classical in +/-- The number of pairs in a finite Cartesian product carrying the specified color. -/ +def count (q : A → B → C) (r : C) : ℕ := ∑ a, ∑ b, if q a b = r then 1 else 0 + +open Classical in +theorem count_zero (q : A → B → C) (r : C) (h : ∀ a b, q a b ≠ r) : count q r = 0 := by + simp [count, h] + +open Classical in +theorem count_congr {D : Type*} (q : A → B → C) (q' : A → B → D) (r : C) (r' : D) + (h : ∀ a b, q a b = r ↔ q' a b = r') : count q r = count q' r' := by + simp only [count, h] + +open Classical in +theorem count_symm (q : A → B → C) (r : C) : + count q r = count (fun b a => q a b) r := by + exact Finset.sum_comm + +open Classical in +theorem count_split (q : V → V → C) (r : C) (p : V → Prop) [DecidablePred p] : + count q r = + count (fun a b : {v // p v} => q a.1 b.1) r + + count (fun a : {v // p v} => fun b : {v // ¬p v} => q a.1 b.1) r + + count (fun a : {v // ¬p v} => fun b : {v // p v} => q a.1 b.1) r + + count (fun a b : {v // ¬p v} => q a.1 b.1) r := by + unfold count + rw [← Fintype.sum_subtype_add_sum_subtype p] + simp_rw [← Fintype.sum_subtype_add_sum_subtype p (fun b => if q _ b = r then 1 else 0)] + simp only [Finset.sum_add_distrib] + omega + +open Classical in +theorem card_split (p : V → Prop) [DecidablePred p] : + Fintype.card {v // p v} + Fintype.card {v // ¬p v} = Fintype.card V := by + simpa using Fintype.sum_subtype_add_sum_subtype p (fun _ => (1 : ℕ)) + +open Classical in +theorem count_eq_twice_edges (q : V → V → C) (hs : ∀ a b, q a b = q b a) + (r : C) (hdiag : ∀ a, q a a ≠ r) : + count q r = 2 * (OrderedColors.colorGraph q hs r).edgeFinset.card := by + rw [← SimpleGraph.sum_degrees_eq_twice_card_edges] + unfold count + apply Finset.sum_congr rfl + intro a ha + have he : (OrderedColors.colorGraph q hs r).neighborFinset a = + Finset.univ.filter (fun b => q a b = r) := by + ext b + rw [SimpleGraph.mem_neighborFinset] + simp only [OrderedColors.colorGraph, Finset.mem_filter, Finset.mem_univ, true_and] + constructor + · exact And.right + · intro h + refine ⟨?_, h⟩ + intro hab + exact hdiag a (hab ▸ h) + rw [← SimpleGraph.card_neighborFinset_eq_degree, he, Finset.card_filter] + +end +end LeanPool.RareDistanceFields.SplitCounts diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 563c654dd8..c6493a5a8c 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -7255,3 +7255,88 @@ projects: - "11T06" - "11T71" - "94A60" + + - slug: rare-distance-fields + title: Rare-distance bounds over specified coordinate fields + summary: >- + Proves n <= 2^r for n distinct planar points whose coordinates lie in + Q(sqrt(2)), and separately in any real purely transcendental extension + Q(T), where r counts positive occurring Euclidean distances realized by + at most n unordered pairs. Both settings give two rare distances for + n >= 3 and at least k for n >= 2^k. Exact rational specialization + preserves the complete distance-equality pattern in the Q(T) case. + The coordinate restrictions are essential; this does not solve the + unrestricted Erdos problem 132 or cover arbitrary algebraic extensions. + The proofs construct the arithmetic descent and all multiplicity + transfers. No published classification is assumed. The linked problem + is motivation; these quantitative restricted statements are proved here, + without a claim of new mathematics. + branch: discrete geometry and arithmetic + entry_module: LeanPool.RareDistanceFields + authors: + - Egor Lyfar + source: + title: Erdos problem 132 (motivation; restricted results proved in this project) + url: https://www.erdosproblems.com/132 + github_repo: lyfar/rare-distance-fields + license: Apache-2.0 + status: verified + provenance: AI + main_declarations: + - LeanPool.RareDistanceFields.bounds + main_results: + - declaration: LeanPool.RareDistanceFields.bounds + informal: >- + For every finite label type, the bound n <= 2^r holds both for + injective planar configurations with coordinates in Q(sqrt(2)) + and, separately, for configurations in a real purely + transcendental extension Q(T). In each clause r counts positive + occurring Euclidean distances with unordered multiplicity at most n. + - declaration: LeanPool.RareDistanceFields.OctagonalRational.card_le_pow_rareDistances + informal: >- + For any injective finite planar configuration with both coordinates + in Q(sqrt(2)), n <= 2^r, where r counts its positive occurring + Euclidean distances with complete unordered multiplicity at most n. + - declaration: LeanPool.RareDistanceFields.OctagonalRational.two_rare_classes + informal: >- + Every configuration of at least three distinct planar points with + both coordinates in Q(sqrt(2)) has at least two rare distances. + - declaration: LeanPool.RareDistanceFields.OctagonalRational.uniform_divergence + informal: >- + For every k there is a uniform N such that every injective finite + planar configuration with coordinates in Q(sqrt(2)) and n >= N has + at least k rare distances. The proof chooses N = 2^k. + - declaration: LeanPool.RareDistanceFields.OctagonalRational.rareDistances_spec + informal: >- + Membership in rareDistances is exactly positivity, occurrence + between two distinct configuration points, and a complete + unordered distance-graph edge count at most the number of points. + - declaration: LeanPool.RareDistanceFields.PureTranscendental.exists_rational_pattern + informal: >- + For any finite configuration with both coordinates in a real image + of the fraction field of rational multivariate polynomials, there + is a rational planar configuration preserving equality and + disequality between every pair of distance labels. + - declaration: LeanPool.RareDistanceFields.PureTranscendental.card_le_pow_rare + informal: >- + For an injective finite planar configuration over any real purely + transcendental extension Q(T), n <= 2^r, where r counts its positive + occurring Euclidean distances with unordered multiplicity at most n. + - declaration: LeanPool.RareDistanceFields.PureTranscendental.two_rare_distances + informal: >- + Every configuration of at least three distinct planar points over + a real purely transcendental extension Q(T) has two distinct + positive occurring distances of unordered multiplicity at most n. + - declaration: LeanPool.RareDistanceFields.PureTranscendental.uniform_divergence + informal: >- + For every k there is N, independent of the variable type, real + field embedding and finite configuration, such that n >= N implies + at least k rare distances. The proof chooses N = 2^k. + tags: + - discrete-geometry + - distance-multiplicity + - arithmetic-coordinates + msc: + - 52C10 + - 11R11 + - 05C35