发表机构
University of Szeged（塞格德大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明了Kasami单项式满足Carlet提出的循环加法差集条件，通过傅里叶修正和Fermat三次曲线上的关联论证，并用Lean 4完成机器验证。
AI 中文摘要
设 $K$ 是特征为二的有限域，且 $|K| = 2^{n}$，设 $\n\ngcd(k,n) = 1$，设 $d_{k} = 4^{k} - 2^{k} + 1$ 为 Kasami 指数，并设 $\n\nDelta_{k} = \n\n{(b+1)^{d_{k}} + b^{d_{k}} + 1: b \n\nin K}$ 为 Kasami 单项式在方向 $1$ 上的正规化导数的像。我们证明，对于所有不同的非零 $v_{1},v_{2} \n\nin K$，\n\n[ \n\nbigl| \n\n{(x,y,z) \n\nin \n\nDelta_{k}^{3}: v_{1}x + v_{2}y + (v_{1}+v_{2})z = 0 \n\n} \n\nbigr| = 2^{2n-3}. \n\n] 这建立了 Carlet 引入的循环加法差集条件，该条件后来在 NSUCRYPTO~2019 中针对 Kasami 函数提出。从导数像的已知半尺寸性质出发，我们将傅里叶修正表示为扭曲根计数，并通过 Fermat 三次曲线上的关联论证证明其所需的非负性。然后对斜率进行精确平均，从而逐点强制等式成立。该论证覆盖所有允许的配对 $(n,k)$，并已在 Lean~4 与 Mathlib 中形式化并通过机器检查。
英文摘要
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.
