Exact modular equations · actual arithmetic witnesses

Congruence Arithmetic

Explore the exact twelve newly checked congruence arithmetic statements and their complete original proofs.

12 kernel- and Lean-verified Alpha-closed theorems · 12 conservative definitions · 9 notation dependencies

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.

24 items
CG0001 mod_eq_cancel_gcd_cofactor

The 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 Stable
CG0004 linear_congruence_progression_bound_iff

With 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 Stable
CG0006 linear_congruence_bounded_parameter_unique

The 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 Stable
CG000C fermat_little_all_inputs

Fermat's little theorem for every natural base in relational-power form.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable
PD0001 Le(a,b)

Witness-defined non-strict order on natural numbers.

Conservative definition · notation layer 0
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0003 Dvd(d,n)

The natural number d divides n.

Conservative definition · notation layer 0
PD0004 Prime(p)

p is nonunit and every factorization of p has a unit factor.

Conservative definition · notation layer 0
PD0005 Coprime(a,b)

Every common divisor of a and b is one.

Conservative definition · notation layer 1
PD0006 IsGCD(g,a,b)

g is a common divisor divisible by every common divisor.

Conservative definition · notation layer 1
PD0007 DivRem(n,d,q,r)

q and r are a quotient and a strict remainder for n by d.

Conservative definition · notation layer 1
PD0008 ModEq(m,a,b)

Balanced-natural congruence modulo m.

Conservative definition · notation layer 0
PD0013 BetaAt(b,c,i,x)

x is the bounded beta-decoded value at index i.

Conservative definition · notation layer 0
PD0014 Product(b,c,l,z)

z is the product of a beta-coded prefix of length l.

Conservative definition · notation layer 1
PD0019 Repeat(b,c,a,l)

The decoded prefix repeats a for l positions.

Conservative definition · notation layer 1
PD0020 Pow(a,e,z)

z is the relational e-th power of a.

Conservative definition · notation layer 2

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.