Desargues' theorem in the affine plane: perspective from a point implies perspective from a line

Identifier: F:geometry-desargues-affine-perspective
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.bc-meets-b2c2, geometry.nondegeneracy.ca-meets-c2a2, geometry.nondegeneracy.ab-meets-a2b2

Recorded description

Let O, A, B, C be points of the affine plane and let A' = O + la*(A-O), B' = O + lb*(B-O), C' = O + lc*(C-O), so that the triangles ABC and A'B'C' are in perspective from O by construction (A' ranges over every finite point of the line OA). Let X lie on BC and on B'C', Y on CA and on C'A', and Z on AB and on A'B'. If BC is not parallel to B'C', CA is not parallel to C'A' and AB is not parallel to A'B', then X, Y and Z are collinear. This is the AFFINE reading: the centre, the six vertices and the three intersection points are all finite. The projective statement, where any of them may lie on the line at infinity, is a different statement and is neither certified nor claimed here. All three conditions are used and the set of them is minimal ABSOLUTELY, not budget-relatively: each of the seven proper subsets is refuted by a committed configuration that satisfies every hypothesis, keeps the subset's conditions nonzero, and falsifies the conclusion.

Formal statement

(assert (forall ((ax Real) (ay Real) (bx Real) (by Real) (cx Real) (cy Real) (la Real) (lb Real) (lc Real) (ox Real) (oy Real) (xx Real) (xy Real) (yx Real) (yy Real) (zx Real) (zy Real))
  (=> (and (= (+ (* bx cy) (* by xx) (* cx xy)) (+ (* bx xy) (* by cx) (* cy xx)))
           (= (+ (* bx cy lb lc) (* bx lb oy) (* by lb lc ox) (* by lb xx) (* cx lb lc oy) (* cx lc xy) (* cy lc ox) (* lb ox xy) (* lc oy xx)) (+ (* bx lb lc oy) (* bx lb xy) (* by cx lb lc) (* by lb ox) (* cx lc oy) (* cy lb lc ox) (* cy lc xx) (* lb oy xx) (* lc ox xy)))
           (= (+ (* ax yy) (* ay cx) (* cy yx)) (+ (* ax cy) (* ay yx) (* cx yy)))
           (= (+ (* ax la lc oy) (* ax la yy) (* ay cx la lc) (* ay la ox) (* cx lc oy) (* cy la lc ox) (* cy lc yx) (* la oy yx) (* lc ox yy)) (+ (* ax cy la lc) (* ax la oy) (* ay la lc ox) (* ay la yx) (* cx la lc oy) (* cx lc yy) (* cy lc ox) (* la ox yy) (* lc oy yx)))
           (= (+ (* ax by) (* ay zx) (* bx zy)) (+ (* ax zy) (* ay bx) (* by zx)))
           (= (+ (* ax by la lb) (* ax la oy) (* ay la lb ox) (* ay la zx) (* bx la lb oy) (* bx lb zy) (* by lb ox) (* la ox zy) (* lb oy zx)) (+ (* ax la lb oy) (* ax la zy) (* ay bx la lb) (* ay la ox) (* bx lb oy) (* by la lb ox) (* by lb zx) (* la oy zx) (* lb ox zy)))
           (not (= (+ (* bx cy lb) (* bx lc oy) (* by cx lc) (* by lb ox) (* cx lb oy) (* cy lc ox)) (+ (* bx cy lc) (* bx lb oy) (* by cx lb) (* by lc ox) (* cx lc oy) (* cy lb ox))))
           (not (= (+ (* ax cy la) (* ax lc oy) (* ay cx lc) (* ay la ox) (* cx la oy) (* cy lc ox)) (+ (* ax cy lc) (* ax la oy) (* ay cx la) (* ay lc ox) (* cx lc oy) (* cy la ox))))
           (not (= (+ (* ax by la) (* ax lb oy) (* ay bx lb) (* ay la ox) (* bx la oy) (* by lb ox)) (+ (* ax by lb) (* ax la oy) (* ay bx la) (* ay lb ox) (* bx lb oy) (* by la ox)))))
      (= (+ (* xx yy) (* xy zx) (* yx zy)) (+ (* xx zy) (* xy yx) (* yy zx))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

geometry-certificate-desargues-affine-perspective

Kind: witness-replay
Status: checked

Supports: the saturated cofactor certificate over THREE non-degeneracy conditions, 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 three conditions enter only through the Rabinowitsch generators `condition_i * Zinv_i - 1`; specialising Zinv_i := 1/condition_i is legitimate exactly when that pair of corresponding sides is not parallel. Each degenerate witness puts the centre O on one collapsing side line with the two ratios along it equal, so that side and its image are the SAME line: the intersection point is then free along that line rather than lost, which is why the configuration still satisfies every incidence hypothesis while breaking collinearity. Every tamper control in the cited suite runs against this certificate too -- a cofactor edited by one, a conclusion edited by one, a swapped non-degeneracy condition, cofactors donated by a neighbouring certificate, a deleted counterexample, and a counterexample that sits on the locus without falsifying anything are each rejected.

geometry-condition-minimality-desargues-affine-perspective

Kind: witness-replay
Status: checked

Supports: that the three non-degeneracy conditions this certificate consumes form a set that is minimal ABSOLUTELY rather than budget-relative (ADR-0455)

Checker command

cargo test -p axeyum-cas --test geometry_certificate_artifacts

Evidence notes

This is the corpus's first three-condition certificate to be checked this way, so it is the case that exercises the subset enumeration rather than merely satisfying it: a one-condition certificate has exactly one proper subset (the empty one), while this theorem has seven, and each must be refuted by a committed configuration. Refuting the singletons and the pairs is the part that a budget-relative claim cannot deliver, because a subset can fail a bounded-degree search for reasons that have nothing to do with the theorem.

Provenance

{
  "date": "2026-09-06",
  "established_by": "lane geometry: axeyum_cas::geometry_certify (untrusted cofactor-tracked search over the Rabinowitsch saturation) + axeyum_cas::geometry_check (independent re-derivation); this ledger row transcribes the committed certificate",
  "source": "classical; coordinatised in the affine plane, with the second triangle parametrised by three ratios along the lines through the centre, by the certificate's lane",
  "prior_art": [
    {
      "who": "Girard Desargues",
      "what": "two triangles in perspective from a point are in perspective from a line",
      "where": "published by Abraham Bosse, Maniere universelle de M. Desargues pour pratiquer la perspective (1648), as a proposition attributed to Desargues",
      "year": 1648,
      "attribution": "standard historical attribution; this lane did not consult the primary source"
    }
  ]
}