A rational the decided test calls nonzero is nonzero propositionally

Identifier: F:rat-ne-zero-of-is-zero-b-false
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For every x : Rat, Rat.isZeroB x = Bool.false implies Not (Eq Rat x Rat.zero). This is the direction a FOUND pivot arrives in: Rat.pivotSearch returns an index precisely because Rat.isZeroB said false at that entry, and every field law that would then divide by it -- Rat.mul_inv_cancel_of_ne_zero above all -- wants Not (Eq x 0). The proof moves the hypothesis to x := 0 along the assumed equation and contradicts Rat.isZeroB_zero, which is Eq.refl because Rat.zero is built with Rat.mk so both projections compute and Rat.ble decides by cross-multiplication into Int.ble.

Formal statement

theorem Rat.ne_zero_of_isZeroB_false : ((x0 : Rat) -> ((x1 : Eq.{1} Bool (Rat.isZeroB x0) Bool.false) -> ((x2 : Eq.{1} Rat x0 Rat.zero) -> False)))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

rat-ne-zero-of-is-zero-b-false-1

Kind: kernel-term
Status: checked

Supports: `Rat.ne_zero_of_isZeroB_false` is a checked `Declaration::Theorem` with an EMPTY `Kernel::axiom_footprint` in all four preludes carrying the rationals. The `formal.statement` is the kernel's `render_lean` of the admitted type; reading it confirms the conclusion is spelled out as `(Eq Rat x0 Rat.zero) -> False` rather than through a `Not` abbreviation, which is what a consumer has to match against.

Checker command

out=$(target/release/examples/kernel_declaration_projection --require-declaration Rat.ne_zero_of_isZeroB_false --require-kind theorem 2>&1) && test "$(printf "%s\n" "$out" | grep -cE 'found[[:space:]]+(rat|creal|complex|cpoint)[[:space:]]+theorem[[:space:]]+Rat\.ne_zero_of_isZeroB_false[[:space:]]+0$')" = 4

Evidence notes

Run 2026-09-02: prints four `found ... theorem Rat.ne_zero_of_isZeroB_false 0` rows (rat, creal, complex, cpoint) and exits 0. The checker COUNTS those rows and requires exactly 4, so a deletion, a rename, a demotion to a `Definition`, a nonzero axiom footprint, or the declaration failing to survive into a downstream prelude each make the count differ and the command exit 1. `scripts/new-fact.py` verified the pattern fails on mutated output before this file was written.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/echelon.rs)",
  "source": "docs/research/09-decisions/adr-1554-the-pivot-is-computed-not-extracted-and-the-fuel-is-exact.md"
}