Polarization identity for the sum of two points

Identifier: F:cpoint-dot-self-add
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For points a, b of the constructed plane, dot(a+b, a+b) is CReal.Equiv-equivalent to dot(a,a) + dot(a,b) + dot(a,b) + dot(b,b) -- the expansion half of the polarization identity, and (with F:cpoint-dot-self-sub) the pair that F:cpoint-parallelogram-law is built from.

Formal statement

theorem CPoint.dot_self_add : ((x0 : CPoint) -> ((x1 : CPoint) -> CReal.Equiv (CPoint.dot (CPoint.add x0 x1) (CPoint.add x0 x1)) (CReal.add (CPoint.dot x0 x0) (CReal.add (CPoint.dot x0 x1) (CReal.add (CPoint.dot x0 x1) (CPoint.dot x1 x1))))))

Dependencies

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

7 direct dependencies 9 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CPoint.dot_self_add

Kind: kernel-term
Status: checked

Supports: CPoint.dot_self_add 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.dot_self_add 2>/dev/null | grep -cE '^CPoint\.dot_self_add[[:space:]]'

Evidence notes

`build_cpoint_prelude` admits CPoint.dot_self_add 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.dot_self_add

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- CPoint.dot_self_add'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\.dot_self_add[[: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."
}