CG0001 mod_eq_cancel_gcd_cofactorThe actual quotient modulus m/g exactly classifies cancellation of a common coefficient at nonzero m.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableExact modular equations · actual arithmetic witnesses
Explore the exact twelve newly checked congruence arithmetic statements and their complete original proofs.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
CG0001 mod_eq_cancel_gcd_cofactorThe actual quotient modulus m/g exactly classifies cancellation of a common coefficient at nonzero m.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0002 linear_congruence_solution_class_iff_reduced_modulusRelative to any actual solution, every natural solution is exactly its class modulo the actual gcd cofactor.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0003 linear_congruence_reduced_representative_existsConstruct a genuine solution strictly below m/g, not merely below m, from the actual gcd divisibility witness.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0004 linear_congruence_progression_bound_iffWith an actual remainder r<M, r+M*t is below g*M exactly when t<g; no field or coprimality hypothesis is used.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0005 linear_congruence_bounded_residue_parametrizedConstruct the exact interval parameter for every bounded member of a residue class, and conversely.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0006 linear_congruence_bounded_parameter_uniqueThe actual progression parameter is unique for nonzero M, even without imposing a redundant parameter bound.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0007 linear_congruence_bounded_solutions_parametrizedAll solutions below the original nonzero modulus are exactly r+M*t for t<g, for an actual reduced representative r.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0008 linear_congruence_exact_bounded_enumeration_existsConstruct r and an actual bijection from t<g to all solutions x<m. This is a cardinality witness, not a claimed beta-coded list.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG0009 linear_congruence_zero_modulus_nonzero_coefficient_uniqueAt modulus zero a nonzero coefficient has at most one natural solution; no bounded residue or finite-class formula is asserted.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG000A linear_congruence_zero_modulus_zero_coefficient_iffWith coefficient and modulus both zero, every natural x is a solution exactly when the target is zero.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG000B linear_congruence_modulus_one_bounded_iff_zeroFor modulus one the unique strictly bounded solution is zero for every coefficient and target.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StableCG000C fermat_little_all_inputsFermat's little theorem for every natural base in relational-power form.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not StablePD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0PD0004 Prime(p)p is nonunit and every factorization of p has a unit factor.
Conservative definition · notation layer 0PD0005 Coprime(a,b)Every common divisor of a and b is one.
Conservative definition · notation layer 1PD0006 IsGCD(g,a,b)g is a common divisor divisible by every common divisor.
Conservative definition · notation layer 1PD0007 DivRem(n,d,q,r)q and r are a quotient and a strict remainder for n by d.
Conservative definition · notation layer 1PD0008 ModEq(m,a,b)Balanced-natural congruence modulo m.
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 2Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.