Pascal's theorem on a parabola: the three diagonal points of an inscribed hexagon are collinear

Identifier: F:geometry-pascal-parabola-hexagon
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

Let A=(a,a^2), B=(b,b^2), C=(c,c^2), D=(d,d^2), E=(e,e^2), F=(f,f^2) be six points of the parabola y = x^2, given by their parameters, and let the line through the parabola points at parameters t and u be the homogeneous triple L(t,u) = (-(t+u), 1, tu), whose incidence relation Y - (t+u)X + tuW = 0 is the chord when t and u differ and the tangent when they coincide. Let X, Y and Z be the homogeneous points L(a,b) x L(d,e), L(b,c) x L(e,f) and L(c,d) x L(f,a) -- the standard projective meet, which lies on both of its lines because L.(L x M) and M.(L x M) are identically zero. Then X, Y and Z are collinear, i.e. the 3x3 determinant of their homogeneous coordinates vanishes. NO non-degeneracy condition is used or needed: the conclusion lies in the plain hypothesis ideal, a pair of parallel opposite sides meets at the ordinary point at infinity of their common direction, and a diagonal point degenerating to the zero vector satisfies the conclusion. Collinearity is scale-invariant, so the statement transfers to any other representatives of the same projective points. The conic hypothesis is discharged by the parametrisation rather than assumed: every configuration of six points on THIS conic is covered, and the statement for an arbitrary conic follows by projective equivalence, which is NOT part of this certificate and is not claimed here.

Formal statement

(assert (forall ((ta Real) (tb Real) (tc Real) (td Real) (te Real) (tf Real) (xw Real) (xx Real) (xy Real) (yw Real) (yx Real) (yy Real) (zw Real) (zx Real) (zy Real))
  (=> (and (= (+ (* ta tb) xx) (* td te))
           (= (+ (* ta tb td) (* ta tb te) xy) (+ (* ta td te) (* tb td te)))
           (= (+ ta tb xw) (+ td te))
           (= (+ (* tb tc) yx) (* te tf))
           (= (+ (* tb tc te) (* tb tc tf) yy) (+ (* tb te tf) (* tc te tf)))
           (= (+ tb tc yw) (+ te tf))
           (= (+ (* tc td) zx) (* ta tf))
           (= (+ (* ta tc td) (* tc td tf) zy) (+ (* ta tc tf) (* ta td tf)))
           (= (+ tc td zw) (+ ta tf)))
      (= (+ (* xw yx zy) (* xx yy zw) (* xy yw zx)) (+ (* xw yy zx) (* xx yw zy) (* xy yx zw))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

geometry-certificate-pascal-parabola-hexagon

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 carries no saturations, so this fact's `axiom_footprint` lists no non-degeneracy entry: the collinearity is a member of the plain ideal generated by the nine incidence hypotheses. The parallel-sides configuration is committed as a GENERIC witness rather than a degenerate one, which is the precise sense in which the projective reading removes the side condition that the affine reading of Pascal would need.

Provenance

{
  "date": "2026-09-06",
  "established_by": "lane geometry: axeyum_cas::geometry_certify (untrusted cofactor-tracked search) + axeyum_cas::geometry_check (independent re-derivation); this ledger row transcribes the committed certificate",
  "source": "classical; coordinatised on the parabola y = x^2 by the certificate's lane",
  "prior_art": [
    {
      "who": "Blaise Pascal",
      "what": "the three points of intersection of the opposite sides of a hexagon inscribed in a conic are collinear (the hexagrammum mysticum)",
      "where": "Essai pour les coniques (1640); the theorem itself survives only through Leibniz's copy of the lost manuscript",
      "year": 1640,
      "attribution": "standard historical attribution; this lane did not consult the primary source"
    }
  ]
}