Fine Difference Structure and Prime-Power Depth of Bent Partitions
Zhaorui Wu
cs.IT
Aug 28, 2026 · v1
math.CO
TL;DR
The balanced-fusion lemma, fine same-label count, cell-size moment, and a five-test certificate were formalized and kernel-checked in Lean 4 with Mathlib.
Abstract
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.
Problem
A p-ary bent partition of F_p^n partitions the space into K cells so every balanced coarsening yields a bent function. It was open whether the depth K must always be a power of p, with prior affirmative results requiring regularity or cell-symmetry hypotheses.
Approach
A balanced-fusion lemma shows that averaging zero-derivative counts over all balanced coarsenings determines the hidden same-cell diagonal exactly. This identifies the fine cells as a partitioned difference family and the label map as zero-difference balanced, forcing K to divide p^n. The main counting identity, cell-size moment, and a five-test depth-six certificate are formalized and kernel-checked in Lean 4.32.0 with Mathlib 4.32.0.
Results
For every nonzero h exactly p^n/K points share their fine cell, so K divides p^n and hence K=p^t with 1<=t<n. Combined with even-dimensional and odd ternary restrictions this gives the global bound t<=floor(n/2), removing prior regularity and symmetry hypotheses.