The assembled Kasami chain

This file is the place where the independently machine-checked geometric and phase modules — Geometry/FermatCubic, Geometry/PointFrobenius.lean, Geometry/FermatCubic/RationalKernel.lean, Geometry/EvenCase.lean and Phase/RootCount.lean — are joined into the final chain of the conjecture.

The main theorem is parameterized by explicit mathematical hypotheses for the Walsh formula, the triple-count formula, and the slope average. These are ordinary theorem arguments, not axioms; the count and average formulas are discharged internally from the half-size result, while the Walsh formula can be supplied by the phase theorem.

The even-dimensional route is implemented outside this file: Geometry/EvenCase.lean proves root-solvability by the quotient-first bridge, inverting the prime-to-3 isogeny factor G on E(K) directly (PointFrobenius.exists_gMap_preimage) and then taking a single (1 + π) preimage over AlgebraicClosure K.

The four bridging statements

The statements joining the geometric and phase modules to the counting argument. They are collected here so that the chain reads end to end.

Auxiliary lemmas for the Dillon--Kashyap derivation

theorem KasamiCyclicAdditive.fourier_units {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {psi : AddChar K ℂ} (g : Kˣ → ℂ) (a : Kˣ) : ↑(Fintype.card Kˣ) * ∑ x : Kˣ, g x * psi (↑a * ↑x) = ∑ chi : MulChar K ℂ, (∑ y : Kˣ, g y * chi ↑y) * chi ↑a * gaussSum chi⁻¹ psi

Multiplicative Fourier inversion on Kˣ: additive sum to Gauss sums.

The geometric input, in slope-free form

The two root-existence statements exist only to supply RootEqSolvable: the bare statement that the twisted root equation is solvable at every affine Fermat target with nonzero coordinates. one_le_rootCount below uses it directly to bound the root counts, with no intermediate geometric assumption.

Concretely w = W ^ 3, z = T ^ 3 for a point (W, T) of the Fermat cubic, so w + z = 1 is the Fermat equation and w ^ m = W ^ (3m) = W ^ (2^k+1); the displayed equation is then exactly the twisted root equation of KasamiCyclicAdditive.FermatCubic.exists_twisted_root_equation.

(RootEqSolvable lives in Geometry/RootEquation.lean so that Geometry/EvenCase.lean, which proves it for even n, can be imported here without an import cycle.)

theorem KasamiCyclicAdditive.walshCharacterFormula_of_phase_formula {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {k : ℕ} {ψ : AddChar K ℂ} (_hψ : ψ.IsPrimitive) (_hphase : DillonKashyapPhaseFormula k ψ) : Phase.WalshCharacterFormula ψ (2 ^ k + 1) (walshCoefficient k ψ)

The Fourier interface. The Dillon–Kashyap phase formula plus 0 ∈ Δ give the all-character Walsh identity 2 S(a) = (Q/N) ∑_χ [G(χ^e)/G(χ³)] χ(a), which is KasamiCyclicAdditive.Phase.WalshCharacterFormula — the sole hypothesis consumed by KasamiCyclicAdditive.Phase.phase_to_root_count.

The derivation: expand 1_Δ = (1 + F)/2 on K*, invert the multiplicative transform, use G(χ)G(χ⁻¹) = Q for χ ≠ 1 (valid because -1 = 1 in characteristic two) and Ghat(1) = -1, Fhat(1) = -1.

theorem KasamiCyclicAdditive.rootEquationSolvable_odd {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k m : ℕ} (hn : Odd n) (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) (hm : 2 ^ k + 1 = 3 * m) : RootEqSolvable m K

Odd-dimensional root existence.

For odd n every affine Fermat target with nonzero coordinates is hit by Φ_k = -(1 + π^k) + T₃, so the twisted root equation is solvable.

Route. Φ_k(Q) = Φ_k(Q') iff (1 + π^k)(Q - Q') = 0, and KasamiCyclicAdditive.FermatCubicFrobenius.rational_kernel_odd says the K-rational kernel of 1 + π^k is just the origin, so Φ_k is injective, hence bijective on the finite group E(K). Given a target (p, q) with p, q ≠ 0 take Q = Φ_k⁻¹ (pt p q). Q is affine (the three points at infinity are 3-torsion and Φ_k maps them among themselves, whereas pt p q is not 3-torsion by KasamiCyclicAdditive.FermatCubic.three_torsion_pt_iff), and Q = pt W T has W, T ≠ 0 by the same torsion criterion. Then KasamiCyclicAdditive.FermatCubic.exists_twisted_root_equation gives W ^ (2^k+1) + p * T ^ (2^k+1) = q, and w = W ^ 3, z = T ^ 3 is the required pair.

theorem KasamiCyclicAdditive.phaseTripleSum_eq_zero_of_not_cube {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {k m : ℕ} {ψ : AddChar K ℂ} {ρ : K} (_hψ : ψ.IsPrimitive) (_he : 2 ^ k + 1 = 3 * m) (_hW : Phase.WalshCharacterFormula ψ (2 ^ k + 1) (walshCoefficient k ψ)) (_hnc : (¬∃ (A : K), A ^ 3 = ρ) ∨ ¬∃ (B : K), B ^ 3 = 1 + ρ) : Phase.phaseTripleSum (walshCoefficient k ψ) ρ (1 + ρ) = 0

Cube-support collapse. For even n, R(χ) = G((χ³)^m)/G(χ³) is invariant under multiplication by cubic characters, so summing each cubic orbit in the Walsh identity kills every non-cube. Hence Z(ρ) = 0 unless both ρ and 1 + ρ are cubes.

The character-sum half is KasamiCyclicAdditive.Phase.S_eq_zero_of_not_cube; this lemma concludes vanishing of the triple sum. It suffices that one of ρ, 1 + ρ fail to be a cube, since the triple sum then has a vanishing factor either way.

theorem KasamiCyclicAdditive.phaseTripleSum_re_nonneg_of_cube {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {k m D : ℕ} {ψ : AddChar K ℂ} {ρ : K} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (he : 2 ^ k + 1 = 3 * m) (hW : Phase.WalshCharacterFormula ψ (2 ^ k + 1) (walshCoefficient k ψ)) (hadm : AdmissibleSlope ρ) {A B : K} (hA : A ≠ 0) (hAB : A ^ 3 + B ^ 3 = 1) (hrho : ρ = A ^ 3) (hsolv : RootEqSolvable m K) : 0 ≤ (Phase.phaseTripleSum (walshCoefficient k ψ) ρ (1 + ρ)).re

Z(ρ) ≥ 0 at a cube slope. KasamiCyclicAdditive.Phase.phase_to_root_count evaluates the correction term at the pair (A³, B³), which for ρ = A³, 1 + ρ = B³ is the slope of interest, as Q²/8 * (T - c²) with T the total root count over μ₃ × μ₃ and c = |μ₃|. one_le_rootCount gives c² ≤ T.

Positivity of the correction term at every slope

theorem KasamiCyclicAdditive.phaseTripleSum_re_nonneg {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k m D : ℕ} {ψ : AddChar K ℂ} {ρ : K} (hψ : ψ.IsPrimitive) (hcard : Fintype.card K = 2 ^ n) (hkn : k.Coprime n) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (he : 2 ^ k + 1 = 3 * m) (hcop : m.Coprime (2 ^ n - 1)) (hW : Phase.WalshCharacterFormula ψ (2 ^ k + 1) (walshCoefficient k ψ)) (hadm : AdmissibleSlope ρ) : 0 ≤ (Phase.phaseTripleSum (walshCoefficient k ψ) ρ (1 + ρ)).re

Z(ρ) ≥ 0 for every admissible slope: cube slopes by root existence, non-cube slopes by the cube-support collapse. In odd dimension every element is a cube, so only the first branch occurs.

The conjecture

theorem KasamiCyclicAdditive.kasami_conjecture_of_inputs {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k m D : ℕ} {ψ : AddChar K ℂ} (hψ : ψ.IsPrimitive) (hcard : Fintype.card K = 2 ^ n) (hkn : k.Coprime n) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (he : 2 ^ k + 1 = 3 * m) (hcop : m.Coprime (2 ^ n - 1)) (hW : Phase.WalshCharacterFormula ψ (2 ^ k + 1) (walshCoefficient k ψ)) (hcount_formula : ∀ (ρ : K), AdmissibleSlope ρ → ↑(slopeTripleCount k ρ) = ↑(Fintype.card K) ^ 2 / 8 + (Phase.phaseTripleSum (walshCoefficient k ψ) ρ (1 + ρ)).re / ↑(Fintype.card K)) (havg : (∑ ρ ∈ slopes K, ↑(slopeTripleCount k ρ)) / ↑(slopes K).card = ↑(Fintype.card K) ^ 2 / 8) (hne : (slopes K).Nonempty) (ρ : K) : ρ ∈ slopes K → ↑(slopeTripleCount k ρ) = ↑(Fintype.card K) ^ 2 / 8

The Kasami cyclic-additive conjecture, in normalised slope form.

Let K = GF(2^n), gcd(k, n) = 1, d = 4^k - 2^k + 1, δ(b) = (b+1)^d + b^d + 1 and Δ = im δ. Then for every ρ ≠ 0, 1

#{(x,y,z) ∈ Δ³ : x + ρ y + (1+ρ) z = 0} = Q²/8 = 2^(2n-3).

The theorem is parameterized by the normalisation data (m, D) and by the explicit Walsh, triple-count, and average equations. The Walsh hypothesis hW (KasamiCyclicAdditive.Phase.WalshCharacterFormula) can be obtained from DillonKashyapPhaseFormula via walshCharacterFormula_of_phase_formula; the triple-count and average hypotheses are discharged from the half-size result in Assembly/Reduction.lean.