BX0001 · binary_modulus_nontrivial_nonzeroEvery explicitly guarded modulus m>1 is constructively nonzero.
layer 0 · 13 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.
BX0002 · binary_canonical_residue_existsEvery value has a witnessed canonical residue below every modulus m>1.
layer 1 · 32 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0003 · binary_canonical_residue_functionalTwo canonical residues of the same natural and modulus are equal.
layer 0 · 29 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0004 · binary_canonical_residue_exists_uniqueEach guarded modulus admits exactly one actual bounded residue.
layer 2 · 21 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0005 · binary_exponent_split_existsEvery exponent has an exact half and a witnessed zero-or-one binary digit.
layer 0 · 24 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0006 · binary_exponent_doubled_powerThe relational power at an even exponent is the square of its half power.
layer 0 · 20 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0007 · binary_exponent_odd_powerThe relational power at an odd exponent is its squared half power times the base.
layer 1 · 40 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0008 · binary_modular_square_congruenceSquaring preserves witnessed balanced natural congruence.
layer 0 · 12 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0009 · binary_modular_multiply_congruenceMultiplication preserves both witnessed modular factors.
layer 0 · 15 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX000A · binary_modular_square_residue_existsEvery squaring step has an actual canonical modular residue.
layer 2 · 7 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX000B · binary_modular_multiply_residue_existsEvery multiplication step has an actual canonical modular residue.
layer 2 · 8 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX000C · binary_modular_step_existsEvery guarded square-and-optional-multiply binary transition has a canonical result.
layer 2 · 29 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX000D · binary_modular_step_functionalA fixed binary digit and state determine exactly one modular transition result.
layer 1 · 41 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX000E · binary_modular_exponentiation_result_existsEvery a,e and every modulus m>1 have an exact bounded residue of the relational power a^e.
layer 2 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX000F · binary_modular_exponentiation_result_functionalAny two exact bounded residues of the same relational power are equal.
layer 1 · 27 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBX0010 · binary_modular_exponentiation_result_exists_uniqueEvery guarded modular exponentiation has exactly one actual canonical natural result.
layer 3 · 24 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 16 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.