The boolean order test is false above its bound

Identifier: F:nat-ble-eq-false-of-lt
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all b and n, if n < b then the boolean test `ble b n` is false.

Formal statement

theorem Nat.ble_eq_false_of_lt : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat.lt x1 x0) -> Eq.{1} Bool (AxNat.ble x0 x1) Bool.false)))

Dependencies

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

4 direct dependencies 8 direct dependents

Evidence

kernel-Nat.ble_eq_false_of_lt

Kind: kernel-term
Status: checked

Supports: For all b and n, if n < b then the boolean test `ble b n` is false.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- ble_eq_false_of_lt 2>/dev/null | grep -Ec '^Nat\.ble_eq_false_of_lt[[:space:]]')" -ge 1

Evidence notes

`build_nat_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so producing this row at all is a machine-checked proof. The NEGATIVE half of the `Nat.ble`/`Nat.le` bridge, which the prelude did not have: `ble.rs` carries the two positive directions (`ble_eq_true_of_le`, `le_of_ble_eq_true`) and the negated-`Prop` form (`not_le_of_not_ble_eq_true`), but nothing producing `Eq Bool _ Bool.false` -- which is the only shape that can rewrite a `Bool.rec` cut. Proved by `Bool` excluded middle on `ble b n` (`bool_true_or_false`): the `true` branch gives `b <= n` by `le_of_ble_eq_true`, which with `n < b` gives `n < n` through `lt_of_lt_of_le` and is refuted by `lt_irrefl`; the `false` branch is the goal already. Declared in `log.rs` under its first consumer, which is the retrieval hazard this repository keeps paying for -- it is recorded here so the next lane needing it can find it. `nat_theorem_inventory` exits non-zero for a name that does not exist, and `grep -Ec` consumes the pipe and the count is tested, so the exit status depends on what the run found.

footprint-Nat.ble_eq_false_of_lt

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

`nat_axiom_inventory --require-axiom-free nat` enumerates the built Nat environment and exits non-zero unless it admits no Axiom, Opaque or Quotient declaration. This matters more than usual here: Mathlib's `Nat.log` is defined by WELL-FOUNDED recursion on `n / b`, and the Lean equation compiler's route to that carries `Quot.sound`/`propext`. The fuel-based structural definition in `nat_prelude/log.rs` was chosen so that this row stays empty, and this command is what makes the claim falsifiable rather than asserted.

Provenance

{
  "date": "2026-08-28",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane 199-nat-log",
  "source": "declared by `declare_log_all` (`crates/axeyum-lean-kernel/src/nat_prelude/log.rs`) alongside the `Nat.logAux`/`Nat.log` definitions"
}