bitwise or_fn 3 5 = lor 3 5

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

Recorded description

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

Formal statement

theorem Nat.bitwise_or_eq_lor_three_five : Eq.{1} AxNat (AxNat.bitwise (fun (x0 : Bool) => fun (x1 : Bool) => Bool.rec.{1} (fun (x2 : Bool) => Bool) x1 Bool.true x0) (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero)))))) (AxNat.lor (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_or_eq_lor_three_five

Kind: kernel-term
Status: checked

Supports: bitwise or_fn 3 5 = lor 3 5

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- bitwise_or_eq_lor_three_five 2>/dev/null | grep -Ec '^Nat\.bitwise_or_eq_lor_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. `or_fn` (`bitwise.rs`) is built inline via a local `Bool.rec`-based select (this prelude declares no top-level `Bool.or`) as `fun a b => if a then true else b`. Both `bitwise or_fn 3 5` and `lor 3 5` fully compute (every argument is a concrete numeral) to `7`, from two INDEPENDENTLY constructed `Nat.rec` bodies (`bitwiseAux`'s general per-bit step vs `lorAux`'s direct `max` via `ble`+`bool_select_nat`), so the proof is `Eq.refl` between two terms with no shared head symbol until full reduction. `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_or_eq_lor_three_five[[:space:]]` (verified exactly 1 row).

compute-Nat.bitwise_or_eq_lor_three_five

Kind: kernel-term
Status: checked

Supports: the specialization holds at (3,5) and at seven other pairs, and is not AND'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 or_fn m n` matches `lor 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_or_eq_lor_three_five`'s ADMITTED TYPE is exactly `Eq (bitwise or_fn 3 5) (lor 3 5)`, with a negative control asserting `bitwise or_fn 3 5` does not also def_eq `1` (AND's value at the same operands).

footprint-Nat.bitwise_or_eq_lor_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"
}