Statement definitions for the cyclic-additive statement surface

These definitions intentionally duplicate the concrete statement definitions in Challenge.lean. The Challenge may not import candidate-local helper files, so the proof development carries its own copies. Their semantic agreement with the independently structured literature specification was checked in the source project before this import.

def KasamiCyclicAdditive.kasamiExponent (k : ℕ) : ℕ

The Kasami exponent 4^k - 2^k + 1.

Equations

• KasamiCyclicAdditive.kasamiExponent k = 4 ^ k - 2 ^ k + 1

def KasamiCyclicAdditive.kasamiDerivative {K : Type u_1} [Field K] (k : ℕ) (b : K) : K

The normalized derivative of the Kasami monomial in direction 1: δ(b) = (b+1)^d + b^d + 1.

Equations

• KasamiCyclicAdditive.kasamiDerivative k b = (b + 1) ^ KasamiCyclicAdditive.kasamiExponent k + b ^ KasamiCyclicAdditive.kasamiExponent k + 1

def KasamiCyclicAdditive.derivativeImage (k : ℕ) (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] : Finset K

The image Δ of the normalized Kasami derivative.

Equations

• KasamiCyclicAdditive.derivativeImage k K = Finset.image (KasamiCyclicAdditive.kasamiDerivative k) Finset.univ

def KasamiCyclicAdditive.coefficientTripleCount {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (k : ℕ) (v₁ v₂ : K) : ℕ

The number of triples (x,y,z) ∈ Δ³ satisfying v₁ x + v₂ y + (v₁+v₂) z = 0.

Equations

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