Lagrange's identity in two dimensions

Identifier: F:cpoint-lagrange-identity
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For constructed reals x0, x1, x2, x3, (x0^2 + x1^2)*(x2^2 + x3^2) - (x0*x2 + x1*x3)^2 is CReal.Equiv-equivalent to (x0*x3 - x1*x2)^2 -- the coordinate identity that turns the Cauchy-Schwarz gap into a single squared cross term (x0*x3 - x1*x2 is the 2D cross/determinant of (x0,x1) and (x2,x3)), and the algebraic engine behind why equality in F:cpoint-cauchy-schwarz forces collinearity.

Formal statement

theorem CPoint.lagrange_identity : ((x0 : CReal) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : CReal) -> CReal.Equiv (CReal.add (CReal.mul (CReal.add (CReal.mul x0 x0) (CReal.mul x1 x1)) (CReal.add (CReal.mul x2 x2) (CReal.mul x3 x3))) (CReal.neg (CReal.mul (CReal.add (CReal.mul x0 x2) (CReal.mul x1 x3)) (CReal.add (CReal.mul x0 x2) (CReal.mul x1 x3))))) (CReal.mul (CReal.add (CReal.mul x0 x3) (CReal.neg (CReal.mul x1 x2))) (CReal.add (CReal.mul x0 x3) (CReal.neg (CReal.mul x1 x2))))))))

Dependencies

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

16 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CPoint.lagrange_identity

Kind: kernel-term
Status: checked

Supports: CPoint.lagrange_identity is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- CPoint.lagrange_identity 2>/dev/null | grep -cE '^CPoint\.lagrange_identity[[:space:]]'

Evidence notes

`build_cpoint_prelude` admits CPoint.lagrange_identity through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so a line in this tool's output for the exact name is a machine-checked proof having been admitted. `theorem_dependency_inventory` builds creal/complex/cpoint (extended 2026-08-25); it exits non-zero for a named filter that matches nothing, and `grep -c` (never `-q`) independently asserts the exact tab-anchored line is present. `--release` is MANDATORY: building the constructed carriers recurses deep enough in a debug build to overflow the default thread stack (measured on this tree: release exits 0, debug SIGABRTs at 134) -- the same resource-limit gotcha documented for `prelude_theorem_inventory --include-constructed`.

footprint-CPoint.lagrange_identity

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- CPoint.lagrange_identity's narrow AND widened trusted-declaration closure is empty

Checker command

cargo run -q --release -p axeyum-lean-kernel --example footprint_closure_audit -- --include-constructed 2>/dev/null | grep -cE '^cpoint[[:space:]]CPoint\.lagrange_identity[[:space:]][^[:space:]]*[[:space:]]0[[:space:]][[:space:]][[:space:]]0[[:space:]]$'

Evidence notes

`nat_axiom_inventory` does NOT cover `cpoint` at all (verified: `--include-constructed --require-axiom-free cpoint` errors '"cpoint" is not enumerated by this run (known: ... creal, complex)' -- cpoint was never added to that tool's group list, an empty/absent-coverage trap in its own right). `footprint_closure_audit --include-constructed` DOES build a `cpoint` group (verified in its `build_groups`) and, per admitted theorem, emits a row `cpoint<TAB>NAME<TAB>narrow_kinds<TAB>narrow_dangling<TAB>narrow_trusted<TAB>widened_trusted<TAB>widened_dangling<TAB>inductive_edge_diffs`. An axiom-free theorem has narrow_dangling=0, narrow_trusted empty, widened_trusted empty (the WIDENED closure additionally walks inductive constructor/recursor types one step further than `render_deps`, so this is stronger than the narrow-only check the `nat_axiom_inventory`-style facts use), widened_dangling=0, and no inductive edge diff -- the anchored regex below requires all of that in one line. `--include-constructed` is REQUIRED: without it the cpoint group is never built and BOTH the row-match and the `cpoint: theorems=` coverage line are absent (verified: 0 matches for either, vs 1 for both with the flag), which is the same coverage trap CLAUDE.md already documents for `nat_axiom_inventory`. `--release` is MANDATORY for the same deep-recursion reason as `theorem_dependency_inventory` (this tool's own doc example uses it); measured full-audit wall time on this tree ~20s release.

Provenance

{
  "date": "2026-08-25",
  "established_by": "axeyum-lean-kernel build_cpoint_prelude",
  "source": "theorem name and dependency edges from theorem_dependency_inventory (builds creal/complex/cpoint); canonical type read via a standalone probe binary depending on axeyum-lean-kernel by path, calling only its public Kernel API (environment(), display_name(), render_lean(), axiom_footprint()) -- no in-tree example prints Complex/CPoint theorem types; crates/ source was not touched to produce this batch."
}