Import explicit planar distinct-distance improvement to 43n/120

LeanPool/DistinctDistances.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2026 Adam McKenna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam McKenna
+-/
+module
+
+public import LeanPool.DistinctDistances.S4ConstantGain
+
+/-!
+# An explicit improvement to the planar distinct-distance bound in general position
+
+Source: doi:10.5281/zenodo.23680960, url:https://github.com/mysticflounder/distinct-distances-general-position
+Authors: Adam McKenna
+Status: verified
+Main declarations: `Esgk.numDistances_gt_one_third_add_kappa_image_gap`
+Tags: discrete-geometry, distinct-distances, computational-certificates, farkas-lemma
+MSC: 52C10, 51K05, 68V20
+-/
+
+/-!
+## Upstream sources and certificate data
+
+The proof is ported from Adam McKenna's Apache-2.0 release at commit
+`091530ea585b132a0c893910a9a367a00660659a` of
+<https://github.com/mysticflounder/distinct-distances-general-position>.
+The planar predicates come from `mysticflounder/lean-formalizations` at
+`dd46c17a2a034d7bfa0df02e7f77834d35592864`; that file credits their earlier
+Apache-2.0 formal-conjectures definitions. The mathematical source is the
+accompanying paper, DOI 10.5281/zenodo.23680960. Historical `docs/results/` labels
+in the upstream comments refer to working notes absent from the public release.
+
+Most source lines encode certificate data, rather than generated proof terms.
+The public release includes the raw rational certificate and a Python verifier:
+`certificate/constant-gain-1-40-K160-c60.json.gz` and
+`verifier/verify_constant_gain_1_40.py`. Its uncompressed JSON has SHA-256
+`0ce1bc6d77306573a2eccad01b75168a5faa6d6a058b91c8dcbbd0d1ce6e979a`.
+The original exporter named in the data comments is absent from that release.
+The preserved Lean strings are self-contained: the elaborators construct ordinary
+`Nat`, `Int`, `Rat` and project-owned tree terms, and `decide +kernel` checks every
+certificate. Their soundness follows from the general checker and geometric row
+lemmas. Neither the exporter nor the Python verifier enters the trusted proof.
+-/

