The squared distance from a point to a linear interpolation of two other points, expanded

Identifier: F:cpoint-lerp-dist-sq
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For points x0, x1, x2 of the constructed plane and a scalar x3, distSq(x0, lerp(x1, x2, x3)) is CReal.Equiv-equivalent to distSq(x0, x1) - 2*x3*dot(x0 - x1, x2 - x1) + x3*x3*distSq(x1, x2) -- the algebraic expansion Stewart's theorem is built from.

Formal statement

theorem CPoint.lerp_dist_sq : ((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : CPoint) -> ((x3 : CReal) -> CReal.Equiv (CPoint.distSq x0 (CPoint.lerp x1 x2 x3)) (CReal.add (CPoint.distSq x0 x1) (CReal.add (CReal.neg (CReal.mul x3 (CPoint.dot (CPoint.sub x0 x1) (CPoint.sub x2 x1)))) (CReal.add (CReal.neg (CReal.mul x3 (CPoint.dot (CPoint.sub x0 x1) (CPoint.sub x2 x1)))) (CReal.mul x3 (CReal.mul x3 (CPoint.distSq x1 x2))))))))))

Dependencies

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

17 direct dependencies 2 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CPoint.lerp_dist_sq

Kind: kernel-term
Status: checked

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

Evidence notes

`build_cpoint_prelude` admits CPoint.lerp_dist_sq 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 in one run; 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).

footprint-CPoint.lerp_dist_sq

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the cpoint prelude's trusted surface is empty, which bounds CPoint.lerp_dist_sq

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed --require-axiom-free cpoint

Evidence notes

`nat_axiom_inventory --include-constructed --require-axiom-free cpoint` builds the cpoint environment as its own group and reports `cpoint: axiom=0 opaque=0 quotient=0 total_trusted=0` (re-measured on this tree), covering Axiom, Opaque AND Quotient, not just Declaration::Axiom -- this bounds every individual cpoint theorem's footprint by []. `--include-constructed` is REQUIRED: without it the command exits 1 naming `cpoint` as known but not built this run rather than a silent pass, which is the standing trap of an empty/absent result reading as a strong negative when the tool was never pointed at the subject. `nat_axiom_inventory` now covers `cpoint` directly (re-verified on this tree: `--require-axiom-free cpoint` exits 0 with `cpoint: axiom=0 opaque=0 quotient=0 total_trusted=0`), so the footprint_closure_audit fallback some earlier CPoint facts used is not needed here. `--release` is MANDATORY for the same deep-recursion reason as `theorem_dependency_inventory` (measured on this tree: debug SIGABRTs at 134).

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 and top-level binder arity 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(), expr_node()) -- no in-tree example prints Complex/CPoint theorem types; crates/ source was not touched to produce this batch; the probe was built and run in the session scratchpad and deleted after use."
}