Modular evaluation of ternary prefixes

A ternary prefix depends only on a residue modulo a power of three. The binary-digit modular exponentiation function below lets the finite certificate evaluate those residues without first constructing the enormous value 4 ^ m.

theorem GKPCarry.count_append_replicate_zero {value : ℕ} (hvalue : value ≠ 0) (digits : List ℕ) (count : ℕ) : List.count value (digits ++ List.replicate count 0) = List.count value digits

theorem GKPCarry.count_two_take_eq_count_two_mod_pow (depth n : ℕ) : List.count 2 (List.take depth (Nat.digits 3 n)) = List.count 2 (Nat.digits 3 (n % 3 ^ depth))

Taking depth ternary digits preserves exactly the nonzero digits of the residue modulo 3 ^ depth.

theorem GKPCarry.hasTwoTernaryTwosBelow_iff_mod (depth n : ℕ) : hasTwoTernaryTwosBelow depth n ↔ 2 ≤ List.count 2 (Nat.digits 3 (n % 3 ^ depth))

The two-2 prefix predicate can be checked on a modular residue.

def GKPCarry.powModDigits (base modulus : ℕ) : List ℕ → ℕ

Modular exponentiation over a little-endian list of binary digits.

Equations

• One or more equations did not get rendered due to their size.
• GKPCarry.powModDigits base modulus [] = 1 % modulus

def GKPCarry.powMod (base exponent modulus : ℕ) : ℕ

Modular exponentiation by repeated squaring over binary exponent digits.

Equations

• GKPCarry.powMod base exponent modulus = GKPCarry.powModDigits base modulus (Nat.digits 2 exponent)

theorem GKPCarry.powModDigits_eq_pow_mod (base modulus : ℕ) (digits : List ℕ) (hdigits : ∀ digit ∈ digits, digit < 2) : powModDigits base modulus digits = base ^ Nat.ofDigits 2 digits % modulus

theorem GKPCarry.powMod_eq_pow_mod (base exponent modulus : ℕ) : powMod base exponent modulus = base ^ exponent % modulus

powMod computes the ordinary power modulo modulus.