The phase-to-root-count identity

Assuming the all-character Walsh formula WalshCharacterFormula, we prove

Z(ρ) = Q²/8 * (∑_{u,v ∈ U} R_{u,v}(A,B) - c²),

for A, B ∈ K^* with A³ + B³ = 1 and A³ ≠ 1, where ρ = A³, σ = B³.

Auxiliary facts about μ₃ and Gauss sums

The generic additive-character and Gauss-sum identities used here are shared from Phase/CharacterSums.lean; this file contains the cube-support and root-count-specific argument.

theorem KasamiCyclicAdditive.Phase.sum_mu3Units {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {M : Type u_2} [AddCommMonoid M] (f : K → M) : ∑ u : Kˣ with u ^ 3 = 1, f ↑u = ∑ u ∈ cubeRootsOne K, f u

Summing over the cube roots of unity in Kˣ is the same as summing over μ₃(K) inside K.

theorem KasamiCyclicAdditive.Phase.card_mu3Units {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] : {u : Kˣ | u ^ 3 = 1}.card = mu3Card K

The cube roots of unity in Kˣ number mu3Card K.

theorem KasamiCyclicAdditive.Phase.card_cubeRoots_units {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (A : Kˣ) : {b : Kˣ | b ^ 3 = A ^ 3}.card = mu3Card K

Every cube in Kˣ has exactly c cube roots.

Step 1: the closed form of S

theorem KasamiCyclicAdditive.Phase.ratio_eq {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {ψ : AddChar K ℂ} (hψ : ψ.IsPrimitive) (m : ℕ) (χ : MulChar K ℂ) : gaussSum (χ ^ (3 * m)) ψ / gaussSum (χ ^ 3) ψ = gaussSum ((χ ^ 3) ^ m) ψ * gaussSum (χ ^ 3)⁻¹ ψ / ↑(Fintype.card K) + if χ ^ 3 = 1 then 1 - 1 / ↑(Fintype.card K) else 0

The Gauss-sum ratio of the Walsh formula, rewritten using G(θ) G(θ⁻¹) = Q.

theorem KasamiCyclicAdditive.Phase.sum_gaussSum_prod {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ψ : AddChar K ℂ} {m : ℕ} (a : Kˣ) : ∑ χ : MulChar K ℂ, gaussSum ((χ ^ 3) ^ m) ψ * gaussSum (χ ^ 3)⁻¹ ψ * χ ↑a = ↑(Fintype.card Kˣ) * ∑ x : Kˣ, ∑ y : Kˣ with y ^ 3 = a * x ^ (3 * m), ψ (↑x + ↑y)

Orthogonality turns the character sum into a count of solutions of y³ = a x^{3m}.

theorem KasamiCyclicAdditive.Phase.walshCoefficient_closed_form {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {ψ : AddChar K ℂ} {m e : ℕ} {S : K → ℂ} (hψ : ψ.IsPrimitive) (he : e = 3 * m) (hS : WalshCharacterFormula ψ e S) (a : Kˣ) : 2 * S ↑a = ↑{b : Kˣ | b ^ 3 = a}.card + ∑ x : Kˣ, ∑ y : Kˣ with y ^ 3 = a * x ^ (3 * m), ψ (↑x + ↑y)

The closed form of the Walsh phase obtained from the supplied all-character Walsh formula hS.

theorem KasamiCyclicAdditive.Phase.two_S_cube {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {ψ : AddChar K ℂ} {m D e : ℕ} {S : K → ℂ} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (he : e = 3 * m) (hS : WalshCharacterFormula ψ e S) (A : Kˣ) : 2 * S (↑A ^ 3) = phiHat ψ D ↑A

For A ∈ Kˣ, twice the phase at the cube A³ is the additive Fourier transform of Φ at A.

theorem KasamiCyclicAdditive.Phase.S_eq_zero_of_not_cube {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {ψ : AddChar K ℂ} {m e : ℕ} {S : K → ℂ} (hψ : ψ.IsPrimitive) (he : e = 3 * m) (hS : WalshCharacterFormula ψ e S) (a : Kˣ) (ha : ¬∃ (b : Kˣ), b ^ 3 = a) : S ↑a = 0

If c = 3, the phase vanishes at non-cubes.

theorem KasamiCyclicAdditive.Phase.eight_phaseTripleSum {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {ψ : AddChar K ℂ} {m D e : ℕ} {S : K → ℂ} {A B : K} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (he : e = 3 * m) (hS : WalshCharacterFormula ψ e S) (hA : A ≠ 0) (hB : B ≠ 0) : 8 * phaseTripleSum S (A ^ 3) (B ^ 3) * ↑(mu3Card K) = ∑ z : Kˣ, phiHat ψ D ↑z * phiHat ψ D (A * ↑z) * phiHat ψ D (B * ↑z)

Reindexing Z over G/U, combined with the closed form of S.

Fourier analysis of Φ

theorem KasamiCyclicAdditive.Phase.sum_phi_eq_zero {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ψ : AddChar K ℂ} {m D : ℕ} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) : ∑ t : K, phi ψ D t = 0

Φ has vanishing total mass, i.e. Φ̂(0) = 0.

theorem KasamiCyclicAdditive.Phase.phiHat_zero {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ψ : AddChar K ℂ} {m D : ℕ} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) : phiHat ψ D 0 = 0

The transform phiHat vanishes at 0.

theorem KasamiCyclicAdditive.Phase.fourier_triple {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {ψ : AddChar K ℂ} {D : ℕ} (hψ : ψ.IsPrimitive) (A B : K) : ∑ z : K, phiHat ψ D z * phiHat ψ D (A * z) * phiHat ψ D (B * z) = ↑(Fintype.card K) * ∑ x : K, ∑ y : K, phi ψ D x * phi ψ D y * phi ψ D (A * x + B * y)

The Parseval-type identity replacing the spectral computation of Steps 4–7.

Step 3: symmetrization

theorem KasamiCyclicAdditive.Phase.symmetrization {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ψ : AddChar K ℂ} {m D : ℕ} (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (A B : K) : ∑ x : K, ∑ y : K, phi ψ D x * phi ψ D y * phi ψ D (A * x + B * y) = ↑(mu3Card K) * ∑ u ∈ cubeRootsOne K, ∑ v ∈ cubeRootsOne K, weilSum ψ D A B u v

Symmetrizing the Weil sum over the cube roots of unity.

Step 2: the root-count Weil sum

theorem KasamiCyclicAdditive.Phase.weilSum_eq {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {ψ : AddChar K ℂ} {m D : ℕ} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) {A B : K} (hA3 : A ^ 3 ≠ 1) {u v : K} (hu : u ∈ cubeRootsOne K) (hv : v ∈ cubeRootsOne K) : weilSum ψ D A B u v = ↑(Fintype.card K) * (↑(rootCount D A B u v) - 1)

The Weil sum in terms of the root count.

Step 8: conclusion

theorem KasamiCyclicAdditive.Phase.phase_to_root_count {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {ψ : AddChar K ℂ} {m D e : ℕ} {S : K → ℂ} {A B : K} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (he : e = 3 * m) (hS : WalshCharacterFormula ψ e S) (hA : A ≠ 0) (hAB : A ^ 3 + B ^ 3 = 1) (hA3 : A ^ 3 ≠ 1) : phaseTripleSum S (A ^ 3) (B ^ 3) = ↑(Fintype.card K) ^ 2 / 8 * (∑ u ∈ cubeRootsOne K, ∑ v ∈ cubeRootsOne K, ↑(rootCount D A B u v) - ↑(mu3Card K) ^ 2)

The phase-to-root-count identity. Let K be a finite field of characteristic two, ψ a primitive additive character of K, e = 3m and D an inverse of m modulo N = #Kˣ. Let S : K → ℂ satisfy the all-character Walsh formula. If A, B ∈ K, with A ≠ 0, A³ + B³ = 1, and A³ ≠ 1, then Z(A³) = Q²/8 (∑_{u,v ∈ μ₃(K)} R_{u,v}(A,B) - c²).

(The source's hypothesis B ≠ 0 is not stated separately here: it is implied by A³ + B³ = 1 together with A³ ≠ 1, and is derived inside the proof.)