the diagonals of a non-flat parallelogram bisect each other

Identifier: F:geometry-parallelogram-diagonals-bisect
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.abd-not-collinear

Recorded description

Let A, B, C, D be points of the Euclidean plane. If AB is parallel to DC, BC is parallel to AD, and A, B, D are NOT collinear, then the midpoint of AC equals the midpoint of BD. The non-degeneracy condition is essential and its failure is exhibited, not asserted: A = (0,0), B = (1,0), C = (2,0), D = (5,0) satisfies both parallelism hypotheses -- every direction along a line is parallel to every other -- while the midpoint of AC is (1,0) and the midpoint of BD is (3,0).

Formal statement

(assert (forall ((ax Real) (ay Real) (bx Real) (by Real) (cx Real) (cy Real) (dx Real) (dy Real))
  (=> (and (= (- (* (- bx ax) (- cy dy)) (* (- by ay) (- cx dx))) 0.0)
           (= (- (* (- cx bx) (- dy ay)) (* (- cy by) (- dx ax))) 0.0)
           (not (= (- (* (- bx ax) (- dy ay)) (* (- by ay) (- dx ax))) 0.0)))
      (and (= (+ ax cx) (+ bx dx))
           (= (+ ay cy) (+ by dy))))))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

geometry-certificate-parallelogram-diagonals-bisect

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,D) * Zinv0 - 1`. Specialising Zinv0 := 1/collinear(A,B,D) is legitimate exactly when the parallelogram is not flat, and that is the ONLY place the side condition enters. The cofactor of the saturation generator is minus the conclusion itself, 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-parallelogram

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

The parallelism row is where the degenerate branch is most instructive: when two points coincide the older module refuses to call the segment a line at all, while the determinant vanishes because the zero vector is parallel to everything. The test asserts that this is the ONLY way the two encodings can differ, rather than skipping the case quietly -- which is also exactly the configuration class the counterexample above lives in.

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": "Euclid",
      "what": "in a parallelogram the diameters bisect one another",
      "where": "Elements I.34 (and its corollary)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}