Grace/Cumulus/Geometry/TriangleCenters.g17

Open in Workbench Download source

Imports

Centroid · LinearAlgebra.TwoByTwo

Declarations

Source

1-- Circumcenters, orthocenters, and Euler's line.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.TriangleCenters8import Centroid9import LinearAlgebra.TwoByTwo1011namespace Euclidean12export open Euclidean1314predicate Circumcenter (o a b c : Set) :=15  Euclidean.distanceSquared(o, a) = Euclidean.distanceSquared(o, b) ∧16  Euclidean.distanceSquared(o, a) = Euclidean.distanceSquared(o, c)1718-- Reuse the checked midpoint-of-hypotenuse construction for right triangles.19theorem circumcenter.right_triangle (a b c m : Point)20  requires middle : Midpoint(m, a, b)21  requires right : RightAngle(a, c, b)22  shows Circumcenter(m, a, b, c)23proof24  have radii := right_triangle_circumcenter at a, b, c, m with *25  rcases radii with ⟨first, second⟩26  constructor27  . cc28  . cc2930-- Each vertex-to-center direction is perpendicular to its opposite side.31-- Zero directions are allowed; no distinct-line or uniqueness claim is implicit.32predicate Orthocenter (h a b c : Set) :=33  PerpendicularDirections(a, h, b, c) ∧34  PerpendicularDirections(b, h, c, a) ∧35  PerpendicularDirections(c, h, a, b)3637-- Given a circumcenter O, construct H = A + B + C - 2O.38def orthocenter (o a b c : Set) : Set :=39  (x(a) + x(b) + x(c) - (x(o) + x(o)),40   y(a) + y(b) + y(c) - (y(o) + y(o)))4142theorem orthocenter.point (o a b c : Point)43  shows Point(orthocenter(o, a, b, c))44proof45  unfold orthocenter46  exact pair.point with *4748theorem orthocenter.coordinates (o a b c : Point)49  shows x(orthocenter(o, a, b, c)) = x(a) + x(b) + x(c) - (x(o) + x(o)) ∧50    y(orthocenter(o, a, b, c)) = y(a) + y(b) + y(c) - (y(o) + y(o))51proof52  have horizontal := x.pair at x(a) + x(b) + x(c) - (x(o) + x(o)), y(a) + y(b) + y(c) - (y(o) + y(o)) with *53  have vertical := y.pair at x(a) + x(b) + x(c) - (x(o) + x(o)), y(a) + y(b) + y(c) - (y(o) + y(o)) with *54  constructor55  . unfold orthocenter56    exact horizontal57  . unfold orthocenter58    exact vertical5960theorem orthocenter.rotate (o a b c : Point)61  shows orthocenter(o, a, b, c) = orthocenter(o, b, c, a)62proof63  have firstPoint := orthocenter.point at o, a, b, c with *64  have secondPoint := orthocenter.point at o, b, c, a with *65  have first := orthocenter.coordinates at o, a, b, c with *66  have second := orthocenter.coordinates at o, b, c, a with *67  rcases first with ⟨firstX, firstY⟩68  rcases second with ⟨secondX, secondY⟩69  have horizontal : x(orthocenter(o, a, b, c)) = x(orthocenter(o, b, c, a)) by linear_combination firstX - secondX70  have vertical : y(orthocenter(o, a, b, c)) = y(orthocenter(o, b, c, a)) by linear_combination firstY - secondY71  exact point.ext with *7273-- Equal radii to B and C make AH perpendicular to BC.74theorem orthocenter.altitude (o a b c : Point)75  requires equalRadii : Euclidean.distanceSquared(o, b) = Euclidean.distanceSquared(o, c)76  shows PerpendicularDirections(a, orthocenter(o, a, b, c), b, c)77proof78  have point := orthocenter.point at o, a, b, c with *79  have product := vector.dot_coordinates at a, orthocenter(o, a, b, c), b, c with *80  have firstRadius := Euclidean.distanceSquared.coordinates at o, b with *81  have secondRadius := Euclidean.distanceSquared.coordinates at o, c with *82  rw [firstRadius, secondRadius] at equalRadii83  unfold PerpendicularDirections84  rw product85  have coordinates := orthocenter.coordinates at o, a, b, c with *86  rcases coordinates with ⟨horizontal, vertical⟩87  linear_combination (x(c) - x(b)) * horizontal + (y(c) - y(b)) * vertical - equalRadii8889-- The three altitude statements follow by cyclic permutation.90theorem orthocenter.correct (o a b c : Point)91  requires circle : Circumcenter(o, a, b, c)92  shows Orthocenter(orthocenter(o, a, b, c), a, b, c)93proof94  rcases circle with ⟨firstRadii, secondRadii⟩95  have oppositeRadii : Euclidean.distanceSquared(o, b) = Euclidean.distanceSquared(o, c) by cc96  have reversedRadii : Euclidean.distanceSquared(o, c) = Euclidean.distanceSquared(o, a)97    symm98    exact secondRadii99  have first := orthocenter.altitude at o, a, b, c with *100  have second := orthocenter.altitude at o, b, c, a with *101  have third := orthocenter.altitude at o, c, a, b with *102  have rotate := orthocenter.rotate at o, a, b, c with *103  have again := orthocenter.rotate at o, b, c, a with *104  rw [← again, ← rotate] at third105  rw ← rotate at second106  unfold Orthocenter107  refine ⟨first, second, third⟩108109-- G lies two thirds of the way from H to O, so HG = 2 GO as directed vectors.110theorem orthocenter.centroid_ratio (o a b c g : Point)111  requires center : Centroid(g, a, b, c)112  shows MedianRatio(orthocenter(o, a, b, c), g, o)113proof114  have point := orthocenter.point at o, a, b, c with *115  unfold MedianRatio116  have coordinates := orthocenter.coordinates at o, a, b, c with *117  rcases coordinates with ⟨horizontal, vertical⟩118  rcases center with ⟨centerX, centerY⟩119  constructor120  . linear_combination centerX - horizontal121  . linear_combination centerY - vertical122123-- Euler's line, formulated to include coincident centers without claiming124-- that such points determine a unique line.125theorem euler_line (o a b c g : Point)126  requires circle : Circumcenter(o, a, b, c)127  requires center : Centroid(g, a, b, c)128  shows ∃ h, Point(h) ∧ Orthocenter(h, a, b, c) ∧129    Collinear(h, g, o) ∧ MedianRatio(h, g, o)130proof131  have point := orthocenter.point at o, a, b, c with *132  have altitudes := orthocenter.correct with *133  have ratio := orthocenter.centroid_ratio at o, a, b, c, g with *134  have line := medianRatio.collinear with *135  refine ⟨orthocenter(o, a, b, c), point, altitudes, line, ratio⟩136137-- The affine construction collapses to G when O = G.138theorem orthocenter.at_centroid (o a b c : Point)139  requires center : Centroid(o, a, b, c)140  shows orthocenter(o, a, b, c) = o141proof142  have point := orthocenter.point at o, a, b, c with *143  have coordinates := orthocenter.coordinates at o, a, b, c with *144  rcases coordinates with ⟨horizontal, vertical⟩145  rcases center with ⟨centerX, centerY⟩146  have sameX : x(orthocenter(o, a, b, c)) = x(o) by linear_combination horizontal - centerX147  have sameY : y(orthocenter(o, a, b, c)) = y(o) by linear_combination vertical - centerY148  exact point.ext with *149150theorem euler_line.coincident (o a b c : Point)151  requires circle : Circumcenter(o, a, b, c)152  requires center : Centroid(o, a, b, c)153  shows Orthocenter(o, a, b, c)154proof155  have altitudes := orthocenter.correct with *156  have same := orthocenter.at_centroid with *157  rwa same at altitudes158159-- An altitude condition is a linear equation in the candidate center.160theorem altitude.equation (a h b c : Point)161  requires perpendicular : PerpendicularDirections(a, h, b, c)162  shows (x(c) - x(b)) * x(h) + (y(c) - y(b)) * y(h) =163    (x(c) - x(b)) * x(a) + (y(c) - y(b)) * y(a)164proof165  have product := vector.dot_coordinates at a, h, b, c with *166  unfold PerpendicularDirections at perpendicular167  rw product at perpendicular168  linear_combination perpendicular169170-- Two altitudes already determine the center of a noncollinear triangle.171theorem altitudes.unique (a b c h k : Point)172  requires noncollinear : ¬Collinear(a, b, c)173  requires firstAltitude : PerpendicularDirections(a, h, b, c)174  requires secondAltitude : PerpendicularDirections(b, h, c, a)175  requires otherFirstAltitude : PerpendicularDirections(a, k, b, c)176  requires otherSecondAltitude : PerpendicularDirections(b, k, c, a)177  shows h = k178proof179  have nonsingular : (x(c) - x(b)) * (y(a) - y(c)) - (y(c) - y(b)) * (x(a) - x(c)) ≠ 0180    intro zero181    apply noncollinear182    unfold Collinear183    unfold directionCross184    linear_combination zero185  have first := altitude.equation at a, h, b, c with *186  have second := altitude.equation at b, h, c, a with *187  have otherFirst := altitude.equation at a, k, b, c with *188  have otherSecond := altitude.equation at b, k, c, a with *189  have coordinates := LinearSystem2.unique at x(c) - x(b), y(c) - y(b), x(a) - x(c), y(a) - y(c),190    (x(c) - x(b)) * x(a) + (y(c) - y(b)) * y(a),191    (x(a) - x(c)) * x(b) + (y(a) - y(c)) * y(b), x(h), y(h), x(k), y(k) with *192  rcases coordinates with ⟨horizontal, vertical⟩193  exact point.ext with *194195theorem orthocenter.unique (a b c h k : Point)196  requires noncollinear : ¬Collinear(a, b, c)197  requires firstCenter : Orthocenter(h, a, b, c)198  requires secondCenter : Orthocenter(k, a, b, c)199  shows h = k200proof201  rcases firstCenter with ⟨firstAltitude, secondAltitude, thirdAltitude⟩202  rcases secondCenter with ⟨otherFirstAltitude, otherSecondAltitude, otherThirdAltitude⟩203  exact altitudes.unique with *204205end Euclidean206