Reduction around the assembled Kasami chain

This module assembles the reduction around kasami_conjecture_of_inputs. The count and average identities are derived in Counting/Average.lean, and the normalization and Frobenius coefficient transport in Normalization, both from the derivative-image half-size equation together with elementary arithmetic. The theorems below are kept in their general hypothesis-taking form, with convenience wrappers taking only the half-size equation (and, in one case, also DillonKashyapPhaseFormula) supplied afterwards.

theorem KasamiCyclicAdditive.three_factor_ne_zero {k m : ℕ} (he : 2 ^ k + 1 = 3 * m) : m ≠ 0

The factor m in 2^k+1=3m is automatically nonzero.

theorem KasamiCyclicAdditive.normalized_slope_of_phase_count_average {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k m : ℕ} (hn : 2 ≤ n) (hcard : Fintype.card K = 2 ^ n) (hkn : k.Coprime n) (he : 2 ^ k + 1 = 3 * m) (hcop : m.Coprime (2 ^ n - 1)) (hphase : DillonKashyapPhaseFormula k (primitiveAddChar K)) (hcount_formula : ∀ (ρ : K), AdmissibleSlope ρ → ↑(slopeTripleCount k ρ) = ↑(Fintype.card K) ^ 2 / 8 + (Phase.phaseTripleSum (walshCoefficient k (primitiveAddChar K)) ρ (1 + ρ)).re / ↑(Fintype.card K)) (havg : (∑ ρ ∈ slopes K, ↑(slopeTripleCount k ρ)) / ↑(slopes K).card = ↑(Fintype.card K) ^ 2 / 8) (ρ : K) : ρ ∈ slopes K → ↑(slopeTripleCount k ρ) = ↑(Fintype.card K) ^ 2 / 8

The normalized slope theorem from the Dillon–Kashyap phase formula together with the count and average identities. The primitive additive character, the inverse exponent D, the Walsh formula, and nonemptiness of slopes K are all constructed internally.

Half-size/cardinality-only form

phase_formula_from_half_size (MCM/PhaseFormula.lean) supplies the phase formula directly from the half-size cardinality and elementary MCM/Dickson character algebra, so these theorems need no Dillon–Kashyap or Dillon–Dobbertin input.

theorem KasamiCyclicAdditive.normalized_slope_of_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k m : ℕ} (hkpos : 1 ≤ k) (hklt : k < n) (hk : Odd k) (hcard : Fintype.card K = 2 ^ n) (hkn : k.Coprime n) (he : 2 ^ k + 1 = 3 * m) (hcop : m.Coprime (2 ^ n - 1)) (hhalf : 2 * (derivativeImage k K).card = Fintype.card K) (ρ : K) : ρ ∈ slopes K → ↑(slopeTripleCount k ρ) = ↑(Fintype.card K) ^ 2 / 8

The normalized slope theorem, half-size/cardinality-only form.

theorem KasamiCyclicAdditive.coefficient_conjecture_of_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k k0 m : ℕ} (hkpos : 1 ≤ k0) (hklt : k0 < n) (hk : Odd k0) (hcard : Fintype.card K = 2 ^ n) (hkn0 : k0.Coprime n) (he : 2 ^ k0 + 1 = 3 * m) (hcop : m.Coprime (2 ^ n - 1)) (hhalf : 2 * (derivativeImage k0 K).card = Fintype.card K) {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 half-size at the normalized parameter k0, given coefficients w1, w2 carrying the count to k0.

theorem KasamiCyclicAdditive.kasami_conjecture_of_half_size {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₂) : coefficientTripleCount k v₁ v₂ = 2 ^ (2 * n - 3)

The Kasami cyclic-additive coefficient conjecture, half-size-only form. The sole size input is the derivative-image half-size equation; the Dillon–Kashyap phase formula is derived internally by phase_formula_from_half_size of MCM/PhaseFormula.lean.