`powMod`: binary modular exponentiation for kernel-`decide` modular arithmetic #

ZModDecide decides a ground ZMod m ring identity by a bounded integer-residue computation, reducing % m after every operation. Its pow node computes base ^ n in full before the final % m, so a huge exponent — a Legendre-symbol exponent (p - 1) / 2 ≈ 2 ^ 380 at BLS12-381 size — builds an astronomically large intermediate and stalls the kernel.

This module supplies the missing piece: a square-and-multiply modular exponentiation powMod b e m that reduces % m after every squaring and multiply, so no intermediate exceeds m ^ 2. The recursion is structural on a fuel argument, and the fuel is only a termination certificate — the e = 0 guard halts the loop after ⌈log₂ e⌉ steps — so the Lean kernel reduces a fully applied powMod in a logarithmic number of steps and decide stays on the GMP Nat fast path.

On top of it sit two number-theoretic deciders whose exponents were previously out of reach: a modular inverse via Fermat's little theorem, and a quadratic-residue test via Euler's criterion.

Main results #

powMod / powModGo — square-and-multiply modular exponentiation and its fuelled worker.
powMod_cast — the correctness lemma: (powMod b e m : ZMod m) = (b : ZMod m) ^ e.
powMod_lt — the output is a residue, powMod b e m < m for 1 < m.
invMod / invMod_cast — modular inverse for a prime modulus, a ^ (p - 2) % p, correct as (a : ZMod p)⁻¹.
isSquare_of_powMod / not_isSquare_of_powMod — the Euler-criterion quadratic-residue decider: IsSquare (a : ZMod p) reduces to a kernel decide on powMod a.val (p / 2) p = 1.

Binary modular exponentiation #

source

def Transfer.ZModPowMod.powModGo (m : ℕ) :

ℕ → ℕ → ℕ → ℕ → ℕ

Square-and-multiply worker for modular exponentiation. fuel bounds the number of squarings; base is the running square b ^ (2 ^ k), e the remaining exponent bits, and acc the accumulated product, all kept reduced % m. The e = 0 guard halts the loop, so the actual recursion depth is the bit length of the initial exponent.

Equations

One or more equations did not get rendered due to their size.
Transfer.ZModPowMod.powModGo m 0 x✝² x✝¹ x✝ = x✝

Instances For

source

def Transfer.ZModPowMod.powMod (b e m : ℕ) :

ℕ

b ^ e mod m by square-and-multiply, reducing % m after every operation. Fuel e is a termination certificate (e < 2 ^ e); the e = 0 guard in powModGo stops the loop after ⌈log₂ e⌉ steps, so a fully applied powMod reduces in the kernel in a logarithmic number of GMP Nat operations.

Equations

Transfer.ZModPowMod.powMod b e m = Transfer.ZModPowMod.powModGo m e (b % m) e (1 % m)

Instances For

source

theorem Transfer.ZModPowMod.powModGo_cast (m fuel base e acc : ℕ) :

e < 2 ^ fuel → ↑(powModGo m fuel base e acc) = ↑acc * ↑base ^ e

The worker invariant: cast back into ZMod m, powModGo computes acc * base ^ e, provided the fuel covers the exponent (e < 2 ^ fuel).

source

theorem Transfer.ZModPowMod.powMod_cast (b e m : ℕ) :

↑(powMod b e m) = ↑b ^ e

Correctness. In ZMod m, powMod b e m is (b : ZMod m) ^ e: the residue computation cast back equals the abstract power.

source

theorem Transfer.ZModPowMod.powModGo_lt (m : ℕ) (hm : 0 < m) (fuel base e acc : ℕ) :

acc < m → powModGo m fuel base e acc < m

The worker stays inside [0, m): with a reduced accumulator, so is the output.

source

theorem Transfer.ZModPowMod.powMod_lt (b e m : ℕ) (hm : 1 < m) :

powMod b e m < m

powMod b e m is a residue: it lies in [0, m) for 1 < m.

Modular inverse via Fermat's little theorem #

source

theorem Transfer.ZModPowMod.zmod_pow_sub_two (p : ℕ) [Fact (Nat.Prime p)] (a : ZMod p) (h : a ≠ 0) :

a ^ (p - 2) = a⁻¹

Fermat's little theorem in inverse form: over a prime field, a ^ (p - 2) = a⁻¹.

source

def Transfer.ZModPowMod.invMod (a p : ℕ) :

ℕ

Modular inverse of a modulo a prime p, computed as a ^ (p - 2) mod p.

Equations

Transfer.ZModPowMod.invMod a p = Transfer.ZModPowMod.powMod a (p - 2) p

Instances For

source

theorem Transfer.ZModPowMod.invMod_cast (p : ℕ) [Fact (Nat.Prime p)] (a : ℕ) (ha : a % p ≠ 0) :

↑(invMod a p) = (↑a)⁻¹

Correctness of invMod. For a prime modulus and a not divisible by p, invMod a p casts to the field inverse (a : ZMod p)⁻¹.

Quadratic residues via Euler's criterion #

source

theorem Transfer.ZModPowMod.isSquare_of_powMod (p : ℕ) [Fact (Nat.Prime p)] (a : ZMod p) (ha : a ≠ 0) (h : powMod a.val (p / 2) p = 1) :

IsSquare a

Euler-criterion quadratic-residue witness. For a concrete nonzero a : ZMod p with p prime, a kernel decide on powMod a.val (p / 2) p = 1 proves IsSquare a.

source

theorem Transfer.ZModPowMod.not_isSquare_of_powMod (p : ℕ) [Fact (Nat.Prime p)] (a : ZMod p) (ha : a ≠ 0) (h : powMod a.val (p / 2) p ≠ 1) :

¬IsSquare a

Euler-criterion non-residue witness. For a concrete nonzero a : ZMod p with p prime, a kernel decide on powMod a.val (p / 2) p ≠ 1 proves ¬ IsSquare a.