the polar line of a point on a conic is the tangent line there

Identifier: F:geometry-conic-polar-is-tangent
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 Q be a general conic, homogenized to the quadratic form a X^2 + b XY + c Y^2 + d XW + e YW + f W^2, let P0 be a point on it, and let D be a point on the polar line of P0 with respect to Q. Then, writing the conic's value along the line through P0 in direction D as a function of the parameter t, Q(P0 + t*D) = t^2 * Q(D) identically: the value has (at least) a double zero at t=0, which is the algebraic meaning of tangency at P0. NO non-degeneracy condition is required -- not on the conic, which may be singular or even identically zero, and not on the point. The identity is the polarization identity Q(u+v) = Q(u) + 2*B(u,v) + Q(v) with the two hypotheses substituted in, cofactors 1 and 2t: a direct substitution, not a search.

Formal statement

(assert (forall ((dw Real) (dx Real) (dy Real) (p0w Real) (p0x Real) (p0y Real) (qa Real) (qb Real) (qc Real) (qdd Real) (qee Real) (qff Real) (t Real))
  (=> (and (= (+ (* p0w p0x qdd) (* p0w p0y qee) (* p0w p0w qff) (* p0x p0y qb) (* p0x p0x qa) (* p0y p0y qc)) 0.0)
           (= (+ (* dw p0w qff) (* (/ 1.0 2.0) dw p0x qdd) (* (/ 1.0 2.0) dw p0y qee) (* (/ 1.0 2.0) dx p0w qdd) (* dx p0x qa) (* (/ 1.0 2.0) dx p0y qb) (* (/ 1.0 2.0) dy p0w qee) (* (/ 1.0 2.0) dy p0x qb) (* dy p0y qc)) 0.0))
      (= (+ (* 2.0 dw p0w qff t) (* dw p0x qdd t) (* dw p0y qee t) (* dx p0w qdd t) (* 2.0 dx p0x qa t) (* dx p0y qb t) (* dy p0w qee t) (* dy p0x qb t) (* 2.0 dy p0y qc t) (* p0w p0x qdd) (* p0w p0y qee) (* p0w p0w qff) (* p0x p0y qb) (* p0x p0x qa) (* p0y p0y qc)) 0.0))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

geometry-certificate-conic-polar-is-tangent

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

This is the smallest certificate in the geometry corpus and the only one whose cofactors were not searched for at all: they are the constant 1 on the conic hypothesis and 2t on the polar hypothesis, two cofactor terms in total. It is worth having in the ledger for exactly that reason -- it is the boundary case for the tamper controls, since a certificate this small has nowhere for an error to hide, and `cofactors_from_a_neighbouring_certificate_are_rejected` needs a corpus that spans this range of sizes. The six conic coefficients are free variables rather than a fixed conic, so the statement is about EVERY conic, including the degenerate ones.

Provenance

{
  "date": "2026-09-06",
  "established_by": "lane geometry: axeyum_cas::geometry_certify (the cofactors here are written down by the polarization identity rather than searched for) + axeyum_cas::geometry_check (independent re-derivation); this ledger row transcribes the committed certificate",
  "source": "classical; coordinatised in homogeneous coordinates over a general quadratic form by the certificate's lane",
  "prior_art": [
    {
      "who": "classical projective geometry; pole and polar are usually credited to Apollonius in the case of the circle and to Poncelet and Gergonne in general",
      "what": "the polar of a point lying on a conic is the tangent to the conic at that point",
      "where": "standard; see e.g. Coxeter, Projective Geometry (2nd ed., 1974), chapter 6",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}