From 96959bfa93d5e2c5ad42388c086806660d7fa840 Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sun, 13 Sep 2026 21:23:01 +0200
Subject: [PATCH 1/3] Add geometric Ford-circle tangency bridge

---
 LeanFrontier/Geometry/FordCircleTangency.lean | 70 +++++++++++++++++++
 Submissions/ford-circle-sphere-tangency.json  | 17 +++++
 2 files changed, 87 insertions(+)
 create mode 100644 LeanFrontier/Geometry/FordCircleTangency.lean
 create mode 100644 Submissions/ford-circle-sphere-tangency.json

diff --git a/LeanFrontier/Geometry/FordCircleTangency.lean b/LeanFrontier/Geometry/FordCircleTangency.lean
new file mode 100644
index 0000000..514a2fa
--- /dev/null
+++ b/LeanFrontier/Geometry/FordCircleTangency.lean
@@ -0,0 +1,70 @@
+import LeanFrontier.NumberTheory.FordCircle
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Geometry.Euclidean.Sphere.Tangent
+import Mathlib.Tactic.Nlinarith
+
+/-!
+# Ford circles as Euclidean spheres
+
+`LeanFrontier.NumberTheory.FordCircle` proves the Ford-circle tangency criterion algebraically,
+using the squared distance between centres. This module connects that result to Mathlib's actual
+Euclidean sphere tangency predicate.
+
+A Ford circle with fraction `p / q` is represented as a sphere in the Euclidean plane `ℂ`, with
+centre `(p / q, radius q)` and radius `radius q`. For nonzero denominators, two such spheres are
+externally tangent exactly when the accepted Ford-circle cross determinant has square `1`.
+
+The proof deliberately reuses both sides of the existing interface: the exact squared-distance
+criterion from `LeanFrontier.FordCircle` and Mathlib's characterization of external sphere
+tangency by centre distance and nonnegative radii.
+-/
+
+namespace LeanFrontier.FordCircle
+
+/-- The Euclidean centre of the Ford circle of `p / q`, represented in the complex plane. -/
+def euclideanCenter (p q : ℝ) : ℂ := ⟨p / q, radius q⟩
+
+/-- The Ford circle of `p / q` as a Mathlib Euclidean sphere in the complex plane. -/
+def euclideanSphere (p q : ℝ) : EuclideanGeometry.Sphere ℂ where
+  center := euclideanCenter p q
+  radius := radius q
+
+/-- The square of the Euclidean distance between the geometric Ford-circle centres is exactly
+`centerDistSq` from the accepted algebraic Ford-circle module. -/
+theorem dist_euclideanCenter_sq (p q r s : ℝ) :
+    dist (euclideanCenter p q) (euclideanCenter r s) ^ 2 = centerDistSq p q r s := by
+  rw [Complex.dist_eq, Complex.sq_norm]
+  simp [euclideanCenter, centerDistSq, Complex.normSq_apply]
+
+private theorem radius_nonneg (q : ℝ) : 0 ≤ radius q := by
+  unfold radius
+  positivity
+
+/-- Two geometric Ford circles with nonzero denominators are externally tangent in Mathlib's
+`EuclideanGeometry.Sphere` sense exactly when their cross determinant has square `1`.
+
+This is the geometric form of the Farey-neighbour tangency criterion proved algebraically in
+`LeanFrontier.NumberTheory.FordCircle`.
+-/
+theorem isExtTangent_euclideanSphere_iff
+    {p q r s : ℝ} (hq : q ≠ 0) (hs : s ≠ 0) :
+    (euclideanSphere p q).IsExtTangent (euclideanSphere r s) ↔
+      Mediant.crossDet p q r s ^ 2 = 1 := by
+  rw [EuclideanGeometry.Sphere.isExtTangent_iff_dist_center]
+  change
+    (dist (euclideanCenter p q) (euclideanCenter r s) = radius q + radius s ∧
+      0 ≤ radius q ∧ 0 ≤ radius s) ↔ Mediant.crossDet p q r s ^ 2 = 1
+  have hqrad : 0 ≤ radius q := radius_nonneg q
+  have hsrad : 0 ≤ radius s := radius_nonneg s
+  constructor
+  · rintro ⟨hdist, -, -⟩
+    apply (centerDistSq_eq_iff hq hs).1
+    rw [← dist_euclideanCenter_sq, hdist]
+  · intro hdet
+    refine ⟨?_, hqrad, hsrad⟩
+    have hsq := (centerDistSq_eq_iff hq hs).2 hdet
+    rw [← dist_euclideanCenter_sq] at hsq
+    have hdist_nonneg : 0 ≤ dist (euclideanCenter p q) (euclideanCenter r s) := dist_nonneg
+    nlinarith
+
+end LeanFrontier.FordCircle
diff --git a/Submissions/ford-circle-sphere-tangency.json b/Submissions/ford-circle-sphere-tangency.json
new file mode 100644
index 0000000..5c8535e
--- /dev/null
+++ b/Submissions/ford-circle-sphere-tangency.json
@@ -0,0 +1,17 @@
+{
+  "protocol_version": "0.1",
+  "submission_id": "ford-circle-sphere-tangency",
+  "producer": {
+    "type": "autonomous_agent",
+    "model": "gpt-5.6-sol",
+    "agent": "chatgpt"
+  },
+  "origin_mode": "autonomous_discovery",
+  "statement_origin": "machine",
+  "proof_origin": "machine",
+  "entrypoints": [
+    "LeanFrontier.FordCircle.isExtTangent_euclideanSphere_iff"
+  ],
+  "base_mathlib_revision": "v4.33.1",
+  "source_context": "Independent extension chosen by the agent after the human operator asked for another LeanFrontier extension without naming a subject. The agent inspected the current accepted corpus and selected an explicit boundary left open by the accepted FordCircle module: that module proves the Ford-circle tangency criterion through squared centre distances and explicitly notes that a bridge to Mathlib's EuclideanGeometry.Sphere.IsExtTangent predicate is separate work. The formal statement and Lean proof in this submission were authored by GPT-5.6 Sol / ChatGPT; the human did not author or materially edit them. The new module represents Ford circles as Euclidean spheres in the complex plane and proves that, for nonzero denominators, Mathlib external tangency is equivalent to the accepted cross-determinant-square-equals-one criterion. The proof imports and depends on the accepted LeanFrontier.FordCircle API and Mathlib's sphere tangency characterization. No claim of new mathematics is made."
+}

