Bounded modular exponentiation

Exponentiation by squaring for exact modular arithmetic without constructing the usually enormous unreduced power.

This helper is representation-independent and is used when quantizers need a power only modulo a known denominator or code range. Reducing after every multiplication keeps intermediate naturals bounded while the accompanying equations preserve the exact mathematical residue.

def FloatLib.Numerics.modularPow (base exponent modulus : ℕ) : ℕ

Compute base ^ exponent modulo modulus by exponentiation by squaring.

Only residues smaller than modulus are multiplied, so a large exponent does not construct the usually enormous natural number base ^ exponent. Modulus zero has the explicit total result zero; callers that need ordinary modular arithmetic should establish that the modulus is nonzero.

@[simp]

theorem FloatLib.Numerics.modularPow_zero (base exponent : ℕ) : modularPow base exponent 0 = 0

The library's total modular-power convention returns zero at modulus zero.

theorem FloatLib.Numerics.modularPow_eq_pow_mod (base exponent modulus : ℕ) (hmodulus : modulus ≠ 0) : modularPow base exponent modulus = base ^ exponent % modulus

Exponentiation by squaring computes the ordinary modular power for a nonzero modulus.