The Walsh and average formulas from half-size alone

The Walsh triple-count formula and the slope-average formula are elementary consequences of the derivative-image half-size equation 2|Δ| = Q alone, for an arbitrary finite subset of a characteristic-two field: no Kasami-specific fact beyond half-size is used.

The arguments are additive-character orthogonality for the Walsh formula, and direct double-counting — including the diagonal x = y = z contribution — for the average. Both are proved for an arbitrary Δ : Finset K and then specialized to derivativeImage k K.

def KasamiCyclicAdditive.CountAverage.slopeTripleCount {K : Type u_1} [Field K] [DecidableEq K] (Delta : Finset K) (ρ : K) : ℕ

Normalized triple count for an arbitrary finite subset.

Equations

• KasamiCyclicAdditive.CountAverage.slopeTripleCount Delta ρ = {p ∈ Delta ×ˢ Delta ×ˢ Delta | p.1 + ρ * p.2.1 + (1 + ρ) * p.2.2 = 0}.card

noncomputable def KasamiCyclicAdditive.CountAverage.walshCoefficient {K : Type u_1} [Field K] (Delta : Finset K) (psi : AddChar K ℂ) (a : K) : ℂ

Walsh coefficient of a finite subset: ∑_{x ∈ Δ} ψ(a x).

Equations

• KasamiCyclicAdditive.CountAverage.walshCoefficient Delta psi a = ∑ x ∈ Delta, psi (a * x)

Auxiliary lemmas

