Carlet's cyclic-additive conjecture for the Kasami monomials
Gábor P. Nagy, Douglas S. McNeil, Attila Vajda
math.NT
Oct 6, 2026 · v1
math.CO
TL;DR
The main theorem on Kasami cyclic-additive difference sets is formalised and machine-checked in Lean 4 on Mathlib, with AI assistance including Aristotle.
Abstract
Let $K$ be a finite field of characteristic two with $|K| = 2^{n}$, let $\gcd(k,n) = 1$, let $d_{k} = 4^{k} - 2^{k} + 1$ be the Kasami exponent, and let $Δ_{k} = \{(b+1)^{d_{k}} + b^{d_{k}} + 1 : b \in K\}$ be the image of the normalised derivative of the Kasami monomial in the direction $1$. We show that, for all distinct nonzero $v_{1},v_{2} \in K$, \[ \bigl|\{(x,y,z) \in Δ_{k}^{3} : v_{1}x + v_{2}y + (v_{1}+v_{2})z = 0\}\bigr| = 2^{2n-3}. \] This establishes the cyclic-additive difference-set condition introduced by Carlet and later posed for the Kasami functions at NSUCRYPTO 2019. Starting from the known half-size property of the derivative image, we express the Fourier correction as twisted root counts and prove their required nonnegativity by an incidence argument on the Fermat cubic. An exact average over the slopes then forces equality pointwise. The argument covers every admissible pair $(n,k)$ and has been formalised and machine-checked in Lean 4 with Mathlib.
Problem
Carlet's cyclic-additive difference-set condition asks whether the image of the normalised derivative of the Kasami monomial gives exactly 2^{2n-3} solutions to v1 x + v2 y + (v1+v2) z = 0 for all distinct nonzero v1, v2. The condition was posed for the Kasami functions at NSUCRYPTO 2019.
Approach
The parameter is first reduced modulo n, and Frobenius transport moves it to an odd parameter k0 with 2^{k0}+1 = 3m. A Walsh triple-count formula and an exact average over slopes are derived using only the half-size property of the image. The Dillon–Kashyap phase formula turns the Fourier correction into twisted root counts. Nonnegativity of these counts is proved by an incidence argument on the Fermat cubic. The full argument is formalised in Lean 4 with Mathlib, with AI assistance.
Results
The condition holds with exactly 2^{2n-3} solutions for every admissible pair (n,k) with gcd(k,n)=1, which settles the conjecture. The proof is machine-checked by the Lean kernel.