From 274d71f20a8b9f626a0fb7ed0f29f0b1f9d9999a Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sun, 13 Sep 2026 21:24:28 +0200
Subject: [PATCH 2/3] Use available Linarith tactic import

---
 LeanFrontier/Geometry/FordCircleTangency.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanFrontier/Geometry/FordCircleTangency.lean b/LeanFrontier/Geometry/FordCircleTangency.lean
index 514a2fa..240e168 100644
--- a/LeanFrontier/Geometry/FordCircleTangency.lean
+++ b/LeanFrontier/Geometry/FordCircleTangency.lean
@@ -1,7 +1,7 @@
 import LeanFrontier.NumberTheory.FordCircle
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Geometry.Euclidean.Sphere.Tangent
-import Mathlib.Tactic.Nlinarith
+import Mathlib.Tactic.Linarith
 
 /-!
 # Ford circles as Euclidean spheres

From d46c9bbf2a7b78ba72982b6eed627cb7c55facbc Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sun, 13 Sep 2026 21:37:40 +0200
Subject: [PATCH 3/3] Fix Ford-circle geometric definitions and distance proof

---
 LeanFrontier/Geometry/FordCircleTangency.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/LeanFrontier/Geometry/FordCircleTangency.lean b/LeanFrontier/Geometry/FordCircleTangency.lean
index 240e168..e0e974c 100644
--- a/LeanFrontier/Geometry/FordCircleTangency.lean
+++ b/LeanFrontier/Geometry/FordCircleTangency.lean
@@ -22,10 +22,10 @@ tangency by centre distance and nonnegative radii.
 namespace LeanFrontier.FordCircle
 
 /-- The Euclidean centre of the Ford circle of `p / q`, represented in the complex plane. -/
-def euclideanCenter (p q : ℝ) : ℂ := ⟨p / q, radius q⟩
+noncomputable def euclideanCenter (p q : ℝ) : ℂ := ⟨p / q, radius q⟩
 
 /-- The Ford circle of `p / q` as a Mathlib Euclidean sphere in the complex plane. -/
-def euclideanSphere (p q : ℝ) : EuclideanGeometry.Sphere ℂ where
+noncomputable def euclideanSphere (p q : ℝ) : EuclideanGeometry.Sphere ℂ where
   center := euclideanCenter p q
   radius := radius q
 
@@ -35,6 +35,7 @@ theorem dist_euclideanCenter_sq (p q r s : ℝ) :
     dist (euclideanCenter p q) (euclideanCenter r s) ^ 2 = centerDistSq p q r s := by
   rw [Complex.dist_eq, Complex.sq_norm]
   simp [euclideanCenter, centerDistSq, Complex.normSq_apply]
+  ring
 
 private theorem radius_nonneg (q : ℝ) : 0 ≤ radius q := by
   unfold radius