GeometryStarter

Geometry with named points and reusable geometric facts

Open in Workbench View on GitHub

1-- Geometry with named points and reusable geometric facts.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 GeometryStarter8import Grace.Cumulus.Geometry910-- Equal legs give equal base angles: compare the triangle with its reversal.11theorem equal_base_angles (a b c : Euclidean.Point)12  requires base : a ≠ b13  requires leg : a ≠ c14  requires equalLegs : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(b, c)15  shows Euclidean.EqualAngle(c, a, b, c, b, a)16proof17  exact Euclidean.isosceles at a, b, c with *1819-- A diameter subtends a right angle, and its two rays really are nonzero.20theorem angle_in_semicircle (a b p center : Euclidean.Point)21  requires diameter : Euclidean.Midpoint(center, a, b)22  requires onCircle : Euclidean.OnCircle(p, center, a)23  requires firstRay : a ≠ p24  requires secondRay : p ≠ b25  shows Euclidean.RightAngle(a, p, b) ∧26    0 < Euclidean.distanceSquared(a, p) ∧ 0 < Euclidean.distanceSquared(p, b)27proof28  exact Euclidean.thales at a, b, p, center with *2930-- The familiar distance equation characterizes a right angle.31theorem right_angle_from_sides (a b c : Euclidean.Point)32  requires sides : Euclidean.distanceSquared(a, c) =33    Euclidean.distanceSquared(a, b) + Euclidean.distanceSquared(b, c)34  shows Euclidean.RightAngle(a, b, c)35proof36  exact Euclidean.pythagoras_converse at a, b, c with *3738-- The isosceles median is an altitude: a one-step geometric application.39theorem median_is_altitude (a b c m : Euclidean.Point)40  requires middle : Euclidean.Midpoint(m, a, b)41  requires legs : Euclidean.distanceSquared(c, a) = Euclidean.distanceSquared(c, b)42  shows Euclidean.RightAngle(c, m, a)43proof44  exact Euclidean.isosceles_median_perpendicular at a, b, c, m with *4546-- Join the midpoints of two sides: the resulting segment is parallel47-- to the third side. A nonzero base guarantees a nonzero midsegment.48theorem triangle_midsegment (a b c m n : Euclidean.Point)49  requires first : Euclidean.Midpoint(m, c, a)50  requires second : Euclidean.Midpoint(n, c, b)51  requires base : a ≠ b52  shows Euclidean.ParallelSegments(m, n, a, b)53proof54  exact Euclidean.midsegment.parallel at a, b, c, m, n with *5556-- Every pair of points has a midpoint, and every such midpoint lies on57-- their supporting line. The point is constructed using halves.58theorem constructed_midpoint (a b : Euclidean.Point)59  shows Euclidean.Point(Euclidean.midpoint(a, b)) ∧60    Euclidean.Midpoint(Euclidean.midpoint(a, b), a, b) ∧61    Euclidean.Collinear(a, Euclidean.midpoint(a, b), b)62proof63  have point := Euclidean.midpoint.point at a, b with *64  have middle := Euclidean.midpoint.correct at a, b with *65  have onLine := Euclidean.midpoint.collinear at a, b, Euclidean.midpoint(a, b) with *66  refine ⟨point, middle, onLine⟩6768-- Varignon: the four side midpoints of any quadrilateral form an affine69-- parallelogram. This includes concave, crossed, and degenerate inputs.70theorem midpoint_quadrilateral (a b c d : Euclidean.Point)71  shows Euclidean.Parallelogram(Euclidean.midpoint(a, b), Euclidean.midpoint(b, c),72    Euclidean.midpoint(c, d), Euclidean.midpoint(d, a))73proof74  exact Euclidean.varignon.constructed at a, b, c, d with *7576-- A synthetic consequence: the diagonals of the midpoint figure bisect77-- one another. The proof uses only Varignon and the parallelogram API.78theorem midpoint_figure_diagonals (a b c d m n p q : Euclidean.Point)79  requires first : Euclidean.Midpoint(m, a, b)80  requires second : Euclidean.Midpoint(n, b, c)81  requires third : Euclidean.Midpoint(p, c, d)82  requires fourth : Euclidean.Midpoint(q, d, a)83  shows ∃ center, Euclidean.Point(center) ∧84    Euclidean.Midpoint(center, m, p) ∧ Euclidean.Midpoint(center, n, q)85proof86  have shape := Euclidean.varignon at a, b, c, d, m, n, p, q with *87  exact Euclidean.parallelogram.diagonals at m, n, p, q with *8889-- Zero-length sides satisfy the affine identity, but they are not nonzero90-- parallel segments. The distinction is explicit in the public predicates.91theorem collapsed_figure (a : Euclidean.Point)92  shows Euclidean.Parallelogram(a, a, a, a) ∧ ¬Euclidean.ParallelSegments(a, a, a, a)93proof94  constructor95  . unfold Euclidean.Parallelogram96    rfl97  . intro parallel98    rcases parallel with ⟨distinct, rest⟩99    have same : a = a by rfl100    exact distinct with same101102-- The medians meet at the constructed centroid, with no coordinate calculation103-- in this application. Each median carries the same directed 2:1 relation.104theorem triangle_medians (a b c m n p : Euclidean.Point)105  requires first : Euclidean.Midpoint(m, b, c)106  requires second : Euclidean.Midpoint(n, c, a)107  requires third : Euclidean.Midpoint(p, a, b)108  shows ∃ g, Euclidean.Point(g) ∧ Euclidean.Centroid(g, a, b, c) ∧109    Euclidean.Collinear(a, g, m) ∧ Euclidean.Collinear(b, g, n) ∧ Euclidean.Collinear(c, g, p)110proof111  exact Euclidean.centroid.concurrency at a, b, c, m, n, p with *112113theorem median_squared_lengths (a b c g m : Euclidean.Point)114  requires center : Euclidean.Centroid(g, a, b, c)115  requires middle : Euclidean.Midpoint(m, b, c)116  shows Euclidean.distanceSquared(a, g) =117    Euclidean.distanceSquared(g, m) + Euclidean.distanceSquared(g, m) +118    Euclidean.distanceSquared(g, m) + Euclidean.distanceSquared(g, m)119proof120  have ratio := Euclidean.centroid.median_ratio at a, b, c, g, m with *121  exact Euclidean.medianRatio.length at a, g, m with *122123theorem collapsed_triangle (a : Euclidean.Point)124  shows Euclidean.centroid(a, a, a) = a125proof126  exact Euclidean.centroid.repeated at a with *127128-- Given the circumcenter and centroid, construct an orthocenter on Euler's line.129theorem triangle_centers (o a b c g : Euclidean.Point)130  requires circle : Euclidean.Circumcenter(o, a, b, c)131  requires center : Euclidean.Centroid(g, a, b, c)132  shows ∃ h, Euclidean.Point(h) ∧ Euclidean.Orthocenter(h, a, b, c) ∧133    Euclidean.Collinear(h, g, o) ∧ Euclidean.MedianRatio(h, g, o)134proof135  exact Euclidean.euler_line at o, a, b, c, g with *136137-- The same 2:1 lemma used for medians gives HG² = 4 GO².138theorem center_squared_distances (o a b c g : Euclidean.Point)139  requires circle : Euclidean.Circumcenter(o, a, b, c)140  requires center : Euclidean.Centroid(g, a, b, c)141  shows Euclidean.distanceSquared(Euclidean.orthocenter(o, a, b, c), g) =142    Euclidean.distanceSquared(g, o) + Euclidean.distanceSquared(g, o) +143    Euclidean.distanceSquared(g, o) + Euclidean.distanceSquared(g, o)144proof145  have point := Euclidean.orthocenter.point at o, a, b, c with *146  have ratio := Euclidean.orthocenter.centroid_ratio at o, a, b, c, g with *147  exact Euclidean.medianRatio.length at Euclidean.orthocenter(o, a, b, c), g, o with *148149theorem coincident_centers (o a b c : Euclidean.Point)150  requires circle : Euclidean.Circumcenter(o, a, b, c)151  requires center : Euclidean.Centroid(o, a, b, c)152  shows Euclidean.Orthocenter(o, a, b, c)153proof154  exact Euclidean.euler_line.coincident at o, a, b, c with *155156-- A collapsed triangle has coincident centers too, without a unique Euler line.157theorem collapsed_centers (a : Euclidean.Point)158  shows Euclidean.Circumcenter(a, a, a, a) ∧ Euclidean.Orthocenter(a, a, a, a)159proof160  have circle : Euclidean.Circumcenter(a, a, a, a)161    unfold Euclidean.Circumcenter162    constructor163    . rfl164    . rfl165  have center : Euclidean.Centroid(a, a, a, a)166    unfold Euclidean.Centroid167    constructor168    . rfl169    . rfl170  have altitudes := Euclidean.euler_line.coincident at a, a, a, a with *171  refine ⟨circle, altitudes⟩172173-- For a right triangle, the known hypotenuse midpoint supplies the circumcenter.174theorem right_triangle_euler_line (a b c m g : Euclidean.Point)175  requires middle : Euclidean.Midpoint(m, a, b)176  requires right : Euclidean.RightAngle(a, c, b)177  requires center : Euclidean.Centroid(g, a, b, c)178  shows ∃ h, Euclidean.Point(h) ∧ Euclidean.Orthocenter(h, a, b, c) ∧179    Euclidean.Collinear(h, g, m) ∧ Euclidean.MedianRatio(h, g, m)180proof181  have circle := Euclidean.circumcenter.right_triangle at a, b, c, m with *182  exact Euclidean.euler_line at m, a, b, c, g with *183184-- Every noncollinear triangle supplies its own centers: no center hypotheses.185theorem all_triangle_centers (a b c : Euclidean.Point)186  requires noncollinear : ¬Euclidean.Collinear(a, b, c)187  shows ∃ o, ∃ g, ∃ h, Euclidean.Point(o) ∧ Euclidean.Point(g) ∧ Euclidean.Point(h) ∧188    Euclidean.Circumcenter(o, a, b, c) ∧ Euclidean.Centroid(g, a, b, c) ∧ Euclidean.Orthocenter(h, a, b, c) ∧189    Euclidean.Collinear(h, g, o) ∧ Euclidean.MedianRatio(h, g, o)190proof191  exact Euclidean.euler_line.exists at a, b, c with *192193theorem circumcenter_is_unique (a b c o p : Euclidean.Point)194  requires noncollinear : ¬Euclidean.Collinear(a, b, c)195  requires first : Euclidean.Circumcenter(o, a, b, c)196  requires second : Euclidean.Circumcenter(p, a, b, c)197  shows o = p198proof199  exact Euclidean.circumcenter.unique at a, b, c, o, p with *200201-- Any two altitudes determine the unique orthocenter; the third follows.202theorem two_altitudes_suffice (a b c h : Euclidean.Point)203  requires triangle : ¬Euclidean.Collinear(a, b, c)204  requires first : Euclidean.PerpendicularDirections(a, h, b, c)205  requires second : Euclidean.PerpendicularDirections(b, h, c, a)206  shows Euclidean.Orthocenter(h, a, b, c)207proof208  exact Euclidean.orthocenter.of_two_altitudes at a, b, c, h with *209210theorem unique_orthocenter (a b c h k : Euclidean.Point)211  requires triangle : ¬Euclidean.Collinear(a, b, c)212  requires first : Euclidean.Orthocenter(h, a, b, c)213  requires second : Euclidean.Orthocenter(k, a, b, c)214  shows h = k215proof216  exact Euclidean.orthocenter.unique at a, b, c, h, k with *217