Congruence Arithmetic — Exact Proof Explorer

The actual quotient modulus m/g exactly classifies cancellation of a common coefficient at nonzero m.

Relative to any actual solution, every natural solution is exactly its class modulo the actual gcd cofactor.

Construct a genuine solution strictly below m/g, not merely below m, from the actual gcd divisibility witness.

With an actual remainder r<M, r+M*t is below g*M exactly when t<g; no field or coprimality hypothesis is used.

Construct the exact interval parameter for every bounded member of a residue class, and conversely.

The actual progression parameter is unique for nonzero M, even without imposing a redundant parameter bound.

All solutions below the original nonzero modulus are exactly r+M*t for t<g, for an actual reduced representative r.

Construct r and an actual bijection from t<g to all solutions x<m. This is a cardinality witness, not a claimed beta-coded list.

At modulus zero a nonzero coefficient has at most one natural solution; no bounded residue or finite-class formula is asserted.

With coefficient and modulus both zero, every natural x is a solution exactly when the target is zero.

For modulus one the unique strictly bounded solution is zero for every coefficient and target.

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