Grace/Cumulus/Geometry/Chords.g17

Open in Workbench Download source

Imports

Circle · Distance

Declarations

Source

1-- Intersecting chords: the power of a point with respect to a circle, and2-- the equal products of the segments of two chords through one point.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Chords9import Circle10import Distance1112namespace Euclidean13export open Euclidean1415-- A point p of the line through a and b, written p = a + t(b − a).16predicate OnLine (p a b t : Set) :=17  x(p) = x(a) + (t:R) * (x(b) - x(a)) ∧ y(p) = y(a) + (t:R) * (y(b) - y(a))1819-- The power of a point: for a chord ab through p, the dot product of the20-- two segments at p is the squared distance to the center less the squared21-- radius, whatever the position of p on the line.22theorem chord.power (a b p center through : Point) (t : Real)23  requires onA : OnCircle(a, center, through)24  requires onB : OnCircle(b, center, through)25  requires onLine : OnLine(p, a, b, t)26  shows angleDot(a, p, b) =27    distanceSquared(p, center) - distanceSquared(a, center)28proof29  rcases onLine with ⟨horizontal, vertical⟩30  unfold OnCircle at onA31  unfold OnCircle at onB32  have angle := angleDot.coordinates at a, p, b with *33  have pointRadius := distanceSquared.coordinates at p, center with *34  have firstRadius := distanceSquared.coordinates at a, center with *35  have secondRadius := distanceSquared.coordinates at b, center with *36  have throughRadius := distanceSquared.coordinates at through, center with *37  rw [firstRadius, throughRadius] at onA38  rw [secondRadius, throughRadius] at onB39  rw [angle, pointRadius, firstRadius, horizontal, vertical]40  linear_combination t * onA - t * onB4142-- The squared segments of a chord through p, in terms of the parameter.43theorem chord.segment_squares (a b p : Point) (t : Real)44  requires onLine : OnLine(p, a, b, t)45  shows distanceSquared(p, a) * distanceSquared(p, b) =46    angleDot(a, p, b) * angleDot(a, p, b)47proof48  rcases onLine with ⟨horizontal, vertical⟩49  have first := distanceSquared.coordinates at p, a with *50  have second := distanceSquared.coordinates at p, b with *51  have angle := angleDot.coordinates at a, p, b with *52  rw [first, second, angle, horizontal, vertical]53  ring5455-- Two chords ab and cd through p: the products of the squared segments agree.56theorem chord.products_squared (a b c d p center through : Point) (t u : Real)57  requires onA : OnCircle(a, center, through)58  requires onB : OnCircle(b, center, through)59  requires onC : OnCircle(c, center, through)60  requires onD : OnCircle(d, center, through)61  requires firstLine : OnLine(p, a, b, t)62  requires secondLine : OnLine(p, c, d, u)63  shows distanceSquared(p, a) * distanceSquared(p, b) =64    distanceSquared(p, c) * distanceSquared(p, d)65proof66  have firstPower := chord.power at a, b, p, center, through, t with *67  have secondPower := chord.power at c, d, p, center, through, u with *68  have firstSquares := chord.segment_squares at a, b, p, t with *69  have secondSquares := chord.segment_squares at c, d, p, u with *70  unfold OnCircle at onA71  unfold OnCircle at onC72  have same : angleDot(a, p, b) = angleDot(c, p, d)73    linear_combination firstPower - secondPower - onA + onC74  rw [firstSquares, secondSquares, same]75  rfl7677-- The classical statement: the products of the segment lengths agree.78theorem chord.products (a b c d p center through : Point) (t u : Real)79  requires onA : OnCircle(a, center, through)80  requires onB : OnCircle(b, center, through)81  requires onC : OnCircle(c, center, through)82  requires onD : OnCircle(d, center, through)83  requires firstLine : OnLine(p, a, b, t)84  requires secondLine : OnLine(p, c, d, u)85  shows distance(p, a) * distance(p, b) = distance(p, c) * distance(p, d)86proof87  have squares := chord.products_squared at a, b, c, d, p, center, through, t, u88    with *89  have nonnegativeA := Euclidean.distanceSquared.nonnegative_real at p, a with *90  have nonnegativeB := Euclidean.distanceSquared.nonnegative_real at p, b with *91  have nonnegativeC := Euclidean.distanceSquared.nonnegative_real at p, c with *92  have nonnegativeD := Euclidean.distanceSquared.nonnegative_real at p, d with *93  have first := sqrt.mul with nonnegativeA, nonnegativeB94  have second := sqrt.mul with nonnegativeC, nonnegativeD95  unfold distance96  rw [← first, ← second, squares]97  rfl9899end Euclidean100