the perpendicular bisector planes of a tetrahedron's edges are concurrent

Identifier: F:geometry-tetrahedron-perpendicular-bisectors-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

Recorded description

Let A, B, C, D and P be points of Euclidean 3-space. If P is equidistant from A and B, from B and C, and from C and D, then P is equidistant from A and C, from B and D, and from A and D -- so all six perpendicular-bisector planes of the tetrahedron ABCD's edges pass through P. NO non-degeneracy condition is required: each conclusion is a telescoping sum of the hypotheses (`P eq A,C` = `P eq A,B` + `P eq B,C`, `P eq B,D` = `P eq B,C` + `P eq C,D`, `P eq A,D` = the sum of all three), valid for ANY five points. The tetrahedron must be non-degenerate for such a P to EXIST and be unique -- that is the standard side condition on the circumcentre -- but existence is a different claim and this fact does not make it. This is the solid-geometry analogue of F:geometry-orthocentre-altitudes-concurrent, and it is unconditional for the same reason.

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 (= (+ (* ax ax) (* ay ay) (* az az) (* 2.0 bx px) (* 2.0 by py) (* 2.0 bz pz)) (+ (* 2.0 ax px) (* 2.0 ay py) (* 2.0 az pz) (* bx bx) (* by by) (* bz bz)))
           (= (+ (* bx bx) (* by by) (* bz bz) (* 2.0 cx px) (* 2.0 cy py) (* 2.0 cz pz)) (+ (* 2.0 bx px) (* 2.0 by py) (* 2.0 bz pz) (* cx cx) (* cy cy) (* cz cz)))
           (= (+ (* cx cx) (* cy cy) (* cz cz) (* 2.0 dx px) (* 2.0 dy py) (* 2.0 dz pz)) (+ (* 2.0 cx px) (* 2.0 cy py) (* 2.0 cz pz) (* dx dx) (* dy dy) (* dz dz))))
      (and (= (+ (* ax ax) (* ay ay) (* az az) (* 2.0 cx px) (* 2.0 cy py) (* 2.0 cz pz)) (+ (* 2.0 ax px) (* 2.0 ay py) (* 2.0 az pz) (* cx cx) (* cy cy) (* cz cz)))
           (= (+ (* bx bx) (* by by) (* bz bz) (* 2.0 dx px) (* 2.0 dy py) (* 2.0 dz pz)) (+ (* 2.0 bx px) (* 2.0 by py) (* 2.0 bz pz) (* dx dx) (* dy dy) (* dz dz)))
           (= (+ (* ax ax) (* ay ay) (* az az) (* 2.0 dx px) (* 2.0 dy py) (* 2.0 dz pz)) (+ (* 2.0 ax px) (* 2.0 ay py) (* 2.0 az pz) (* dx dx) (* dy dy) (* dz 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-perpendicular-bisectors-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

Every cofactor is the constant 1: `P eq A,C` uses generators 0 and 1, `P eq B,D` uses 1 and 2, and `P eq A,D` uses all three, for 2 + 2 + 3 = 7 cofactor terms across the whole certificate. That is the same shape as the plane's orthocentre certificate, whose cofactors are all the constant -1, and it is the sharpest form the claim can take: the concurrency of the six bisector planes -- the theorem whose textbook statement always carries `for a tetrahedron` -- is, in the universally quantified incidence form, an unconditional linear identity between the equidistance polynomials.

Provenance

{
  "date": "2026-09-06",
  "established_by": "lane geometry: axeyum_cas::geometry_certify (untrusted cofactor-tracked search) + 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 circumsphere of a non-degenerate tetrahedron is standard, and the concurrency of the six bisector planes is the statement underlying it",
      "what": "the six perpendicular bisector planes of a tetrahedron's edges meet in a point, the circumcentre",
      "where": "standard; see e.g. Altshiller-Court, Modern Pure Solid Geometry (2nd ed., 1964), chapter 4",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}