bit-i disagreement plus agreement above i forces the order

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

Recorded description

For every natural n, m, i: if testBit(n, i) = 0, testBit(m, i) = 1, and testBit(n, j) = testBit(m, j) for every j > i, then n < m.

Formal statement

theorem Nat.lt_of_testBit : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : Eq.{1} AxNat (AxNat.testBit x0 x2) AxNat.zero) -> ((x4 : Eq.{1} AxNat (AxNat.testBit x1 x2) (AxNat.succ AxNat.zero)) -> ((x5 : ((x5 : AxNat) -> ((x6 : AxNat.lt x2 x5) -> Eq.{1} AxNat (AxNat.testBit x0 x5) (AxNat.testBit x1 x5)))) -> AxNat.lt x0 x1))))))

Dependencies

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

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

Evidence

kernel-Nat.lt_of_testBit

Kind: kernel-term
Status: checked

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

shape-Nat.lt_of_testBit

Kind: kernel-term
Status: checked

Supports: The declared type's exact SHAPE (hypothesis order, that H0 is about n not m, that H1's target is one not zero, that the conclusion is Lt n m not Lt m n) is confirmed by applying it to a genuinely free (n, m, i, H0, H1, Hagree) tuple, wrapped in a fresh theorem so the free variables are properly registered via pi_fv/lam_fv.

Checker command

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

Evidence notes

A concrete DISCRIMINATING numeric instance was scoped out of this test: building one honestly needs Hagree's full universally-quantified proof (forall j, i < j -> ...), which requires a general "testBit is eventually zero above a magnitude bound" lemma this lane did not build (see docs/plan/status/265-nat-msb-order.md). The kernel's own admission of the full universally-quantified statement is strictly stronger evidence than any single concrete instantiation would be; this test additionally confirms the shape.

footprint-Nat.lt_of_testBit

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-order",
  "source": "theorem name and canonical type read directly via nat_theorem_inventory, which prints render_lean of the admitted type."
}