bitwise and_fn 3 5 = land 3 5

Identifier: F:nat-bitwise-and-eq-land-three-five
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The general bitwise combinator instantiated at Bool.and, applied to 3 and 5, equals the specialized bitwise-AND of 3 and 5.

Formal statement

theorem Nat.bitwise_and_eq_land_three_five : Eq.{1} AxNat (AxNat.bitwise (fun (x0 : Bool) => fun (x1 : Bool) => Bool.rec.{1} (fun (x2 : Bool) => Bool) Bool.false x1 x0) (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero)))))) (AxNat.land (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero))))))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

kernel-Nat.bitwise_and_eq_land_three_five

Kind: kernel-term
Status: checked

Supports: bitwise and_fn 3 5 = land 3 5

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- bitwise_and_eq_land_three_five 2>/dev/null | grep -Ec '^Nat\.bitwise_and_eq_land_three_five[[: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. `and_fn` (`bitwise.rs`) is built inline via a local `Bool.rec`-based select (this prelude declares no top-level `Bool.and`) as `fun a b => if a then b else false`. Both `bitwise and_fn 3 5` and `land 3 5` fully compute (every argument is a concrete numeral) to `1`, from two INDEPENDENTLY constructed `Nat.rec` bodies (`bitwiseAux`'s general per-bit `bool_select_nat (f (beq _ 1) (beq _ 1)) 1 0` step vs `landAux`'s direct `mul` step), so the proof is `Eq.refl` between two terms with no shared head symbol until full reduction -- a genuine, if non-universal, check that the general definition specializes correctly at a witness where `land`'s own sanity check (`F:nat-land-three-five`) already discriminates a wrong-way per-bit step. `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. Anchored with `^Nat\.bitwise_and_eq_land_three_five[[:space:]]` (verified exactly 1 row).

compute-Nat.bitwise_and_eq_land_three_five

Kind: kernel-term
Status: checked

Supports: the specialization holds at (3,5) and at seven other pairs, and is not OR's value

Checker command

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

Evidence notes

`Kernel::def_eq` confirms `bitwise and_fn m n` matches `land m n` exactly over a table of eight pairs including `(0,0)`, `(0,5)`, `(5,0)`, `(1,1)`, `(3,5)`, `(5,3)`, `(6,3)`, `(7,7)` -- not just the one pair this fact pins -- and separately confirms `Nat.bitwise_and_eq_land_three_five`'s ADMITTED TYPE is exactly `Eq (bitwise and_fn 3 5) (land 3 5)`, with a negative control asserting `bitwise and_fn 3 5` does not also def_eq `7` (OR's value at the same operands).

footprint-Nat.bitwise_and_eq_land_three_five

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. Measured with `Nat.bitwise` landed: `nat: axiom=0 opaque=0 quotient=0 total_trusted=0`.

Provenance

{
  "date": "2026-08-28",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane nat-bitwise-general",
  "source": "one of three concrete specialization checks `declare_bitwise_all` (`crates/axeyum-lean-kernel/src/nat_prelude/bitwise.rs`) admits alongside the `Nat.bitwise`/`Nat.bitwiseAux` definitions"
}