bitwise combines two bit-appended naturals bit-by-bit, given no leading-zero ambiguity

Identifier: F:nat-bitwise-bit
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every Bool -> Bool -> Bool function f, every Bool a, b and natural m, n: if m = 0 implies a = true, and n = 0 implies b = true, then bitwise(f, bit(a, m), bit(b, n)) = bit(f(a, b), bitwise(f, m, n)).

Formal statement

theorem Nat.bitwise_bit' : ((x0 : ((x0 : Bool) -> ((x1 : Bool) -> Bool))) -> ((x1 : Bool) -> ((x2 : AxNat) -> ((x3 : Bool) -> ((x4 : AxNat) -> ((x5 : ((x5 : Eq.{1} AxNat x2 AxNat.zero) -> Eq.{1} Bool x1 Bool.true)) -> ((x6 : ((x6 : Eq.{1} AxNat x4 AxNat.zero) -> Eq.{1} Bool x3 Bool.true)) -> Eq.{1} AxNat (AxNat.bitwise x0 (AxNat.bit x1 x2) (AxNat.bit x3 x4)) (AxNat.bit (x0 x1 x3) (AxNat.bitwise x0 x2 x4)))))))))

Dependencies

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

4 direct dependencies 0 direct dependents

Evidence

kernel-Nat.bitwise_bit

Kind: kernel-term
Status: checked

Supports: Nat.bitwise_bit' is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

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

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 decides the exit status. Anchored with a literal trailing apostrophe plus `[[:space:]]` (the field separator in the inventory's tab-separated output) so no sibling name can satisfy this row -- verified with `/usr/bin/grep` explicitly, per this repository's own standing warning that `grep` is `ugrep` interactively and the two disagree on escapes. Run `--release` -- the debug build of this inventory example SIGABRTs on stack depth (unrelated to this proof).

compute-Nat.bitwise_bit

Kind: kernel-term
Status: checked

Supports: With f = fst (fun a b => a, deliberately non-commutative) at a = false, m = 2, b = true, n = 3 (a != b, so an argument-order bug in the per-bit combine would be caught; m = 2 is nonzero, so the side hypothesis hm : m = 0 -> a = true is genuinely discharged -- via Nat.succ_ne_zero, since its premise is impossible here, not merely assumed): bitwise(fst, bit(false, 2), bit(true, 3)) = bitwise(fst, 4, 7) = 4, and bit(fst(false, true), bitwise(fst, 2, 3)) = bit(false, 2) = 4. A non-vacuity check confirms the swapped combine bit(fst(true, false), bitwise(fst, 2, 3)) = bit(true, 2) = 5 != 4, so the chosen instance genuinely discriminates argument order.

Checker command

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

Evidence notes

Applies `Nat.bitwise_bit'` at the concrete instance above, confirming both that the admitted type matches `Eq (bitwise fst (bit false 2) (bit true 3)) (bit (fst false true) (bitwise fst 2 3))` and that the value (4) and the swapped-combine control (5) genuinely differ.

footprint-Nat.bitwise_bit

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