BL0001 binary_length_digit_boundedEvery witnessed binary digit is strictly below two.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableCurrent library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
BL0002 binary_length_digit_split_existsEvery natural number has an exact binary quotient and zero-or-one digit.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0003 binary_length_digit_split_functionalBinary division by two has a unique quotient and unique digit.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0004 binary_length_digit_split_exists_uniqueEvery natural has exactly one fully witnessed binary quotient/digit pair.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0005 binary_power_two_existsEvery natural exponent has a witnessed beta-coded power of two.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0006 binary_power_two_functionalThe relational power of two is functional at every exponent.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0007 binary_power_two_zero_valueThe beta-coded zeroth power of two is exactly one.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0008 binary_power_two_nonzeroEvery beta-coded power of two is constructively nonzero.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0009 binary_power_two_successor_doubleA successor power of two is exactly the sum of two predecessor powers.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL000A binary_power_two_strict_growthSuccessive beta-coded powers of two grow strictly.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL000B binary_power_two_exponent_monotoneThe relational powers of two preserve non-strict exponent ordering.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL000C binary_power_two_exponent_strictStrictly ordered exponents have strictly ordered powers of two.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL000D binary_length_zeroThe blueprint convention gives zero exactly one displayed binary digit.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL000E binary_length_oneThe positive integer one has exactly one binary digit.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL000F binary_length_zero_input_valueAny binary-length witness for zero is necessarily one.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0010 binary_length_successor_stepA binary-length witness for n constructively produces one for S n.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0011 binary_length_existsEvery natural number has a constructively witnessed canonical bit length.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0012 binary_length_zero_input_generalAny canonical bit-length witness at an input equal to zero is one.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0013 binary_length_functionalTwo complete constructive binary-length witnesses for one input agree.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0014 binary_length_exists_uniqueEvery natural has exactly one canonical blueprint-compatible bit length.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StableBL0015 binary_length_power_exactThe exact beta-coded power 2^e has canonical binary length e+1.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not StablePD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0014 Product(b,c,l,z)z is the product of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0019 Repeat(b,c,a,l)The decoded prefix repeats a for l positions.
Conservative definition · notation layer 1PD0020 Pow(a,e,z)z is the relational e-th power of a.
Conservative definition · notation layer 2ND0028 PowTwo(e,p)The exact existing constructive exponentiation relation Pow(2,e,p).
Conservative definition · notation layer 3ND0022 BinaryExponentSplit(e,h,b)The exact binary decomposition e=2*h+b with an explicit b=0 or b=1 witness.
Conservative definition · notation layer 0ND0029 BinaryDigit(n,h,b)An exact binary digit split n=2h+b, with b explicitly zero or one.
Conservative definition · notation layer 1PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0ND0030 BitLen(n,ell)The unique binary length, with BitLen(0,1) and positive bounds 2^(ell-1)≤n<2^ell.
Conservative definition · notation layer 4Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.