LeanPool/DistinctDistances/AnnularTripleCollapse.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2026 Adam McKenna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam McKenna
+-/
+module
+
+public import LeanPool.DistinctDistances.ThinAnnulus
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.Ring
+
+/-!
+# Three equidistant neighbors in a thin planar annulus contain a close pair
+
+The coordinates are in an orthonormal frame with the apex `(a,0)`.
+The inputs and output are exact squared Euclidean distances. The limit proof
+in `docs/results/annulus-atomic-limit-2026-10-13.md` uses this finite lemma
+before counting perpendicular-bisector witnesses. No limit theorem is asserted
+in this module.
+-/
+
+@[expose] public section
+
+namespace Esgk
+
+/-- Two equidistant neighbors on the same transverse side of the apex axis
+are close, provided their squared radii lie in `[1-x,1]` and `a≥1/2`. -/
+lemma annular_same_side_sqDist_le {a x u v U V : ℝ}
+    (ha : 1 / 2 ≤ a) (hx : 0 ≤ x) (hx1 : x ≤ 1)
+    (hlo : 1 - x ≤ u ^ 2 + v ^ 2) (hhi : u ^ 2 + v ^ 2 ≤ 1)
+    (hLo : 1 - x ≤ U ^ 2 + V ^ 2) (hHi : U ^ 2 + V ^ 2 ≤ 1)
+    (heq : (a - u) ^ 2 + v ^ 2 = (a - U) ^ 2 + V ^ 2)
+    (hside : 0 ≤ v * V) :
+    (u - U) ^ 2 + (v - V) ^ 2 ≤ 4 * x := by
+  have hrow : 2 * a * (u - U) = (u ^ 2 + v ^ 2) - (U ^ 2 + V ^ 2) := by
+    nlinarith [heq]
+  have hcoeff : 0 ≤ 2 * a - 1 := by linarith
+  have hdu : u - U ≤ x := by
+    by_cases hd : 0 ≤ u - U
+    · nlinarith [mul_nonneg hcoeff hd]
+    · linarith
+  have hdl : -x ≤ u - U := by
+    by_cases hd : 0 ≤ U - u
+    · nlinarith [mul_nonneg hcoeff hd]
+    · linarith
+  have hdabs : |u - U| ≤ x := abs_le.mpr ⟨hdl, hdu⟩
+  have hu : |u| ≤ 1 := by
+    rw [abs_le]
+    constructor <;> nlinarith [sq_nonneg v]
+  have hU : |U| ≤ 1 := by
+    rw [abs_le]
+    constructor <;> nlinarith [sq_nonneg V]
+  have hsabs : |u + U| ≤ 2 := (abs_add_le u U).trans (by linarith)
+  have husq : |u ^ 2 - U ^ 2| ≤ 2 * x := by
+    calc
+      |u ^ 2 - U ^ 2| = |u - U| * |u + U| := by
+        rw [← abs_mul]
+        congr 1
+        ring
+      _ ≤ x * 2 := mul_le_mul hdabs hsabs (abs_nonneg _) hx
+      _ = 2 * x := by ring
+  obtain ⟨husql, husqu⟩ := abs_le.mp husq
+  have hvsq : |v ^ 2 - V ^ 2| ≤ 3 * x := by
+    rw [abs_le]
+    constructor <;> nlinarith
+  have habs : |v - V| ≤ |v + V| := by
+    have hm := sq_abs (v - V)
+    have hp := sq_abs (v + V)
+    have hn := abs_nonneg (v - V)
+    have hN := abs_nonneg (v + V)
+    nlinarith
+  have hvclose : (v - V) ^ 2 ≤ |v ^ 2 - V ^ 2| := by
+    calc
+      (v - V) ^ 2 = |v - V| * |v - V| := by rw [← pow_two, sq_abs]
+      _ ≤ |v - V| * |v + V| := mul_le_mul_of_nonneg_left habs (abs_nonneg _)
+      _ = |v ^ 2 - V ^ 2| := by
+        rw [← abs_mul]
+        congr 1
+        ring
+  have hdclose : (u - U) ^ 2 ≤ x ^ 2 := by
+    nlinarith [mul_nonneg (by linarith : 0 ≤ x - (u - U))
+      (by linarith : 0 ≤ x + (u - U))]
+  nlinarith [mul_nonneg hx (by linarith : 0 ≤ 1 - x)]
+
+/-- Among three real transverse coordinates, two lie on the same weak side
+of zero. -/
+lemma three_has_same_transverse_side (v : Fin 3 → ℝ) :
+    ∃ i j : Fin 3, i ≠ j ∧ 0 ≤ v i * v j := by
+  by_cases h0 : 0 ≤ v 0 <;> by_cases h1 : 0 ≤ v 1 <;> by_cases h2 : 0 ≤ v 2
+  · exact ⟨0, 1, by decide, mul_nonneg h0 h1⟩
+  · exact ⟨0, 1, by decide, mul_nonneg h0 h1⟩
+  · exact ⟨0, 2, by decide, mul_nonneg h0 h2⟩
+  · exact ⟨1, 2, by decide, mul_nonneg_of_nonpos_of_nonpos (by linarith) (by linarith)⟩
+  · exact ⟨1, 2, by decide, mul_nonneg h1 h2⟩
+  · exact ⟨0, 2, by decide, mul_nonneg_of_nonpos_of_nonpos (by linarith) (by linarith)⟩
+  · exact ⟨0, 1, by decide, mul_nonneg_of_nonpos_of_nonpos (by linarith) (by linarith)⟩
+  · exact ⟨0, 1, by decide, mul_nonneg_of_nonpos_of_nonpos (by linarith) (by linarith)⟩
+
+/-- In an orthonormal frame with apex `(a,0)`, three points with equal
+distance to the apex and squared radii in `[1-x,1]` contain a pair of squared
+distance at most `4*x`. In the annulus application `x≤3/4` guarantees `a≥1/2`.
+The stronger coordinate statement only needs `x≤1` once the apex bound is given. -/
+theorem annular_three_equidistant_has_close_pair (u v : Fin 3 → ℝ) {a x : ℝ}
+    (ha : 1 / 2 ≤ a) (hx : 0 ≤ x) (hx1 : x ≤ 1)
+    (hlo : ∀ i, 1 - x ≤ u i ^ 2 + v i ^ 2)
+    (hhi : ∀ i, u i ^ 2 + v i ^ 2 ≤ 1)
+    (heq : ∀ i j, (a - u i) ^ 2 + v i ^ 2 = (a - u j) ^ 2 + v j ^ 2) :
+    ∃ i j : Fin 3, i ≠ j ∧ (u i - u j) ^ 2 + (v i - v j) ^ 2 ≤ 4 * x := by
+  obtain ⟨i, j, hij, hside⟩ := three_has_same_transverse_side v
+  exact ⟨i, j, hij, annular_same_side_sqDist_le ha hx hx1
+    (hlo i) (hhi i) (hlo j) (hhi j) (heq i j) hside⟩
+
+end Esgk