feat(Geometry): bridge Ford circles to Euclidean sphere tangency

[qazW12345]

One ordinary extension submission: Submissions/ford-circle-sphere-tangency.json plus one new subject module, LeanFrontier/Geometry/FordCircleTangency.lean.

Subject

This extends the accepted LeanFrontier.NumberTheory.FordCircle development at an explicit boundary left open by that module: connecting its algebraic squared-distance tangency criterion to Mathlib's actual EuclideanGeometry.Sphere.IsExtTangent predicate.

The candidate represents the Ford circle of p / q as a Euclidean sphere in ℂ, centred at (p / q, radius q) with radius radius q, and proves for nonzero denominators that Mathlib external tangency is equivalent to the accepted cross-determinant-square criterion.

Entrypoint

LeanFrontier.FordCircle.isExtTangent_euclideanSphere_iff

Composition with the accepted corpus

The proof reuses:

• LeanFrontier.FordCircle.centerDistSq_eq_iff from the accepted Ford-circle submission;
• the accepted FordCircle.radius / centerDistSq definitions;
• Mathlib's EuclideanGeometry.Sphere.isExtTangent_iff_dist_center characterization.

A small bridge theorem identifies the squared Euclidean distance in ℂ with the accepted centerDistSq expression.

Adversarial boundary review

Before opening this PR, the exact candidate was deliberately pressure-tested at the statement/proof boundary:

• q = 0 or s = 0 is intentionally excluded because the accepted centerDistSq_eq_iff requires nonzero denominators and Lean field division at zero would otherwise describe degenerate objects rather than the intended Ford-circle criterion.
• Negative nonzero denominators do not create a sign bug: the radius is 1 / (2*q^2), so it remains nonnegative, and the theorem is a valid real-field generalization of the accepted algebraic statement.
• In the reverse implication, equality of squared centre distance and squared radius sum is converted back to an unsquared equality only after establishing nonnegativity of the Euclidean distance and both radii; there is no hidden a^2 = b^2 -> a = b sign assumption.
• The public theorem is not a restatement or alias of an existing corpus result: the accepted FordCircle source explicitly says the IsExtTangent bridge is separate work, and corpus search found no existing such theorem.
• The receiver's exact-statement search found zero Mathlib exact matches, and kernel recheck passed.

Provenance

The human operator asked the agent for another independent LeanFrontier extension without naming a subject. The agent inspected the accepted corpus, selected this Ford-circle/Mathlib geometry bridge, and authored the formal Lean statement and proof. The human did not author or materially edit either. Accordingly the claim uses origin_mode: autonomous_discovery, statement_origin: machine, and proof_origin: machine; that history is recorded in source_context.

Exact-head validation evidence

Base: main @ 9f708c18fccb311646b10af124c60ca70e41857b

Candidate: d46c9bbf2a7b78ba72982b6eed627cb7c55facbc

OCI diagnostic harness on the exact candidate:

• diagnostic lake build: success
• restricted formal validation: success

Fork canonical CI on the same exact head:

• test: success (run 34778277093)
• validate-submission: success (run 34778277095)
• trusted preflight: accepted, no diagnostics
• restricted formal validation: accepted, no diagnostics
• build: pass
• kernel recheck: pass
• downstream import smoke: pass
• Mathlib exact matches: 0
• receiver observed exactly the two ordinary submission files

The fork-local PR is only a development harness and will remain unmerged.

[qazW12345]

I'd like to ask about the contribution etiquette, namely, if there is a limit for simultanously open PRs or anything else that would affect the cadence of work the AI agent is doing - should i let the agent contribute freely or constrain it in some way?