the medians of a tetrahedron meet at the centroid (A+B+C+D)/4, given that the tetrahedron is non-degenerate

Identifier: F:geometry-tetrahedron-medians-concurrent
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-polynomial-normal-form, geometry.cartesian-coordinatisation-of-euclidean-3-space, geometry.characteristic-zero-specialisation, geometry.rabinowitsch-inverse-specialisation, geometry.nondegeneracy.abcd-not-coplanar

Recorded description

Let A, B, C, D and P be points of Euclidean 3-space. If A, B, C, D are NOT coplanar, and P lies on the median from A (the line through A and the centroid of BCD) and on the median from B (through B and the centroid of ACD), then 4P = A + B + C + D -- so P is also on the medians from C and from D, and the four medians are concurrent at the centroid. The non-degeneracy condition is essential and its failure is exhibited rather than asserted: with A=(1,1,0), B=(0,0,0), C=(3,0,0), D=(0,3,0) all four points are coplanar and A is exactly the centroid of BCD, so the median from A is vacuous and satisfied by every P; P=(5,5,0) then lies on the median from B while 4P = (20,20,0) and A+B+C+D = (4,4,0). The condition set is a singleton and is minimal absolutely: its only proper subset is the empty one, and that committed configuration refutes it.

Formal statement

(assert (forall ((ax Real) (ay Real) (az Real) (bx Real) (by Real) (bz Real) (cx Real) (cy Real) (cz Real) (dx Real) (dy Real) (dz Real) (px Real) (py Real) (pz Real))
  (=> (and (= (+ (* (/ 1.0 3.0) ay bz) (* (/ 1.0 3.0) ay cz) (* (/ 1.0 3.0) ay dz) (* az py) (* (/ 1.0 3.0) by pz) (* (/ 1.0 3.0) cy pz) (* (/ 1.0 3.0) dy pz)) (+ (* ay pz) (* (/ 1.0 3.0) az by) (* (/ 1.0 3.0) az cy) (* (/ 1.0 3.0) az dy) (* (/ 1.0 3.0) bz py) (* (/ 1.0 3.0) cz py) (* (/ 1.0 3.0) dz py)))
           (= (+ (* ax pz) (* (/ 1.0 3.0) az bx) (* (/ 1.0 3.0) az cx) (* (/ 1.0 3.0) az dx) (* (/ 1.0 3.0) bz px) (* (/ 1.0 3.0) cz px) (* (/ 1.0 3.0) dz px)) (+ (* (/ 1.0 3.0) ax bz) (* (/ 1.0 3.0) ax cz) (* (/ 1.0 3.0) ax dz) (* az px) (* (/ 1.0 3.0) bx pz) (* (/ 1.0 3.0) cx pz) (* (/ 1.0 3.0) dx pz)))
           (= (+ (* (/ 1.0 3.0) ax by) (* (/ 1.0 3.0) ax cy) (* (/ 1.0 3.0) ax dy) (* ay px) (* (/ 1.0 3.0) bx py) (* (/ 1.0 3.0) cx py) (* (/ 1.0 3.0) dx py)) (+ (* ax py) (* (/ 1.0 3.0) ay bx) (* (/ 1.0 3.0) ay cx) (* (/ 1.0 3.0) ay dx) (* (/ 1.0 3.0) by px) (* (/ 1.0 3.0) cy px) (* (/ 1.0 3.0) dy px)))
           (= (+ (* (/ 1.0 3.0) ay pz) (* (/ 1.0 3.0) az by) (* (/ 1.0 3.0) by cz) (* (/ 1.0 3.0) by dz) (* bz py) (* (/ 1.0 3.0) cy pz) (* (/ 1.0 3.0) dy pz)) (+ (* (/ 1.0 3.0) ay bz) (* (/ 1.0 3.0) az py) (* by pz) (* (/ 1.0 3.0) bz cy) (* (/ 1.0 3.0) bz dy) (* (/ 1.0 3.0) cz py) (* (/ 1.0 3.0) dz py)))
           (= (+ (* (/ 1.0 3.0) ax bz) (* (/ 1.0 3.0) az px) (* bx pz) (* (/ 1.0 3.0) bz cx) (* (/ 1.0 3.0) bz dx) (* (/ 1.0 3.0) cz px) (* (/ 1.0 3.0) dz px)) (+ (* (/ 1.0 3.0) ax pz) (* (/ 1.0 3.0) az bx) (* (/ 1.0 3.0) bx cz) (* (/ 1.0 3.0) bx dz) (* bz px) (* (/ 1.0 3.0) cx pz) (* (/ 1.0 3.0) dx pz)))
           (= (+ (* (/ 1.0 3.0) ax py) (* (/ 1.0 3.0) ay bx) (* (/ 1.0 3.0) bx cy) (* (/ 1.0 3.0) bx dy) (* by px) (* (/ 1.0 3.0) cx py) (* (/ 1.0 3.0) dx py)) (+ (* (/ 1.0 3.0) ax by) (* (/ 1.0 3.0) ay px) (* bx py) (* (/ 1.0 3.0) by cx) (* (/ 1.0 3.0) by dx) (* (/ 1.0 3.0) cy px) (* (/ 1.0 3.0) dy px)))
           (not (= (+ (* ax by dz) (* ax bz cy) (* ax cz dy) (* ay bx cz) (* ay bz dx) (* ay cx dz) (* az bx dy) (* az by cx) (* az cy dx) (* bx cy dz) (* by cz dx) (* bz cx dy)) (+ (* ax by cz) (* ax bz dy) (* ax cy dz) (* ay bx dz) (* ay bz cx) (* ay cz dx) (* az bx cy) (* az by dx) (* az cx dy) (* bx cz dy) (* by cx dz) (* bz cy dx)))))
      (and (= (* 4.0 px) (+ ax bx cx dx))
           (= (* 4.0 py) (+ ay by cy dy))
           (= (* 4.0 pz) (+ az bz cz dz))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

geometry-certificate-tetrahedron-medians-concurrent

Kind: witness-replay
Status: checked

Supports: the saturated cofactor certificate over a SINGLE non-degeneracy condition, 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 condition enters only through the Rabinowitsch generator `volume * Zinv0 - 1`, where the volume polynomial is the 3x3 determinant of B-A, C-A, D-A written out; specialising Zinv0 := 1/volume is legitimate exactly when the four points are not coplanar, and that is the ONLY place the side condition enters. The three conclusions are the three coordinate components of 4P = A+B+C+D and are certified separately, each against the same seven generators. Every tamper control in the cited suite runs against this certificate too -- a cofactor edited by one, a conclusion edited by one, a swapped non-degeneracy condition, cofactors donated by a neighbouring certificate, a deleted counterexample, and a counterexample that sits on the locus without falsifying anything are each rejected.

geometry-condition-minimality-tetrahedron-medians-concurrent

Kind: witness-replay
Status: checked

Supports: that the single non-degeneracy condition this certificate consumes is minimal ABSOLUTELY rather than budget-relative (ADR-0455)

Checker command

cargo test -p axeyum-cas --test geometry_certificate_artifacts

Evidence notes

The only proper subset of a one-element condition set is the empty one, and the coplanar configuration satisfies all six hypotheses while falsifying a conclusion -- so the conclusion is not in the plain hypothesis ideal, decided, with no budget, no monomial order and no algorithm anywhere in the argument. The counterexample is doing real work rather than merely sitting on the locus: it is the case where the median from A degenerates to a vacuous hypothesis because A is itself the centroid of the opposite face, which is exactly how a coplanar tetrahedron can leave both median hypotheses satisfied by a point that is not the centroid.

Provenance

{
  "date": "2026-09-06",
  "established_by": "lane geometry: axeyum_cas::geometry_certify (untrusted cofactor-tracked search over the Rabinowitsch saturation) + axeyum_cas::geometry_check (independent re-derivation); this ledger row transcribes the committed certificate",
  "source": "classical; coordinatised in Euclidean 3-space by the certificate's lane",
  "prior_art": [
    {
      "who": "classical solid geometry; the result is the barycentric statement that the four medians of a tetrahedron meet at the centroid, dividing each in the ratio 3:1",
      "what": "the four medians of a tetrahedron are concurrent at (A+B+C+D)/4",
      "where": "standard; see e.g. Altshiller-Court, Modern Pure Solid Geometry (2nd ed., 1964), chapter 3",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}