Counting definitions

The normalized slope form of the triple count, the Walsh coefficient of the derivative image, and the admissible slopes.

The conjecture is stated in Challenge.lean in coefficient form, with coefficients v₁, v₂, v₁+v₂. Dividing through by v₁ puts it in the slope form used throughout the proof, indexed by ρ = v₂/v₁; Statement/CoefficientForm.lean relates the two.

def KasamiCyclicAdditive.slopeTripleCount {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (k : ℕ) (ρ : K) : ℕ

N(ρ) = #{(x,y,z) ∈ Δ³ : x + ρ y + σ z = 0} with σ = 1 + ρ. This is the normalised form of the triple count of the conjecture, obtained from the original v₁ x + v₂ y + v₃ z = 0 by dividing through by v₁ and setting ρ = v₂/v₁.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KasamiCyclicAdditive.walshCoefficient {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (k : ℕ) (ψ : AddChar K ℂ) (a : K) : ℂ

The Walsh coefficient S(a) = ∑_{x ∈ Δ} ψ(a x).

Equations

• KasamiCyclicAdditive.walshCoefficient k ψ a = ∑ x ∈ KasamiCyclicAdditive.derivativeImage k K, ψ (a * x)

def KasamiCyclicAdditive.AdmissibleSlope {K : Type u_1} [Field K] (ρ : K) : Prop

The admissible slopes ρ ≠ 0, 1.

Equations

• KasamiCyclicAdditive.AdmissibleSlope ρ = (ρ ≠ 0 ∧ ρ ≠ 1)

def KasamiCyclicAdditive.slopes (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] : Finset K

The finset of admissible slopes.

Equations

• KasamiCyclicAdditive.slopes K = {r : K | r ≠ 0 ∧ r ≠ 1}