The centroid vector identity anchoring the Euler line

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

Recorded description

For any basepoint x0 and triangle vertices x1, x2, x3 of the constructed plane, ((x1+x2+x3) - (x0+x0)) + (x0+x0) is CPoint.Equiv-equivalent to centroid(x1,x2,x3) + centroid(x1,x2,x3) + centroid(x1,x2,x3) -- i.e. x1+x2+x3 = 3*centroid(x1,x2,x3), the affine identity (stated relative to an arbitrary basepoint so it type-checks without assuming a canonical origin on CPoint) that the Euler line construction is built from. NOT the collinearity statement itself (centroid/circumcentre/orthocentre collinear) -- that would combine this with F:cpoint-cross-annihilates-difference-style lemmas not in this batch; this fact is the vector identity the construction anchors on.

Formal statement

theorem CPoint.euler_line : ((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : CPoint) -> ((x3 : CPoint) -> CPoint.Equiv (CPoint.add (CPoint.sub (CPoint.add (CPoint.add x1 x2) x3) (CPoint.add x0 x0)) (CPoint.add x0 x0)) (CPoint.add (CPoint.add (CPoint.centroid x1 x2 x3) (CPoint.centroid x1 x2 x3)) (CPoint.centroid x1 x2 x3))))))

Dependencies

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

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

Evidence

kernel-CPoint.euler_line

Kind: kernel-term
Status: checked

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

Evidence notes

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

Kind: exhaustive-enumeration
Status: checked

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