On Lattice Tilings by Symmetric Limited Magnitude Error Balls: Q-polynomials and Ideal Characterization
Ang Xiao
math.CO
Nov 2, 2026 · v1
TL;DR
All statements except those relying on Maple computations are formalized and machine-checked in Lean 4 with Mathlib, using only standard axioms.
Abstract
In this paper, we study the lattice tilings of $\mathbb{Z}^n$ by the symmetric limited magnitude error balls $\mathcal{B}(n,t,k,k)$, which play a crucial role in flash memory applications. Using generating functions and complete Bell polynomials, we derive an explicit formula for the $r$-th Q-polynomial associated with $\mathcal{B}(n,t,k,k)$. Then, an ideal-theoretic characterization of the lattice tiling condition is developed: for an odd prime $p$ dividing $|\mathcal{B}(n,t,k,k)|$ exactly once, a lattice tiling would force a certain polynomial to lie outside a certain ideal of $\mathbb{F}_p[Y_1,\dots,Y_{\frac{p-1}{2}}]$. Applying this criterion yields congruence conditions on the dimension $n$ that rule out lattice tilings; for $2\le t\le10$ and $1\le k\le10$, a systematic Maple computation over all primes $3\le p\le29$ excludes, on average, $35.65\%$ of all dimensions, with a maximum of $76.69\%$. Finally, we obtain two infinite families of parameters $(n,t,k)$ for which no lattice tiling exists: no lattice tiling exists if $k\equiv4\pmod9$ and the base-$3$ addition of $t$ and $n-1-t$ produces exactly one carry; and no lattice tiling of $\mathbb{Z}^n$ by $\mathcal{B}(n,n-1,k,k)$ exists if $k\equiv8\pmod9$ and $n\equiv2,4\pmod6$. Their sizes are also estimated.
Problem
The paper asks for which parameters lattice tilings of Z^n by symmetric limited magnitude error balls B(n,t,k,k) exist. These tilings correspond to linear perfect codes used in flash memory.
Approach
Generating functions and complete Bell polynomials give an explicit formula for the r-th Q-polynomial of B(n,t,k,k). When an odd prime p divides the ball size exactly once, an ideal-theoretic criterion over F_p is derived as a necessary condition for a tiling. The criterion is applied through Maple computations and through analysis of q-series modulo 3. The proofs, apart from the Maple-dependent parts, were formalized in Lean 4 with Mathlib.
Results
For 2≤t≤10, 1≤k≤10 and primes 3≤p≤29, the criterion excludes on average 35.65% of dimensions, with a maximum of 76.69%. Two infinite nonexistence families are proved: k≡4 (mod 9) when the base-3 addition of t and n-1-t has exactly one carry, and t=n-1, k≡8 (mod 9) with n≡2,4 (mod 6).