The decided rational zero test implies the propositional one: isZeroB x = true entails x = 0

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

Recorded description

For every x : Rat, Rat.isZeroB x = Bool.true implies Eq Rat x Rat.zero, where Rat.isZeroB x is the total Bool-valued test 'if Rat.ble x 0 then Rat.ble 0 x else false'. This is the bridge from the COMPUTED zero test that row reduction branches on to the propositional equation every field law consumes, and it is the one place the decidability of the rational order is actually spent. The proof splits on Rat.ble x 0: its true branch reduces isZeroB x to the second comparison, so the hypothesis becomes Rat.ble 0 x = true and Rat.le_antisymm closes it from two applications of Rat.le_of_ble_eq_true; its false branch reduces isZeroB x to Bool.false, contradicting the hypothesis. A Prop-valued Eq x 0 cannot drive a computation, which is why the definition needed a Bool test in the first place.

Formal statement

theorem Rat.eq_zero_of_isZeroB : ((x0 : Rat) -> ((x1 : Eq.{1} Bool (Rat.isZeroB x0) Bool.true) -> Eq.{1} Rat x0 Rat.zero))

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

rat-eq-zero-of-is-zero-b-1

Kind: kernel-term
Status: checked

Supports: `Rat.eq_zero_of_isZeroB` 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 hypothesis is an equation at `Bool` between `Rat.isZeroB x0` and `Bool.true` and the conclusion an equation at `Rat` -- the two different types are the whole content of the bridge, and a paraphrase that said `x is zero` on both sides would lose it.

Checker command

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

Evidence notes

Run 2026-09-02: prints four `found ... theorem Rat.eq_zero_of_isZeroB 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"
}