The conic discriminant is invariant under a rotation of the plane

Identifier: F:conic-discriminant-invariant-under-rotation
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

A conic on the real plane is the six-coefficient datum (A,B,C,D,E,F) whose zero set is the points where A x^2 + B x y + C y^2 + D x + E y + F ~ 0. A rotation by the pair (c,s) with c^2 + s^2 ~ 1 acts on that datum by CPoint.Conic.rotate, and the discriminant B^2 - 4AC of the rotated conic is CReal.Equiv to the discriminant of the original. The unconditional form, proved first and stated separately as CPoint.Conic.discriminant_rotate, carries no hypothesis at all: the discriminant picks up exactly the factor (c^2 + s^2)^2 for EVERY (c,s), because the linear map behind the action has determinant c^2 + s^2 and the discriminant is -4 det Q for the quadratic-part matrix Q, which transforms as M^T Q M. The reflection CPoint.Conic.reflect gets the SAME factor -- its determinant is -(c^2 + s^2) and the discriminant sees only the square -- so orientation reversal is invisible to the classification, which is the correct answer since a reflection does not turn an ellipse into a hyperbola. A translation needs no hypothesis at all and its discriminant law is proved by CReal.Equiv.refl, because a translation copies A, B and C unchanged.

Formal statement

theorem CPoint.Conic.discriminant_rotate_unit : ((x0 : CReal) -> ((x1 : CReal) -> ((x2 : CReal.Equiv (CReal.add (CReal.mul x0 x0) (CReal.mul x1 x1)) CReal.one) -> ((x3 : CPoint.Conic) -> CReal.Equiv (CPoint.Conic.discriminant (CPoint.Conic.rotate x0 x1 x3)) (CPoint.Conic.discriminant x3)))))

Dependencies

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

6 direct dependencies 0 direct dependents

Evidence

kernel-CPoint.Conic.discriminant_rotate_unit

Kind: kernel-term
Status: checked

Supports: CPoint.Conic.discriminant_rotate_unit is admitted by the trusted kernel gate with the type recorded in formal.statement, and Kernel::axiom_footprint reports 0 assumed names.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example cpoint_theorem_inventory -- discriminant_rotate_unit

Evidence notes

--release is mandatory: the CReal/CPoint preludes underneath recurse deep enough that the debug kernel is measured up to 32x slower on proof terms of this size. A filter matching zero declarations exits non-zero (an absent declaration is a failure, not an empty report), the same discipline nat_theorem_inventory and metric_prod_theorem_inventory use.

suite-every_theorem_here_is_axiom_free

Kind: exhaustive-enumeration
Status: checked

Supports: Every CPoint declaration live in the prelude -- all 56 this lane adds included -- has an empty Kernel::axiom_footprint. The test's coverage half enumerates the ENVIRONMENT and fails on any CPoint-prefixed name absent from its list, so a new declaration cannot escape it by being forgotten.

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- creal_point::creal_point_tests::every_theorem_here_is_axiom_free --test-threads=1 2>&1 | grep -cE '^test result: ok\. 1 passed'

Evidence notes

`cargo test -- <filter>` runs ZERO tests and exits 0 when the filter matches nothing, so the exact `1 passed` count is load-bearing, not the exit status alone. --release avoids the debug-build stack overflow the CReal/CPoint preludes are already documented as needing.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_cpoint_prelude, creal_point/conic.rs (declare_discriminant_action_units)",
  "source": "Lane `conics`, roadmap W3-9. ADR-1641. formal.statement is Kernel::render_lean of the declaration's type, taken verbatim from this lane's cpoint_theorem_inventory example."
}