Grace/Cumulus/Geometry/Circumcenter.g17

Open in Workbench Download source

Imports

TriangleCenters · LinearAlgebra.TwoByTwo

Declarations

Source

1-- Constructing the unique circumcenter of a noncollinear triangle.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Geometry.Circumcenter8import TriangleCenters9import LinearAlgebra.TwoByTwo1011namespace Euclidean12export open Euclidean1314-- Right-hand side of the linear perpendicular-bisector equation.15def bisectorOffset (a b : Point) : Real :=16  half(x(b) * x(b) + y(b) * y(b) - (x(a) * x(a) + y(a) * y(a)))1718theorem bisectorOffset.real (a b : Point)19  shows Real(bisectorOffset(a, b))20proof21  unfold bisectorOffset22  typecheck2324theorem bisectorOffset.double (a b : Point)25  shows bisectorOffset(a, b) + bisectorOffset(a, b) =26    x(b) * x(b) + y(b) * y(b) - (x(a) * x(a) + y(a) * y(a))27proof28  have doubled := half.add_self at x(b) * x(b) + y(b) * y(b) - (x(a) * x(a) + y(a) * y(a)) with *29  simp [bisectorOffset]3031-- Squared-distance equality is exactly one linear equation in the center.32theorem circumcenter.bisector_equation (a b o : Point)33  shows Euclidean.distanceSquared(o, a) = Euclidean.distanceSquared(o, b) ↔34    (x(b) - x(a)) * x(o) + (y(b) - y(a)) * y(o) = bisectorOffset(a, b)35proof36  have offsetReal := bisectorOffset.real at a, b with *37  have doubled := bisectorOffset.double at a, b with *38  have firstRadius := Euclidean.distanceSquared.coordinates at o, a with *39  have secondRadius := Euclidean.distanceSquared.coordinates at o, b with *40  constructor41  . intro radii42    rw [firstRadius, secondRadius] at radii43    apply realAddValue.double_cancel with offsetReal44    linear_combination radii - doubled45  . intro equation46    rw [firstRadius, secondRadius]47    linear_combination equation + equation + doubled4849-- Cramer's rule is total; correctness and uniqueness require noncollinearity.50def circumcenter (a b c : Set) : Set :=51  (LinearSystem2.solutionX(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c)),52   LinearSystem2.solutionY(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c)))5354theorem circumcenter.point (a b c : Point)55  shows Point(circumcenter(a, b, c))56proof57  unfold circumcenter58  exact pair.point with *5960theorem circumcenter.coordinates (a b c : Point)61  shows x(circumcenter(a, b, c)) = LinearSystem2.solutionX(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c)) ∧62    y(circumcenter(a, b, c)) = LinearSystem2.solutionY(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c))63proof64  have horizontalProjection := x.pair at LinearSystem2.solutionX(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c)), LinearSystem2.solutionY(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c)) with *65  have verticalProjection := y.pair at LinearSystem2.solutionX(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c)), LinearSystem2.solutionY(x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c)) with *66  constructor67  . simp [circumcenter]68  . simp [circumcenter]6970theorem circumcenter.correct (a b c : Point)71  requires noncollinear : ¬Collinear(a, b, c)72  shows Circumcenter(circumcenter(a, b, c), a, b, c)73proof74  have nonsingular : (x(b) - x(a)) * (y(c) - y(a)) - (y(b) - y(a)) * (x(c) - x(a)) ≠ 075    intro zero76    apply noncollinear77    simp [Collinear, directionCross]78  have equations := LinearSystem2.correct at x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c) with *79  have point := circumcenter.point at a, b, c with *80  have coordinates := circumcenter.coordinates at a, b, c with *81  rcases coordinates with ⟨horizontal, vertical⟩82  rcases equations with ⟨first, second⟩83  rw [← horizontal, ← vertical] at first84  rw [← horizontal, ← vertical] at second85  have firstRadii := circumcenter.bisector_equation.backward at a, b, circumcenter(a, b, c) with *86  have secondRadii := circumcenter.bisector_equation.backward at a, c, circumcenter(a, b, c) with *87  unfold Circumcenter88  refine ⟨firstRadii, secondRadii⟩8990theorem circumcenter.unique (a b c o p : Point)91  requires noncollinear : ¬Collinear(a, b, c)92  requires firstCenter : Circumcenter(o, a, b, c)93  requires secondCenter : Circumcenter(p, a, b, c)94  shows o = p95proof96  have nonsingular : (x(b) - x(a)) * (y(c) - y(a)) - (y(b) - y(a)) * (x(c) - x(a)) ≠ 097    intro zero98    apply noncollinear99    simp [Collinear, directionCross]100  rcases firstCenter with ⟨firstRadii, secondRadii⟩101  rcases secondCenter with ⟨otherFirstRadii, otherSecondRadii⟩102  have first := circumcenter.bisector_equation.forward at a, b, o with *103  have second := circumcenter.bisector_equation.forward at a, c, o with *104  have otherFirst := circumcenter.bisector_equation.forward at a, b, p with *105  have otherSecond := circumcenter.bisector_equation.forward at a, c, p with *106  have equalCoordinates := LinearSystem2.unique at x(b) - x(a), y(b) - y(a), x(c) - x(a), y(c) - y(a), bisectorOffset(a, b), bisectorOffset(a, c), x(o), y(o), x(p), y(p) with *107  rcases equalCoordinates with ⟨horizontal, vertical⟩108  exact point.ext with *109110theorem circumcenter.exists (a b c : Point)111  requires noncollinear : ¬Collinear(a, b, c)112  shows ∃ o, Point(o) ∧ Circumcenter(o, a, b, c)113proof114  have point := circumcenter.point at a, b, c with *115  have circle := circumcenter.correct with *116  refine ⟨circumcenter(a, b, c), point, circle⟩117118-- No center is supplied by the caller: all three are constructed foundationally.119theorem euler_line.exists (a b c : Point)120  requires noncollinear : ¬Collinear(a, b, c)121  shows ∃ o, ∃ g, ∃ h, Point(o) ∧ Point(g) ∧ Point(h) ∧122    Circumcenter(o, a, b, c) ∧ Centroid(g, a, b, c) ∧ Orthocenter(h, a, b, c) ∧123    Collinear(h, g, o) ∧ MedianRatio(h, g, o)124proof125  have oPoint := circumcenter.point at a, b, c with *126  have circle := circumcenter.correct with *127  have gPoint := centroid.point at a, b, c with *128  have center := centroid.correct at a, b, c with *129  have line := euler_line at circumcenter(a, b, c), a, b, c, centroid(a, b, c) with *130  rcases line with ⟨h, hPoint, altitudes, collinear, ratio⟩131  refine ⟨circumcenter(a, b, c), centroid(a, b, c), h, oPoint, gPoint, hPoint, circle, center, altitudes, collinear, ratio⟩132133-- Every noncollinear triangle has a center, constructed from its circumcenter.134theorem orthocenter.exists (a b c : Point)135  requires noncollinear : ¬Collinear(a, b, c)136  shows ∃ h, Point(h) ∧ Orthocenter(h, a, b, c)137proof138  have oPoint := circumcenter.point at a, b, c with *139  have circle := circumcenter.correct with *140  have hPoint := orthocenter.point at circumcenter(a, b, c), a, b, c with *141  have altitudes := orthocenter.correct with *142  refine ⟨orthocenter(circumcenter(a, b, c), a, b, c), hPoint, altitudes⟩143144-- An intersection of two altitudes lies on the third as well.145theorem orthocenter.of_two_altitudes (a b c h : Point)146  requires noncollinear : ¬Collinear(a, b, c)147  requires firstAltitude : PerpendicularDirections(a, h, b, c)148  requires secondAltitude : PerpendicularDirections(b, h, c, a)149  shows Orthocenter(h, a, b, c)150proof151  have center := orthocenter.exists with *152  rcases center with ⟨k, kPoint, altitudes⟩153  obtain ⟨otherFirstAltitude, otherSecondAltitude, otherThirdAltitude⟩ := altitudes154  have same := altitudes.unique at a, b, c, h, k with *155  rwa same156157-- The explicit construction agrees with every geometric orthocenter.158theorem orthocenter.eq_constructed (a b c h : Point)159  requires noncollinear : ¬Collinear(a, b, c)160  requires center : Orthocenter(h, a, b, c)161  shows h = orthocenter(circumcenter(a, b, c), a, b, c)162proof163  have oPoint := circumcenter.point at a, b, c with *164  have circle := circumcenter.correct with *165  have hPoint := orthocenter.point at circumcenter(a, b, c), a, b, c with *166  have altitudes := orthocenter.correct with *167  exact orthocenter.unique with *168169end Euclidean170