Grace/Cumulus/Geometry/Centroid.g17

Open in Workbench Download source

Imports

Parallelogram

Declarations

Source

1-- The centroid and the three medians of a 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.Centroid8import Parallelogram910namespace Euclidean11export open Euclidean1213-- Affine balance, including collinear and collapsed triangles.14predicate Centroid (g a b c : Set) :=15  x(g) + x(g) + x(g) = x(a) + x(b) + x(c) ∧16  y(g) + y(g) + y(g) = y(a) + y(b) + y(c)1718def centroid (a b c : Set) : Set :=19  (third(x(a) + x(b) + x(c)),20   third(y(a) + y(b) + y(c)))2122-- Directed displacement AG is twice GM. This identity also allows A = G = M;23-- interpreting a quotient of nonzero lengths requires nondegeneracy separately.24predicate MedianRatio (a g m : Set) :=25  x(g) - x(a) = (x(m) - x(g)) + (x(m) - x(g)) ∧26  y(g) - y(a) = (y(m) - y(g)) + (y(m) - y(g))2728theorem centroid.point (a b c : Point)29  shows Point(centroid(a, b, c))30proof31  unfold centroid32  exact pair.point with *3334theorem centroid.correct (a b c : Point)35  shows Centroid(centroid(a, b, c), a, b, c)36proof37  have horizontal := x.pair at third(x(a) + x(b) + x(c)), third(y(a) + y(b) + y(c)) with *38  have vertical := y.pair at third(x(a) + x(b) + x(c)), third(y(a) + y(b) + y(c)) with *39  have tripleX := third.add_self at x(a) + x(b) + x(c) with *40  have tripleY := third.add_self at y(a) + y(b) + y(c) with *41  constructor42  . unfold centroid43    cc44  . unfold centroid45    cc4647theorem centroid.rotate (a b c g : Point)48  requires center : Centroid(g, a, b, c)49  shows Centroid(g, b, c, a)50proof51  rcases center with ⟨horizontal, vertical⟩52  constructor53  . linear_combination horizontal54  . linear_combination vertical5556theorem centroid.unique (a b c g h : Point)57  requires first : Centroid(g, a, b, c)58  requires second : Centroid(h, a, b, c)59  shows g = h60proof61  rcases first with ⟨firstX, firstY⟩62  rcases second with ⟨secondX, secondY⟩63  have tripledX : x(g) + x(g) + x(g) = x(h) + x(h) + x(h) by cc64  have tripledY : y(g) + y(g) + y(g) = y(h) + y(h) + y(h) by cc65  have horizontal := realAddValue.triple_cancel at x(g), x(h) with *66  have vertical := realAddValue.triple_cancel at y(g), y(h) with *67  exact point.ext with *6869theorem centroid.median_ratio (a b c g m : Point)70  requires center : Centroid(g, a, b, c)71  requires middle : Midpoint(m, b, c)72  shows MedianRatio(a, g, m)73proof74  rcases center with ⟨centerX, centerY⟩75  rcases middle with ⟨middleX, middleY⟩76  constructor77  . linear_combination centerX + middleX78  . linear_combination centerY + middleY7980theorem medianRatio.collinear (a g m : Point)81  requires ratio : MedianRatio(a, g, m)82  shows Collinear(a, g, m)83proof84  unfold Collinear85  unfold directionCross86  rcases ratio with ⟨horizontal, vertical⟩87  linear_combination (y(m) - y(g)) * horizontal - (x(m) - x(g)) * vertical8889-- The public median argument uses affine balance and midpoint facts only.90theorem centroid.medians (a b c g m n p : Point)91  requires center : Centroid(g, a, b, c)92  requires first : Midpoint(m, b, c)93  requires second : Midpoint(n, c, a)94  requires third : Midpoint(p, a, b)95  shows MedianRatio(a, g, m) ∧ MedianRatio(b, g, n) ∧ MedianRatio(c, g, p)96proof97  have rotated := centroid.rotate with *98  have again := centroid.rotate at b, c, a, g with *99  have firstRatio := centroid.median_ratio at a, b, c, g, m with *100  have secondRatio := centroid.median_ratio at b, c, a, g, n with *101  have thirdRatio := centroid.median_ratio at c, a, b, g, p with *102  refine ⟨firstRatio, secondRatio, thirdRatio⟩103104theorem centroid.concurrency (a b c m n p : Point)105  requires first : Midpoint(m, b, c)106  requires second : Midpoint(n, c, a)107  requires third : Midpoint(p, a, b)108  shows ∃ g, Point(g) ∧ Centroid(g, a, b, c) ∧109    Collinear(a, g, m) ∧ Collinear(b, g, n) ∧ Collinear(c, g, p)110proof111  have point := centroid.point at a, b, c with *112  have center := centroid.correct at a, b, c with *113  have ratios := centroid.medians with *114  rcases ratios with ⟨firstRatio, secondRatio, thirdRatio⟩115  have firstLine := medianRatio.collinear at a, centroid(a, b, c), m with *116  have secondLine := medianRatio.collinear at b, centroid(a, b, c), n with *117  have thirdLine := medianRatio.collinear at c, centroid(a, b, c), p with *118  refine ⟨centroid(a, b, c), point, center, firstLine, secondLine, thirdLine⟩119120-- The directed 2:1 relation implies the corresponding squared-length identity.121theorem medianRatio.length (a g m : Point)122  requires ratio : MedianRatio(a, g, m)123  shows Euclidean.distanceSquared(a, g) =124    Euclidean.distanceSquared(g, m) + Euclidean.distanceSquared(g, m) +125    Euclidean.distanceSquared(g, m) + Euclidean.distanceSquared(g, m)126proof127  rcases ratio with ⟨horizontal, vertical⟩128  have doubledX : (x(m) - x(g)) + (x(m) - x(g)) = x(g) - x(a)129    symm130    exact horizontal131  have doubledY : (y(m) - y(g)) + (y(m) - y(g)) = y(g) - y(a)132    symm133    exact vertical134  have squareX := realMulValue.square_of_double at x(m) - x(g), x(g) - x(a) with *135  have squareY := realMulValue.square_of_double at y(m) - y(g), y(g) - y(a) with *136  have long := Euclidean.distanceSquared.coordinates at a, g with *137  have short := Euclidean.distanceSquared.coordinates at g, m with *138  rw [long, short, squareX, squareY]139  ring140141theorem centroid.repeated (a : Point)142  shows centroid(a, a, a) = a143proof144  have point := centroid.point with *145  have first := centroid.correct at a, a, a with *146  have second : Centroid(a, a, a, a)147    constructor148    . rfl149    . rfl150  exact centroid.unique with *151152end Euclidean153