Varignon's theorem over the constructed reals: the midpoint quadrilateral is a parallelogram in CPoint

Identifier: F:geometry-varignon-over-constructed-reals
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any four points A, B, C, D of the plane CPoint = CReal x CReal over the constructed (Bishop) reals, let P, Q, R, S be the midpoints of AB, BC, CD, DA. Then Q - P and R - S are equal as CPoint vectors, under CPoint.Equiv (the pointwise CReal.Equiv, a DEFINED Prop relation, not Eq). No non-degeneracy condition is required. This is a statement about CPoint and nothing else; it is NOT the classical Euclidean-plane Varignon theorem, which is recorded separately as F:geometry-varignon-midpoint-parallelogram and rests on a coordinatisation assumption this one does not need and does not supply.

Formal statement

theorem CPoint.varignon_vector_parallel : ((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : CPoint) -> ((x3 : CPoint) -> CPoint.Equiv (CPoint.sub (CPoint.midpoint x1 x2) (CPoint.midpoint x0 x1)) (CPoint.sub (CPoint.midpoint x2 x3) (CPoint.midpoint x3 x0))))))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-CPoint.varignon_vector_parallel

Kind: kernel-term
Status: checked

Supports: For any four points A, B, C, D, writing P, Q, R, S for the midpoints of AB, BC, CD, DA, the vector Q - P equals the vector R - S -- proved as `CPoint.varignon_vector_parallel` over the constructed reals (`CReal`), matching the ledger statement's vector-difference form exactly (not the weaker midpoint-of-diagonals form `CPoint.varignon_diagonals_bisect` this lane proved first).

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal_point::creal_point_tests::varignon_vector_parallel_is_a_sub_statement_not_a_midpoint_statement -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

This re-derives the proof from source every run: the checker command re-builds `CPointPrelude` (which re-typechecks `CReal.add_right_cancel`, `CPoint.Scalar.sum_of_midpoints_perm`, `CPoint.Scalar.midpoint_vector_swap` and `CPoint.varignon_vector_parallel` through the kernel's trusted `add_declaration` gate) and then asserts the resulting theorem's RENDERED TYPE matches the statement above character for character. Anchored on the exact `1 passed; 0 failed` count, so a filter that silently matches nothing cannot read as success. Verified by construction, not by a mutation run: the assert_eq! in that test is exact-string, so any of {wrong argument order, `midpoint` in place of `sub`, a dropped `neg`, a swapped `P`/`Q`} changes the rendered string and fails it.

footprint-CPoint.varignon_vector_parallel

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] -- the theorem and everything it is built from (`add_right_cancel`, `sum_of_midpoints_perm`, `midpoint_vector_swap`, `point_sub`, and the `CReal`/`CPoint` prelude beneath them) are all checked declarations with an empty `Kernel::axiom_footprint`, over a trusted surface this lane did not add to.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal_point::creal_point_tests:: 2>&1 | grep -Ec 'test result: ok\. 5 passed; 0 failed')" -ge 1

Evidence notes

Counting `Declaration::Axiom` alone would not suffice in this kernel (`Opaque` has no proof body and `Quotient` admits `Quot.sound`); `axiom_footprint` covers all three, and this file introduces none of them -- `CReal.add_right_cancel` is a `Theorem` built from `add_zero`/`add_neg`/`add_assoc`/`add_congr` alone, and `CPoint.sub` is a plain `Definition`. Anchored on the NONZERO, exact test count (5) for this module, so a dropped test cannot silently shrink what 'passed' means.

Provenance

{
  "date": "2026-08-14",
  "established_by": "lane geometry (2026-08-14): axeyum_cas::geometry_certify (untrusted cofactor-tracked Buchberger search) + axeyum_cas::geometry_check (independent re-derivation) -- the ORIGINAL route, superseded as the recorded proof_route on 2026-08-22 by a geometry lane's `crates/axeyum-lean-kernel/src/creal_point.rs`: `CPoint.varignon_vector_parallel`, a kernel theorem over `CReal` (the constructed reals, ADR-0512) matching this fact's vector-difference statement exactly and admitting with an empty `axiom_footprint`.",
  "source": "classical; coordinatised by the geometry 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"
    }
  ]
}