Shared Frobenius and power-of-two arithmetic

Facts used by the Fermat-cubic, MCM and normalization layers alike. This module depends on nothing but Mathlib, and is kept separate from Statement/Definitions.lean so that a file may depend on the arithmetic without depending on the Kasami definitions, or vice versa.

• pow_two_pow_mul_self, pow_two_pow_gcd, pow_card_two_pow: fixedness under iterated Frobenius and finite-field cardinality.
• two_pow_mod_three, two_pow_mod_three_of_odd, two_pow_mod_nine, two_pow_two_mul_sub_one: elementary arithmetic of 2 ^ k.

Fixedness under iterated Frobenius

theorem KasamiCyclicAdditive.pow_two_pow_mul_self {K : Type u_1} [Field K] {x : K} {m : ℕ} (hm : x ^ 2 ^ m = x) (q : ℕ) : x ^ 2 ^ (m * q) = x

Iterating the 2^m-power map: x^(2^(m*q)) = x whenever x^(2^m) = x.

theorem KasamiCyclicAdditive.pow_two_pow_gcd {K : Type u_1} [Field K] {x : K} {a b : ℕ} (ha : x ^ 2 ^ a = x) (hb : x ^ 2 ^ b = x) : x ^ 2 ^ a.gcd b = x

Fixed field / Bézout step. If x is fixed by π^a and by π^b, then it is fixed by π^(gcd a b).

theorem KasamiCyclicAdditive.pow_card_two_pow {K : Type u_1} [Field K] [Fintype K] {n : ℕ} (hcard : Fintype.card K = 2 ^ n) (a : K) : a ^ 2 ^ n = a

On a finite field of order 2 ^ n, a ^ (2 ^ n) = a.

Elementary arithmetic of 2 ^ k

theorem KasamiCyclicAdditive.two_pow_mod_three (k : ℕ) : 2 ^ k % 3 = 2 ^ (k % 2) % 3

2 has multiplicative order dividing 2 modulo 3.

theorem KasamiCyclicAdditive.two_pow_mod_three_of_odd {k : ℕ} (hk : Odd k) : 2 ^ k % 3 = 2

For odd k, 2 ^ k ≡ 2 (mod 3).

theorem KasamiCyclicAdditive.two_pow_mod_nine (k : ℕ) : 2 ^ k % 9 = 2 ^ (k % 6) % 9

2 has multiplicative order dividing 6 modulo 9.

theorem KasamiCyclicAdditive.two_pow_two_mul_sub_one (k : ℕ) : 2 ^ (2 * k) - 1 = (2 ^ k + 1) * (2 ^ k - 1)

2 ^ (2k) - 1 factors as (2 ^ k + 1) (2 ^ k - 1).