BL0001 · binary_length_digit_boundedEvery witnessed binary digit is strictly below two.
layer 0 · 9 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.
layer 0 · 3 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0003 · binary_length_digit_split_functionalBinary division by two has a unique quotient and unique digit.
layer 1 · 42 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0004 · binary_length_digit_split_exists_uniqueEvery natural has exactly one fully witnessed binary quotient/digit pair.
layer 2 · 19 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0005 · binary_power_two_existsEvery natural exponent has a witnessed beta-coded power of two.
layer 0 · 4 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0006 · binary_power_two_functionalThe relational power of two is functional at every exponent.
layer 0 · 12 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0007 · binary_power_two_zero_valueThe beta-coded zeroth power of two is exactly one.
layer 0 · 8 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0008 · binary_power_two_nonzeroEvery beta-coded power of two is constructively nonzero.
layer 0 · 12 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0009 · binary_power_two_successor_doubleA successor power of two is exactly the sum of two predecessor powers.
layer 0 · 20 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL000A · binary_power_two_strict_growthSuccessive beta-coded powers of two grow strictly.
layer 1 · 31 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL000B · binary_power_two_exponent_monotoneThe relational powers of two preserve non-strict exponent ordering.
layer 0 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL000C · binary_power_two_exponent_strictStrictly ordered exponents have strictly ordered powers of two.
layer 2 · 33 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL000D · binary_length_zeroThe blueprint convention gives zero exactly one displayed binary digit.
layer 0 · 4 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL000E · binary_length_oneThe positive integer one has exactly one binary digit.
layer 1 · 41 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL000F · binary_length_zero_input_valueAny binary-length witness for zero is necessarily one.
layer 0 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0010 · binary_length_successor_stepA binary-length witness for n constructively produces one for S n.
layer 2 · 75 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0011 · binary_length_existsEvery natural number has a constructively witnessed canonical bit length.
layer 3 · 8 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0012 · binary_length_zero_input_generalAny canonical bit-length witness at an input equal to zero is one.
layer 1 · 11 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0013 · binary_length_functionalTwo complete constructive binary-length witnesses for one input agree.
layer 2 · 120 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0014 · binary_length_exists_uniqueEvery natural has exactly one canonical blueprint-compatible bit length.
layer 4 · 14 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBL0015 · binary_length_power_exactThe exact beta-coded power 2^e has canonical binary length e+1.
layer 2 · 40 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 21 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.