BX0001 binary_modulus_nontrivial_nonzeroEvery explicitly guarded modulus m>1 is constructively nonzero.
Alpha v34 checked-use · first admitted v21 · 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.
BX0002 binary_canonical_residue_existsEvery value has a witnessed canonical residue below every modulus m>1.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0003 binary_canonical_residue_functionalTwo canonical residues of the same natural and modulus are equal.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0004 binary_canonical_residue_exists_uniqueEach guarded modulus admits exactly one actual bounded residue.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0005 binary_exponent_split_existsEvery exponent has an exact half and a witnessed zero-or-one binary digit.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0006 binary_exponent_doubled_powerThe relational power at an even exponent is the square of its half power.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0007 binary_exponent_odd_powerThe relational power at an odd exponent is its squared half power times the base.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0008 binary_modular_square_congruenceSquaring preserves witnessed balanced natural congruence.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0009 binary_modular_multiply_congruenceMultiplication preserves both witnessed modular factors.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX000A binary_modular_square_residue_existsEvery squaring step has an actual canonical modular residue.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX000B binary_modular_multiply_residue_existsEvery multiplication step has an actual canonical modular residue.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX000C binary_modular_step_existsEvery guarded square-and-optional-multiply binary transition has a canonical result.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX000D binary_modular_step_functionalA fixed binary digit and state determine exactly one modular transition result.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; 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.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX000F binary_modular_exponentiation_result_functionalAny two exact bounded residues of the same relational power are equal.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableBX0010 binary_modular_exponentiation_result_exists_uniqueEvery guarded modular exponentiation has exactly one actual canonical natural result.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StablePD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0021 BinaryModulus(m)The exact constructive nontrivial-modulus guard 1<m.
Conservative definition · notation layer 1ND0022 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 0PD0008 ModEq(m,a,b)Balanced-natural congruence modulo m.
Conservative definition · notation layer 0ND0023 CanonicalModularResidue(m,a,r)A strictly bounded canonical natural residue r<m together with exact balanced congruence to a modulo m.
Conservative definition · notation layer 1PD0013 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 2ND0024 BinaryDoubledPower(a,h,e,u,z)The exact even-exponent prerequisites e=2*h, Pow(a,h,u) and Pow(a,e,z).
Conservative definition · notation layer 3ND0025 BinaryOddPower(a,h,e,u,z)The exact odd-exponent prerequisites e=2*h+1, Pow(a,h,u) and Pow(a,e,z).
Conservative definition · notation layer 3ND0026 BinaryModularStep(m,u,a,b,r)One exact binary square or square-and-multiply transition with a genuinely canonical reduced output.
Conservative definition · notation layer 2ND0027 BinaryModularPower(a,e,m,r)The exact canonical natural residue of the existing beta-coded exponentiation relation Pow(a,e,z).
Conservative definition · notation layer 3Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.