the diagonals of a non-flat rhombus are perpendicular

Identifier: F:geometry-rhombus-diagonals-perpendicular
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, |AB| = |BC|, and A, B, D are NOT collinear, then AC is perpendicular to 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 -- and satisfies |AB| = |BC| = 1, while AC.BD = (2,0).(4,0) = 8, so the diagonals are not perpendicular. Sitting on the degeneracy locus is not by itself enough to break the theorem: A = (0,0), B = (1,0), C = (2,0), D = (1,0) is also collinear and its diagonals ARE perpendicular, and the checker rejects a certificate offering that configuration as its counterexample.

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)
           (= (- (+ (* (- bx ax) (- bx ax)) (* (- by ay) (- by ay)))
                 (+ (* (- cx bx) (- cx bx)) (* (- cy by) (- cy by)))) 0.0)
           (not (= (- (* (- bx ax) (- dy ay)) (* (- by ay) (- dx ax))) 0.0)))
      (= (+ (* (- cx ax) (- dx bx)) (* (- cy ay) (- dy by))) 0.0))))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

geometry-certificate-rhombus-diagonals-perpendicular

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 A, B, D are not collinear, and that is the ONLY place the side condition enters. Three tamper controls in the same suite bear directly on this fact and every one of them now runs against EVERY saturated certificate rather than only the alphabetically first: DELETING the degenerate counterexample is rejected; REPLACING it with a generic configuration is rejected; and replacing it with A = (0,0), B = (1,0), C = (2,0), D = (1,0) -- which genuinely violates `abd-not-collinear` but does NOT falsify the conclusion -- is also rejected. That last one is the control that distinguishes a counterexample from a configuration that merely sits on the degeneracy locus.

geometry-coordinatisation-control-rhombus

Kind: witness-replay
Status: checked

Supports: that the polynomials in the certificate mean the geometric predicates they are named after -- including the quadratic |AB| = |BC| hypothesis that distinguishes this theorem from `F:geometry-parallelogram-diagonals-bisect`, and 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 equidistance row is the one this fact adds over its parallelogram sibling. |AB| = |BC| is stated on SQUARED distances so it stays polynomial, and the control checks that against the exact irrational distances themselves rather than against another squaring -- the two are equal for non-negative reals, and that is the step a squared-distance encoding silently assumes.

Provenance

{
  "date": "2026-08-15",
  "established_by": "lane geometry-frontier: axeyum_cas::geometry_certify (untrusted cofactor-tracked Buchberger search, minimal condition subset) + axeyum_cas::geometry_check (independent re-derivation)",
  "source": "classical; coordinatised by the `geometry` lane, with the non-degeneracy condition DERIVED by the certifier rather than supplied, and reached by the `geometry-frontier` lane after the default monomial order changed",
  "prior_art": [
    {
      "who": "Euclid",
      "what": "the diagonals of a rhombus bisect its angles and cut one another at right angles",
      "where": "Elements I.34 with the equilateral case; standard textbook corollary",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}