AI 中文总结
该研究解决Bent划分深度是否为素幂的问题，通过证明平移后点的精细单元分布规律，推出深度必为素幂，结合维度限制得到全局界，相关结论已在Lean 4中形式化验证。
AI 中文摘要
有限域F_p^n上的p元Bent划分是指将其划分为K个非空单元，使得每个单元到F_p的平衡赋值均能生成一个Bent函数。此前有问题提出：每个可能的深度K是否为p的幂次；对于一般的p，已有的肯定结果需满足正则性或单元对称性假设。我们证明了更强的无条件结论：对任意非零h，平移h后恰好有p^n/K个点留在同一精细单元中。由此可得，精细单元构成一个划分差族，且精细标签映射是零差平衡的。进而推出K整除p^n，故K=p^t；结合单元非空的条件可得1≤t<n。在偶维情况下，经典单元大小定理给出K整除p^{n/2}。结合已知的奇维三元三纤维参数限制，得到全局界t≤⌊n/2⌋。该证明是对平衡粗化的精确有限平均，主要计数恒等式及部分结论已在Lean 4中形式化并经内核验证。
英文摘要
A $p$-ary bent partition of $\mathbb{F}_p^n$ is a partition into $K$ nonempty cells such that every balanced assignment of its cells to $\mathbb{F}_p$ produces a bent function. It was asked whether every possible depth $K$ is a power of $p$; for general $p$, previous affirmative results required regularity or cell-symmetry hypotheses. We prove the stronger unconditional statement that, for every nonzero $h$, exactly $p^n/K$ points remain in the same fine cell under translation by $h$. Thus the fine cells form a partitioned difference family and the fine label map is zero-difference balanced. Consequently $K\mid p^n$, so $K=p^t$; nonempty cells further give $1\le t<n$. In even dimension, the classical cell-size theorem yields $K\mid p^{n/2}$. Together with the known odd-dimensional ternary three-fibre parameter restriction, this gives the global bound $t\le\lfloor n/2\rfloor$. The proof is an exact finite average over balanced coarsenings. The main counting identity and selected consequences are formalized and kernel-checked in Lean 4.
Comments8 pages. Ancillary files contain the Lean 4 formalization, axiom audits, and reproducibility materials
