the medians of a non-degenerate triangle meet at (A+B+C)/3

Identifier: F:geometry-centroid-divides-medians
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, geometry.rabinowitsch-inverse-specialisation, geometry.nondegeneracy.abc-not-collinear

Recorded description

Let A, B, C, P be points of the Euclidean plane and let Ma, Mb be the midpoints of BC and CA. If A, B, C are NOT collinear, and P is collinear with A and Ma and collinear with B and Mb, then 3P = A + B + C. The non-degeneracy condition is essential and its failure is exhibited, not asserted: A = (0,0), B = (1,0), C = (2,0), P = (7,0) satisfies both hypotheses -- B coincides with the midpoint of CA, so the second one becomes vacuous -- while 3P.x = 21 and A.x + B.x + C.x = 3.

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)))
    (=> (and (= (- (* (- max ax) (- py ay)) (* (- may ay) (- px ax))) 0.0)
             (= (- (* (- mbx bx) (- py by)) (* (- mby by) (- px bx))) 0.0)
             (not (= (- (* (- bx ax) (- cy ay)) (* (- by ay) (- cx ax))) 0.0)))
        (and (= (* 3.0 px) (+ ax bx cx))
             (= (* 3.0 py) (+ ay by cy)))))))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

geometry-certificate-centroid-divides-medians

Kind: witness-replay
Status: checked

Supports: the saturated 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 uses the Rabinowitsch trick: a fresh variable Zinv0 and the generator `collinear(A,B,C) * Zinv0 - 1`. Specialising Zinv0 := 1/collinear(A,B,C) is legitimate exactly when the triangle is non-degenerate, and that is the ONLY place the side condition enters. The cofactor of the saturation generator is -(3 P.x - A.x - B.x - C.x), i.e. minus the conclusion itself, which is the signature shape of a Rabinowitsch witness. Tamper controls in the same suite that bear directly on this fact: DELETING the degenerate counterexample is rejected, and REPLACING it with a non-degenerate configuration (which therefore fails to break the theorem) is rejected.

geometry-coordinatisation-control-centroid

Kind: witness-replay
Status: checked

Supports: that the polynomials in the certificate mean the geometric predicates they are named after -- including the non-degeneracy condition, whose meaning is what makes or breaks this fact

Checker command

cargo test -p axeyum-cas --test geometry_encoding_agreement

Evidence notes

This control matters more here than for the unconditional facts: the side condition is `this polynomial does not vanish`, so an encoding that got collinearity wrong would relabel the degeneracy locus and the theorem would be about a different set of configurations than its statement claims.

Provenance

{
  "date": "2026-08-14",
  "established_by": "lane geometry: axeyum_cas::geometry_certify (untrusted cofactor-tracked Buchberger search, minimal condition subset) + axeyum_cas::geometry_check (independent re-derivation)",
  "source": "classical; coordinatised by this lane, with the non-degeneracy condition DERIVED by the certifier rather than supplied",
  "prior_art": [
    {
      "who": "classical Greek geometry; the centroid construction is in Archimedes' On the Equilibrium of Planes",
      "what": "the medians of a triangle meet at the centroid, which divides each in the ratio 2:1",
      "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"
    }
  ]
}