Ceva's theorem, sufficiency direction

Identifier: F:cpoint-ceva-concurrent-of-ratio-product
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For a triangle with vertices x0, x1, x2 of the constructed plane and cevian ratios x3, x4, x5 (each in (0,1), defining points on sides x0x1, x1x2, x2x0 via lerp) satisfying a nondegeneracy witness and the normalized ratio-product condition x3*x4*x5 = (1-x3)*(1-x4)*(1-x5) (Ceva's relation), the three cevians are concurrent: the point on the first cevian at the appropriate parameter, the point on the second at its parameter, and the point on the third at its parameter all coincide (CPoint.Equiv, pairwise). The sufficiency half of Ceva's theorem -- the ratio-product condition implies concurrency.

Formal statement

theorem CPoint.ceva_concurrent_of_ratio_product : ((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : CPoint) -> ((x3 : CReal) -> ((x4 : CReal) -> ((x5 : CReal) -> ((x6 : AxNat) -> ((x7 : CReal.PosBound (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4))) x6) -> ((x8 : CReal.Equiv (CReal.mul x3 (CReal.mul x4 x5)) (CReal.mul (CReal.add CReal.one (CReal.neg x3)) (CReal.mul (CReal.add CReal.one (CReal.neg x4)) (CReal.add CReal.one (CReal.neg x5))))) -> And (CPoint.Equiv (CPoint.lerp x0 (CPoint.lerp x1 x2 x3) (CReal.mul (CReal.add CReal.one (CReal.neg x4)) (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.inv (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4))) x6 x7)))) (CPoint.lerp x1 (CPoint.lerp x2 x0 x4) (CReal.mul x3 (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.inv (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4))) x6 x7))))) (CPoint.Equiv (CPoint.lerp x1 (CPoint.lerp x2 x0 x4) (CReal.mul x3 (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.inv (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4))) x6 x7)))) (CPoint.lerp x2 (CPoint.lerp x0 x1 x5) (CReal.mul (CReal.add (CReal.add (CReal.add CReal.one (CReal.neg x3)) (CReal.neg x4)) (CReal.add (CReal.mul x3 x4) (CReal.mul x3 x4))) (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.inv (CReal.mul (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4)) (CReal.add (CReal.add CReal.one (CReal.neg x4)) (CReal.mul x3 x4))) x6 x7))))))))))))))

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.ceva_concurrent_of_ratio_product

Kind: kernel-term
Status: checked

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

Evidence notes

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

Kind: exhaustive-enumeration
Status: checked

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