Thales' theorem: an angle inscribed in a semicircle is right

Identifier: F:geometry-thales-right-angle-in-semicircle
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-polynomial-normal-form, geometry.cartesian-coordinatisation-of-the-euclidean-plane, geometry.characteristic-zero-specialisation

Recorded description

Let A, B, C be points of the Euclidean plane, let O be the midpoint of AB, and suppose |OC| = |OA|, i.e. C lies on the circle with diameter AB. Then CA is perpendicular to CB. NO non-degeneracy condition is required, and this is not an oversight: when A = B the circle degenerates to the single point O = A = B, the hypothesis forces C = A = B, and the conclusion holds because the zero vector is orthogonal to everything. The theorem is true on the degeneracy locus, not merely off it.

Formal statement

(assert (forall ((ax Real) (ay Real) (bx Real) (by Real) (cx Real) (cy Real))
  (let ((ox (/ (+ ax bx) 2.0)) (oy (/ (+ ay by) 2.0)))
    (=> (= (+ (* (- cx ox) (- cx ox)) (* (- cy oy) (- cy oy)))
           (+ (* (- ax ox) (- ax ox)) (* (- ay oy) (- ay oy))))
        (= (+ (* (- ax cx) (- bx cx)) (* (- ay cy) (- by cy))) 0.0)))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 1 direct dependents

Evidence

geometry-certificate-thales-right-angle-in-semicircle

Kind: witness-replay
Status: checked

Supports: the cofactor certificate, re-checked from the committed artifact by a checker that shares no code with the search that produced it

Checker command

cargo test -p axeyum-cas --test geometry_certificate_artifacts

Evidence notes

The certificate has a SINGLE cofactor, the constant +1: Thales' theorem in coordinates is the bare identity (A-C).(B-C) = |C-O|^2 - |A-O|^2 with O the midpoint of AB. That is the whole proof, and the constancy of the cofactor is why no side condition can arise -- nothing in the identity is divided by anything.

geometry-coordinatisation-control-thales

Kind: witness-replay
Status: checked

Supports: that the polynomials in the certificate mean the geometric predicates they are named after

Checker command

cargo test -p axeyum-cas --test geometry_encoding_agreement

Evidence notes

The equidistance row is the strongest of the three: the concrete module computes an exact radical and compares CasExpr values, so agreement is not a restatement of the same squared-distance arithmetic.

Provenance

{
  "date": "2026-08-14",
  "established_by": "lane geometry: axeyum_cas::geometry_certify (untrusted cofactor-tracked Buchberger search) + axeyum_cas::geometry_check (independent re-derivation)",
  "source": "classical; coordinatised by this lane",
  "prior_art": [
    {
      "who": "Thales of Miletus",
      "what": "an angle inscribed in a semicircle is right",
      "where": "attributed by Diogenes Laertius; Euclid, Elements III.31",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}