theorem KasamiCyclicAdditive.CountAverage.sum_char_mul {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (psi : AddChar K ℂ) (hpsi : psi.IsPrimitive) (t : K) : ∑ a : K, psi (a * t) = if t = 0 then ↑(Fintype.card K) else 0

Orthogonality: the sum of psi (a * t) over all a is |K| if t = 0, else 0.

theorem KasamiCyclicAdditive.CountAverage.sum_units_eq {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : K → ℂ) : ∑ u : Kˣ, f ↑u = ∑ a ∈ Finset.univ.erase 0, f a

Sum over the units of K equals the sum over the nonzero elements.

theorem KasamiCyclicAdditive.CountAverage.walshCoefficient_zero {K : Type u_1} [Field K] (Delta : Finset K) (psi : AddChar K ℂ) : walshCoefficient Delta psi 0 = ↑Delta.card

The Walsh coefficient at 0 is |Δ|.

theorem KasamiCyclicAdditive.CountAverage.sum_triple_prod {K : Type u_1} (Delta : Finset K) (f g h : K → ℂ) : ∑ p ∈ Delta ×ˢ Delta ×ˢ Delta, f p.1 * g p.2.1 * h p.2.2 = ((∑ x ∈ Delta, f x) * ∑ y ∈ Delta, g y) * ∑ z ∈ Delta, h z

A sum over Δ³ of a product of three one-variable functions factors into the product of the three sums.

theorem KasamiCyclicAdditive.CountAverage.slopeTripleCount_complex {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (Delta : Finset K) (psi : AddChar K ℂ) (hpsi : psi.IsPrimitive) (ρ : K) : ↑(slopeTripleCount Delta ρ) = (↑Delta.card ^ 3 + Phase.phaseTripleSum (walshCoefficient Delta psi) ρ (1 + ρ)) / ↑(Fintype.card K)

The count as a complex identity: (|Δ|³ + Z(ρ)) / |K|.

Combinatorial lemmas for the average

theorem KasamiCyclicAdditive.CountAverage.slopes_card {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (hK : 2 < Fintype.card K) : (slopes K).card = Fintype.card K - 2

slopes K is K with 0 and 1 removed, hence has |K| - 2 elements.

theorem KasamiCyclicAdditive.CountAverage.mem_slopes_iff {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (r : K) : r ∈ slopes K ↔ r ≠ 0 ∧ r ≠ 1

Membership in slopes K is being neither 0 nor 1.

theorem KasamiCyclicAdditive.CountAverage.slope_filter_card {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (hK : 2 < Fintype.card K) (x y z : K) : {ρ ∈ slopes K | x + ρ * y + (1 + ρ) * z = 0}.card = ((Fintype.card K - 2) * if x = y ∧ y = z then 1 else 0) + if x ≠ y ∧ x ≠ z ∧ y ≠ z then 1 else 0

For a fixed triple, the number of admissible slopes solving the equation: |K| - 2 on the diagonal x = y = z, one for a pairwise-distinct triple, and none otherwise.

theorem KasamiCyclicAdditive.CountAverage.diag_card {K : Type u_1} [DecidableEq K] (Delta : Finset K) : {p ∈ Delta ×ˢ Delta ×ˢ Delta | p.1 = p.2.1 ∧ p.2.1 = p.2.2}.card = Delta.card

The diagonal x = y = z of Δ³ has |Δ| points.

theorem KasamiCyclicAdditive.CountAverage.card_filter_ne_two {K : Type u_1} [DecidableEq K] (Delta : Finset K) {x y : K} (hx : x ∈ Delta) (hy : y ∈ Delta) (hxy : x ≠ y) : {z ∈ Delta | x ≠ z ∧ y ≠ z}.card = Delta.card - 2

Removing two specified distinct elements of a finite set lowers its cardinality by two.

theorem KasamiCyclicAdditive.CountAverage.distinct_card {K : Type u_1} [DecidableEq K] (Delta : Finset K) : {p ∈ Delta ×ˢ Delta ×ˢ Delta | p.1 ≠ p.2.1 ∧ p.1 ≠ p.2.2 ∧ p.2.1 ≠ p.2.2}.card = Delta.card * (Delta.card - 1) * (Delta.card - 2)

Δ³ has |Δ| * (|Δ| - 1) * (|Δ| - 2) pairwise-distinct triples.

theorem KasamiCyclicAdditive.CountAverage.sum_tripleCount {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (Delta : Finset K) (hK : 2 < Fintype.card K) : ∑ ρ ∈ slopes K, slopeTripleCount Delta ρ = (Fintype.card K - 2) * Delta.card + Delta.card * (Delta.card - 1) * (Delta.card - 2)

Double-counting over the admissible slopes: a diagonal triple is counted by all |K| - 2 slopes, a pairwise-distinct triple by exactly one, and no other triple contributes.

The two generic targets

theorem KasamiCyclicAdditive.CountAverage.count_formula_of_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (Delta : Finset K) (psi : AddChar K ℂ) (hpsi : psi.IsPrimitive) (hhalf : 2 * Delta.card = Fintype.card K) (ρ : K) : ↑(slopeTripleCount Delta ρ) = ↑(Fintype.card K) ^ 2 / 8 + (Phase.phaseTripleSum (walshCoefficient Delta psi) ρ (1 + ρ)).re / ↑(Fintype.card K)

The count formula under half-size: additive-character orthogonality turns 2|Δ| = |K| into |K|²/8 plus the real part of the phase correction, at every slope ρ.

theorem KasamiCyclicAdditive.CountAverage.average_of_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (Delta : Finset K) (hhalf : 2 * Delta.card = Fintype.card K) (hK : 2 < Fintype.card K) : (∑ ρ ∈ slopes K, ↑(slopeTripleCount Delta ρ)) / ↑(slopes K).card = ↑(Fintype.card K) ^ 2 / 8

Under half-size the admissible-slope average of the triple count is exactly |K|²/8, by double-counting (ρ,x,y,z). The assumption 2 < |K| only makes the average's denominator nonzero; in the final Kasami theorem |K| = 2^n with n ≥ 2.

Specialization to derivativeImage k K

theorem KasamiCyclicAdditive.walshTripleCountFormula_of_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {k : ℕ} (hhalf : 2 * (derivativeImage k K).card = Fintype.card K) (ρ : K) : AdmissibleSlope ρ → ↑(slopeTripleCount k ρ) = ↑(Fintype.card K) ^ 2 / 8 + (Phase.phaseTripleSum (walshCoefficient k (primitiveAddChar K)) ρ (1 + ρ)).re / ↑(Fintype.card K)

The Walsh triple-count formula follows from the derivative-image half-size equation alone. AdmissibleSlope is retained here because this theorem is the downstream slope-interface, although the generic identity holds for every ρ.

theorem KasamiCyclicAdditive.slopeAverageFormula_of_half_size {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {k : ℕ} (hhalf : 2 * (derivativeImage k K).card = Fintype.card K) (hK : 2 < Fintype.card K) : (∑ ρ ∈ slopes K, ↑(slopeTripleCount k ρ)) / ↑(slopes K).card = ↑(Fintype.card K) ^ 2 / 8

The slope-average formula follows from the derivative-image half-size equation (and |K| > 2) alone.