the medians of a triangle are concurrent

Identifier: F:geometry-medians-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 and let Ma, Mb, Mc be the midpoints of BC, CA, AB. If P is collinear with A and Ma, and collinear with B and Mb, then P is collinear with C and Mc. NO non-degeneracy condition is required for this incidence form: the conclusion lies in the plain hypothesis ideal with constant cofactors (-1, -1). What DOES require one is locating the meeting point, which is F:geometry-centroid-divides-medians.

Formal statement

(assert (forall ((ax Real) (ay Real) (bx Real) (by Real) (cx Real) (cy Real) (px Real) (py Real))
  (let ((max (/ (+ bx cx) 2.0)) (may (/ (+ by cy) 2.0))
        (mbx (/ (+ cx ax) 2.0)) (mby (/ (+ cy ay) 2.0))
        (mcx (/ (+ ax bx) 2.0)) (mcy (/ (+ ay by) 2.0)))
    (=> (and (= (- (* (- max ax) (- py ay)) (* (- may ay) (- px ax))) 0.0)
             (= (- (* (- mbx bx) (- py by)) (* (- mby by) (- px bx))) 0.0))
        (= (- (* (- mcx cx) (- py cy)) (* (- mcy cy) (- px cx))) 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-medians-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, exactly as for the altitudes: the three median-incidence polynomials sum to zero identically. The certifier tries the empty condition set first, so the absence of `geometry.nondegeneracy.*` from this fact's footprint is the search's answer rather than the author's assumption; the same certifier run on F:geometry-centroid-divides-medians, which shares these two hypotheses verbatim, reports that a condition IS consumed.

geometry-coordinatisation-control-medians

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 opens with hand-picked degenerate shapes -- two coincident points, four collinear points, four collinear vertical points, all four coincident -- because that is where two encodings of the same predicate are most likely to part company.

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 Greek geometry; the centroid construction is in Archimedes' On the Equilibrium of Planes",
      "what": "the three medians of a triangle meet in a point",
      "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"
    }
  ]
}