Stewart's theorem

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

Recorded description

For points a, b, c of the constructed plane and a constructed real t, let p = lerp(b, c, t) be the point dividing segment bc in ratio t (p = b + t*(c-b)). Then distSq(a,p) + t*(1-t)*distSq(b,c) is CReal.Equiv-equivalent to (1-t)*distSq(a,b) + t*distSq(a,c) -- Stewart's theorem, relating a cevian's length to the two sides it splits and the ratio it splits them in.

Formal statement

theorem CPoint.stewart : ((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : CPoint) -> ((x3 : CReal) -> CReal.Equiv (CReal.add (CPoint.distSq x0 (CPoint.lerp x1 x2 x3)) (CReal.mul x3 (CReal.mul (CReal.add CReal.one (CReal.neg x3)) (CPoint.distSq x1 x2)))) (CReal.add (CReal.mul (CReal.add CReal.one (CReal.neg x3)) (CPoint.distSq x0 x1)) (CReal.mul x3 (CPoint.distSq x0 x2)))))))

Dependencies

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

19 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CPoint.stewart

Kind: kernel-term
Status: checked

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

Evidence notes

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

Kind: exhaustive-enumeration
Status: checked

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