the altitudes of a triangle are concurrent

Identifier: F:geometry-orthocentre-altitudes-concurrent
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, P be points of the Euclidean plane. If AP is perpendicular to BC and BP is perpendicular to CA, then CP is perpendicular to AB. NO non-degeneracy condition is required: in coordinates the statement is the polynomial identity (P-C).(B-A) + (P-A).(C-B) + (P-B).(A-C) = 0, which holds for all four points. The triangle must be non-degenerate for such a P to EXIST and be unique -- that is the standard side condition on the orthocentre -- but existence is a different claim and this fact does not make it.

Formal statement

(assert (forall ((ax Real) (ay Real) (bx Real) (by Real) (cx Real) (cy Real) (px Real) (py Real))
  (=> (and (= (+ (* (- px ax) (- cx bx)) (* (- py ay) (- cy by))) 0.0)
           (= (+ (* (- px bx) (- ax cx)) (* (- py by) (- ay cy))) 0.0))
      (= (+ (* (- px cx) (- bx ax)) (* (- py cy) (- by ay))) 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-orthocentre-altitudes-concurrent

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

Both cofactors are the constant -1. That is the sharpest single result in this corpus: the concurrency of the altitudes -- the theorem whose textbook statement always carries `for a triangle` -- is, in the universally quantified incidence form, an unconditional linear identity between the three perpendicularity polynomials.

geometry-coordinatisation-control-orthocentre

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 sweep asserts a POSITIVE count of perpendicular configurations, so the agreement is not vacuous on the side that matters.

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": "classical; the vector proof is usually credited to the 19th-century synthetic tradition and the concurrency itself was known to Archimedes' commentators",
      "what": "the three altitudes of a triangle meet in a point (the orthocentre)",
      "where": "standard; see e.g. Coxeter and Greitzer, Geometry Revisited (1967), section 1.4",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}