every bit at or above a value's own magnitude bound is zero

Identifier: F:nat-testbit-eq-zero-of-lt
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

For every natural n, j: if n < 2^j then testBit(n, j) = 0.

Formal statement

theorem Nat.testBit_eq_zero_of_lt : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat.lt x0 (AxNat.pow (AxNat.succ (AxNat.succ AxNat.zero)) x1)) -> Eq.{1} AxNat (AxNat.testBit x0 x1) AxNat.zero)))

Dependencies

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

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

Evidence

kernel-Nat.testBit_eq_zero_of_lt

Kind: kernel-term
Status: checked

Supports: Nat.testBit_eq_zero_of_lt 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 nat_theorem_inventory -- testBit_eq_zero_of_lt 2>/dev/null | grep -Ec '^Nat\.testBit_eq_zero_of_lt[[:space:]]'

Evidence notes

`build_nat_prelude` admits this theorem only through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type. `nat_theorem_inventory` exits non-zero for a name that does not exist, and `grep -Ec` consumes the pipe so the tested count (expected >= 1) decides the exit status, never `grep -q` under pipefail. Anchored with `[[:space:]]`, never a literal tab. `--release` is mandatory: this tool builds `creal`/`complex`/`cpoint`, which overflow the default debug thread stack.

instance-Nat.testBit_eq_zero_of_lt

Kind: kernel-term
Status: checked

Supports: Applies at a CONCRETE discriminating instance (n := 5 = 101_2, j := size 5 = 3, hypothesis supplied by the already-checked lt_pow_size) confirming the conclusion reduces to Eq (testBit 5 3) zero and NOT Eq (testBit 5 3) one, AND at a genuinely FREE (n, j) pair with a free hypothesis fvar, confirming the declared shape (Eq (testBit n j) zero, not a swapped Eq (testBit j n) zero).

Checker command

cargo test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::test_bit_eq_zero_of_lt_applies_at_a_concrete_instance_and_symbolically

Evidence notes

A `Definition`'s admission alone never proves it computes the right value (this repository's own standing lesson), so this test is the discriminating evidence for what the STATEMENT actually pins down, not merely that some proof term checks.

footprint-Nat.testBit_eq_zero_of_lt

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- the Nat environment admits no trusted declaration

Checker command

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

Evidence notes

Reports `nat: axiom=0 opaque=0 quotient=0 total_trusted=0`, over the FULL trusted surface rather than `Declaration::Axiom` alone. The enumeration is per-environment, not per-theorem; it bounds this theorem's footprint because a proof cannot depend on a trusted declaration the environment does not contain.

Provenance

{
  "date": "2026-08-29",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane nat-msb-exists",
  "source": "theorem name and canonical type read directly via nat_theorem_inventory, which prints render_lean of the admitted type."
}