Add rare-distance bounds over Q(sqrt(2)) and Q(T)

LeanPool.lean

@@ -3908,6 +3908,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

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

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

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