Normalization and Frobenius coefficient transport

Two independent facts:

• exists_normalized_parameter — elementary arithmetic choosing between k and n - k so that the chosen representative avoids the bad class k ≡ 3 (mod 6);
• coefficientCount_transfer_complement — the finite-field Frobenius bijection relating the counts at k and n - k.

Transport is stated in the original coefficient form. This avoids the incorrect stronger claim that slopeTripleCount k ρ = slopeTripleCount (n-k) ρ at the same slope: Frobenius acts on the coefficients, hence on the slope, as well.

theorem KasamiCyclicAdditive.exists_normalized_parameter {n k : ℕ} (hklt : k < n) (hkn : k.Coprime n) : ∃ (k0 : ℕ) (m : ℕ), (k0 = k ∨ k0 = n - k) ∧ Odd k0 ∧ k0.Coprime n ∧ 2 ^ k0 + 1 = 3 * m ∧ m.Coprime (2 ^ n - 1)

For k < n coprime to n, one of k, n - k is odd, coprime to n, and avoids k ≡ 3 (mod 6) when n is even, hence supplies an m with 2 ^ k0 + 1 = 3 * m and gcd(m, 2 ^ n - 1) = 1.

Frobenius transport auxiliaries

theorem KasamiCyclicAdditive.coefficientCount_transfer_complement {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k : ℕ} (hk : k ≤ n) (hcard : Fintype.card K = 2 ^ n) {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : ∃ (w1 : K) (w2 : K), w1 ≠ 0 ∧ w2 ≠ 0 ∧ w1 ≠ w2 ∧ coefficientTripleCount k v₁ v₂ = coefficientTripleCount (n - k) w1 w2

Frobenius transport of the coefficient count from k to n - k. The coefficients move with Δ, so the transported count sits at new coefficients w1, w2 rather than at v₁, v₂.

theorem KasamiCyclicAdditive.normalize_with_count_transport {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k : ℕ} (hkpos : 1 ≤ k) (hklt : k < n) (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) (hhalf : 2 * (derivativeImage k K).card = Fintype.card K) {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : ∃ (k0 : ℕ) (m : ℕ) (w1 : K) (w2 : K), (k0 = k ∨ k0 = n - k) ∧ 1 ≤ k0 ∧ k0 < n ∧ Odd k0 ∧ k0.Coprime n ∧ 2 ^ k0 + 1 = 3 * m ∧ m.Coprime (2 ^ n - 1) ∧ 2 * (derivativeImage k0 K).card = Fintype.card K ∧ w1 ≠ 0 ∧ w2 ≠ 0 ∧ w1 ≠ w2 ∧ coefficientTripleCount k v₁ v₂ = coefficientTripleCount k0 w1 w2

The normalized parameter k0 together with the coefficients carrying the count to it: exists_normalized_parameter chooses k0 ∈ {k, n - k}, and in the complement case coefficientCount_transfer_complement supplies w1, w2.