The assembled theorem

The final assembly. Assembly/Reduction.lean proves the conjecture from the half-size cardinality at k; MCM/HalfSize.lean proves the half-size fact itself from the MCM permutation theorem. Composing them leaves no mathematical hypothesis beyond those in the normalized statement.

The literature statement does not assume k < n. The final theorem below derives n ≥ 2 from the coefficient hypotheses, then reduces arbitrary k coprime to n to k % n using the proved periodicity results in Statement/ParameterReduction.lean. Positivity of the normalized representative is also derived, not assumed.

theorem KasamiCyclicAdditive.carlet_kasami_cyclic_additive_core {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) {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : coefficientTripleCount k v₁ v₂ = 2 ^ (2 * n - 3)

Self-contained proof target for Carlet's Kasami cyclic-additive conjecture in the normalized range 1 ≤ k < n.

theorem KasamiCyclicAdditive.carlet_kasami_cyclic_additive_literature {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k : ℕ} (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : coefficientTripleCount k v₁ v₂ = 2 ^ (2 * n - 3)

Literature form of the conjecture. No range or positivity hypothesis on k is needed at the statement surface: the remaining hypotheses force n ≥ 2, and coprimality then makes k % n a positive representative below n. The coefficient count is invariant under this reduction.