[Merged by Bors] - feat(Geometry/Euclidean): nine-point circle

[wwylele]

---

I saw there is a reference to 3(n+1) Point Sphere in MongePoint.lean but no implementation for it, so I decided to fill the gap.

[github-actions]

PR summary 725d7a32b7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Euclidean.NinePointCircle (new file)	2230

---

Declarations diff

+ affineSpan_range_medial
+ altitudeFoot_mem_ninePointCircle
+ eulerPoint
+ eulerPoint_eq_midpoint
+ eulerPoint_map
+ eulerPoint_mem_ninePointCircle
+ eulerPoint_reindex
+ eulerPoint_restrict
+ faceOppositeCentroid_mem_ninePointCircle
+ isDiameter_ninePointCircle
+ medial
+ medial_map
+ medial_points
+ medial_reindex
+ medial_restrict
+ midpoint_faceOppositeCentroid_eulerPoint
+ mongePoint_map
+ mongePoint_restrict
+ ninePointCircle
+ ninePointCircle_center
+ ninePointCircle_center_mem_affineSpan
+ ninePointCircle_eq_circumsphere_medial
+ ninePointCircle_map
+ ninePointCircle_radius
+ ninePointCircle_reindex
+ ninePointCircle_restrict
+ orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle
+ points_vsub_eulerPoint

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Copilot]

Pull request overview

This PR implements the nine-point circle for triangles and its higher-dimensional analogue, the 3(n+1)-point sphere for simplices in Euclidean geometry. The implementation follows the reference paper by Małgorzata Buba-Brzozowa and is mentioned in MongePoint.lean but was not previously implemented.

Changes:

• Adds the ninePointCircle definition for a simplex, defining the center and radius based on the Euler line construction
• Defines eulerPoint as points that the nine-point circle passes through
• Proves that the nine-point circle passes through face centroids, Euler points, and (for triangles) altitude feet

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[jsm28]

I think we should have a definition of Affine.Simplex.medial, the simplex whose vertices are given by faceOppositeCentroid, probably in Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid and for any affine space over a division ring with characteristic zero. Then you can include the statement here that s.medial.circumsphere = s.ninePointCircle.

[jsm28]

A much more ambitious goal, that definitely wouldn't be for this PR but would be nice to have in mathlib eventually, would be to prove Feuerbach's theorem, which is one of the missing entries on the 100-theorems list. Feuerbach is genuinely specific to triangles (it's not true in general for simplices in higher dimensions), and could be stated as t.insphere.IsIntTangent t.ninePointCircle together with (for i : Fin 3) (t.exsphere {i}).IsExtTangent t.ninePointCircle (which is a lot nicer than the statements in other ITPs you can find on Freek's list). Note however that we have very little API at present for IsIntTangent or IsExtTangent - tangencies between spheres / circles - and probably more would need to be added.

[Copilot]

Pull request overview

Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[jsm28]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by jsm28.

[vihdzp]

Mostly just small orthographic fixes.

[ocfnash]

Really this condition should be:

    (hS : Set.range s.points ⊆ S) :

but I see that this pattern goes all the way back to Affine.Simplex.restrict so the issue is orthogonal to the content of this PR.

However I do think we should explore changing Affine.Simplex.restrict to:

def restrict {n : ℕ} (s : Affine.Simplex k P n) (S : AffineSubspace k P)
    (hS : Set.range s.points ⊆ S) :
    have : Nonempty S := .map (fun i ↦ ⟨s.points i, hS <| Set.mem_range_self i⟩) inferInstance
    Affine.Simplex (V := S.direction) k S n :=
  have : Nonempty S := .map (fun i ↦ ⟨s.points i, hS <| Set.mem_range_self i⟩) inferInstance
  { points i := ⟨s.points i, hS <| Set.mem_range_self i⟩
    independent := AffineIndependent.of_comp S.subtype s.independent }

and propagating this change.

[jsm28]

We discussed what the hypothesis should look like in #25172 which originally added Affine.Simplex.restrict, and the likely value of being able to use le_rfl in a common use case. The main awkward thing with the current design is it generally seems to be necessary to give a Nonempty hypothesis explicitly at sites of use.

[ocfnash]

Thanks, I remember that conversation now. I think the case for Eric's suggestion is stronger now that we see there is a growing cost to the complexity of downstream lemma statements.

[jsm28]

I'd rather revisit the idea of removing Nonempty from AddTorsor (thus enabling even empty affine subspaces to have an AddTorsor instance and hopefully removing the need to construct a Nonempty instance here at all) and instead putting Nonempty hypotheses on just those lemmas about torsors that really need the mathematical notion of a torsor rather than what we might call a pretorsor.

[ocfnash]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step