Grace/Cumulus/Geometry/Circle.g17

Open in Workbench Download source

Imports

Isosceles

Declarations

• Midpoint predicate
• OnCircle predicate
• diameter_identity theorem derivation
• thales theorem derivation
• pythagoras_converse theorem derivation

Source

1-- A diameter subtends a right angle: Thales' circle theorem.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.Circle8import Isosceles910namespace Euclidean11export open Euclidean1213predicate Midpoint (m a b : Set) :=14  x(a) + x(b) = x(m) + x(m) ∧15  y(a) + y(b) = y(m) + y(m)1617-- The radius is specified by a point on the circle; no square-root choice18-- is needed. Nonzero radius is imposed only when a nondegenerate angle is used.19predicate OnCircle (p center through : Set) :=20  Euclidean.distanceSquared(p, center) = Euclidean.distanceSquared(through, center)2122-- The underlying identity includes degenerate configurations. All points23-- and lengths here are defined using ordered pairs and real arithmetic.24theorem diameter_identity (a b p center : Point)25  requires midpoint : Midpoint(center, a, b)26  shows angleDot(a, p, b) =27    Euclidean.distanceSquared(p, center) - Euclidean.distanceSquared(a, center)28proof29  rcases midpoint with ⟨horizontal, vertical⟩30  have angle := angleDot.coordinates at a, p, b with *31  have pointRadius := Euclidean.distanceSquared.coordinates at p, center with *32  have endpointRadius := Euclidean.distanceSquared.coordinates at a, center with *33  rw [angle, pointRadius, endpointRadius]34  linear_combination (x(a) - x(p)) * horizontal + (y(a) - y(p)) * vertical3536-- A point on the circle sees the diameter at a right angle.37-- Endpoint exclusion makes both rays nonzero, as angle language requires.38theorem thales (a b p center : Point)39  requires midpoint : Midpoint(center, a, b)40  requires onCircle : OnCircle(p, center, a)41  requires firstRay : a ≠ p42  requires secondRay : p ≠ b43  shows RightAngle(a, p, b) ∧44    0 < Euclidean.distanceSquared(a, p) ∧ 0 < Euclidean.distanceSquared(p, b)45proof46  have identity := diameter_identity at a, b, p, center with *47  have first := Euclidean.distanceSquared.positive at a, p with *48  have second := Euclidean.distanceSquared.positive at p, b with *49  unfold OnCircle at onCircle50  refine ⟨_, first, second⟩51  unfold RightAngle52  linear_combination identity + onCircle5354-- The converse needs no side-length square roots or nondegeneracy.55theorem pythagoras_converse (a b c : Point)56  requires sides : Euclidean.distanceSquared(a, c) =57    Euclidean.distanceSquared(a, b) + Euclidean.distanceSquared(b, c)58  shows RightAngle(a, b, c)59proof60  have identity := cosine_identity at a, b, c with *61  have doubled : angleDot(a, b, c) + angleDot(a, b, c) = (0:R) + (0:R) by linear_combination identity - sides62  unfold RightAngle63  exact realAddValue.double_cancel with realZero.real, doubled6465end Euclidean66