← All papers
First page of Value distributions for read-once polynomials on finite fields

Value distributions for read-once polynomials on finite fields

Alexey Yashunsky, Dmitrii Tabalin

math.CO Jul 29, 2026 · v1 cs.DM math.PR
Lean 4 formalizes the two convolution-stability theorems, the exact volume formula, and its sharp exponential rate for the body of distributions.
Consider read-once polynomial functions over a finite field of order $k$, i.e., functions defined by expressions built from field addition, multiplication, and constants, in which every variable occurs at most once. Let $p=(p_1,\dots,p_k)$ be the distribution of the values of a read-once function on independent uniform inputs. We prove that for every $k\ge4$ all such distributions belong to a body $\mathcal{B}_k$, defined by the following relation on the sorted atoms $p_1^\downarrow\geq\cdots\geq p_k^\downarrow$ of the distribution: \[ \mathcal{B}_k=\left\{p:p_k^\downarrow\ge \frac{1-p_2^\downarrow-(1-p_2^\downarrow)^k}{k-1}\right\}, \] or equivalently, $\mathcal{B}_k = \{ p \colon 1-p_2^\downarrow-(k-1)p_k^\downarrow\le(1-p_2^\downarrow)^k\}$. Our main theorem is that this body is stable under the convolutions corresponding to both field operations. More generally, convolution for any quasigroup operation on $k$ points preserves $\mathcal{B}_k$; the multiplicative conclusion needs only an absorbing zero and a quasigroup operation on the nonzero elements. The body is full-dimensional and contains the uniform law and every point mass; its normalized volume is given by an exact one-dimensional integral, and the $k$th root of that volume tends to $0.2183305369\ldots$. The complete development, including the two stability theorems, the exact volume formula, and its sharp exponential rate, has been formalized in Lean 4.

For read-once polynomial functions over a finite field of order k, one asks which regions of the probability simplex are preserved under the additive and multiplicative convolutions induced by field operations. Such stable regions bound the value distributions of read-once computations on independent uniform inputs.

A body B_k is defined via a scalar function ψ_k relating the sorted atoms of a distribution. The authors prove that B_k contains the uniform law and all point masses, and that convolution for any quasigroup operation on k points preserves B_k, with the multiplicative case needing only an absorbing zero and a quasigroup on the nonzero elements. The proof splits multiplication into K-type and D-type cases with rearrangement inequalities and one-parameter path transfer arguments. The complete development is formalized in Lean 4.

For every k≥4, all read-once value distributions lie in B_k, which is full-dimensional and stable under both field convolutions. The normalized volume is given by an exact one-dimensional integral, whose kth root tends to 0.2183305369…