Varignon's theorem: the midpoint quadrilateral is a parallelogram

Identifier: F:geometry-varignon-midpoint-parallelogram
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

For any four points A, B, C, D of the Euclidean plane, let P, Q, R, S be the midpoints of AB, BC, CD, DA respectively. Then the vector from P to Q equals the vector from S to R, so PQRS is a parallelogram. NO non-degeneracy condition is required: the statement holds for every configuration whatsoever, including collinear quadrilaterals and coincident vertices, in which case the parallelogram is degenerate but the vector identity still holds.

Formal statement

(assert (forall ((ax Real) (ay Real) (bx Real) (by Real) (cx Real) (cy Real) (dx Real) (dy Real))
  (let ((px (/ (+ ax bx) 2.0)) (py (/ (+ ay by) 2.0))
        (qx (/ (+ bx cx) 2.0)) (qy (/ (+ by cy) 2.0))
        (rx (/ (+ cx dx) 2.0)) (ry (/ (+ cy dy) 2.0))
        (sx (/ (+ dx ax) 2.0)) (sy (/ (+ dy ay) 2.0)))
    (and (= (- qx px) (- rx sx))
         (= (- qy py) (- ry sy))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

geometry-certificate-varignon-midpoint-parallelogram

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

The certificate is degenerate in an informative way: the generator list is EMPTY and both conclusion polynomials are identically zero, so the cofactor vector is empty and the identity is `0 = 0`. That is not a gap -- it is what Varignon's theorem IS in coordinates, and it is why the theorem needs no hypothesis and no non-degeneracy condition. The suite's tamper controls (a conclusion edited by one, a truncated file, a foreign format tag, a decimal where an exact integer belongs) all reject.

geometry-coordinatisation-control-varignon

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 coordinatisation is the one assumption on this route that no amount of exact arithmetic verifies, so it is attacked from outside instead: a second implementation of the same predicates, written for concrete rational points, must decide identically on a sweep that deliberately includes the degenerate shapes.

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": "Pierre Varignon",
      "what": "the midpoint quadrilateral of an arbitrary quadrilateral is a parallelogram",
      "year": 1731,
      "where": "Elemens de mathematique (posthumous, 1731)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}