Reduction glue

This module knows nothing about the proof of normalization. It states the exact interface normalization must provide and shows that, once the normalized slope theorem is available, the original coefficient-form conjecture follows.

It also bridges the normalization coprimality gcd(m, 2^n-1) = 1 to the exact modulus |Kˣ| used by the phase argument, and constructs the inverse exponent D.

theorem KasamiCyclicAdditive.card_units_eq_two_pow_sub_one {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {n : ℕ} (hcard : Fintype.card K = 2 ^ n) : Fintype.card Kˣ = 2 ^ n - 1

In a finite field of cardinality 2^n, the unit group has cardinality 2^n-1.

theorem KasamiCyclicAdditive.exists_inverse_exponent_units {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {n m : ℕ} (hn : 2 ≤ n) (hcard : Fintype.card K = 2 ^ n) (hcop : m.Coprime (2 ^ n - 1)) : ∃ (D : ℕ), D ≠ 0 ∧ m * D ≡ 1 [MOD Fintype.card Kˣ]

Inverse exponent D with m * D ≡ 1 modulo the exact order |Kˣ|.

theorem KasamiCyclicAdditive.coefficient_form_of_normalized_witness {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {n k k0 : ℕ} (hn : 2 ≤ n) (hcard : Fintype.card K = 2 ^ n) (hslope : ∀ ρ ∈ slopes K, ↑(slopeTripleCount k0 ρ) = ↑(Fintype.card K) ^ 2 / 8) {v₁ v₂ w1 w2 : K} (hw1 : w1 ≠ 0) (hw2 : w2 ≠ 0) (hwne : w1 ≠ w2) (hcount : coefficientTripleCount k v₁ v₂ = coefficientTripleCount k0 w1 w2) : coefficientTripleCount k v₁ v₂ = 2 ^ (2 * n - 3)

Coefficient form at (k, v₁, v₂) from the normalized slope formula at k0, given a witness identifying the two triple counts.