the recursive equation for bit-halving recursion at a successor

Identifier: F:nat-binary-rec-succ
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

For any carrier alpha, base value z, step function f, and natural m: binaryRec alpha z f (m+1) = f (bit ((m+1) mod 2 = 1)) ((m+1) / 2) (binaryRec alpha z f ((m+1) / 2)).

Formal statement

theorem Nat.binaryRec_succ : ((x0 : Sort (1)) -> ((x1 : x0) -> ((x2 : ((x2 : Bool) -> ((x3 : AxNat) -> ((x4 : x0) -> x0)))) -> ((x3 : AxNat) -> Eq.{1} x0 (AxNat.binaryRec x0 x1 x2 (AxNat.succ x3)) (x2 (AxNat.beq (AxNat.mod (AxNat.succ x3) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ AxNat.zero)) (AxNat.div (AxNat.succ x3) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.binaryRec x0 x1 x2 (AxNat.div (AxNat.succ x3) (AxNat.succ (AxNat.succ AxNat.zero)))))))))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-Nat.binaryRec_succ

Kind: kernel-term
Status: checked

Supports: Nat.binaryRec_succ 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 -- binaryRec_succ 2>/dev/null | grep -Ec '^Nat\.binaryRec_succ[[:space:]]')" -ge 1

Evidence notes

`grep -Ec` consumes the pipe and the tested COUNT decides the exit status; `nat_theorem_inventory` prints nothing for a name that does not exist. Pattern verified with `/usr/bin/grep` (GNU grep, not the interactive `ugrep` shell function): 1 for `^Nat\.binaryRec_succ[[:space:]]`, 0 for a fabricated sibling name against the same output. `--release` is required; the debug build SIGABRTs building the constructed environment.

compute-binaryRec-round-trip

Kind: kernel-term
Status: checked

Supports: binaryRec 0 (fun b _ acc => bit b acc) n reduces to n at n = 0, 1, 6, 10, 13 -- the definition really performs the bit-halving traversal the equation describes -- with four transposition negative controls.

Checker command

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

Evidence notes

The trusted gate admits a `Definition` on its TYPE, so `Nat.binaryRecAux`'s admission says nothing about what it computes; only evaluation can. Two of these round trips are additionally declared as `Eq.refl` THEOREMS in the prelude (`Nat.binaryRec_rebuilds_thirteen`, `Nat.binaryRec_rebuilds_six`), so the prelude build itself fails if the definition stops computing. Mutation-verified during construction: restating `_rebuilds_thirteen` as `= 11` -- `13 = 0b1101` with its bits reversed -- makes the build fail with `DeclarationValueMismatch`, declared `binaryRec … 13` against inferred `11`. The Rust test repeats that as a live `!def_eq` control, so a traversal consuming the bits in the wrong ORDER is excluded rather than passing by symmetry.

footprint-nat-environment

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