Minimum modulus for the unique multiset-sum problem
arXiv:2607.08366
The paper determines the exact smallest modulus N for which a super‑increasing set of residues has a unique size‑n multiset summing to the total, proving N_min(n)=2^n‑2^{⌊log₂ n⌋} and verifying the result in Lean 4, with a conjecture that this bound is optimal.
Abstract
Fix n >= 2. A set A = {a_0 < a_1 < ... < a_{n-1}} of n residues in Z_N is "valid mod N" if the all-ones multiset is the only size-n multiset drawn from A whose sum is p := sum_i a_i (mod N). For the super-increasing set A = {2^k - 1 : 0 <= k <= n-1} we determine the least valid modulus exactly: N_min(n) = 2^n - 2^floor(log_2 n) for all n >= 2. Both directions of the proof are elementary, resting on a sharp minimal-digit-sum estimate for representations by binary coins, and the full theorem has been machine-checked in Lean 4/Mathlib for all n (https://github.com/jarfo/min-modulus). We conjecture that no size-n residue set admits a smaller valid modulus. This validity condition is exactly what makes the permanent of an n x n matrix equal to a single coefficient of a row-product polynomial modulo x^N - 1, extractable by a size-N discrete Fourier (or number-theoretic) transform; the theorem thus identifies the smallest transform, N ~ 2^n, for which this evaluation is exact. That application -- and the resulting common framework for the classical formulas of Ryser and Glynn and this transform -- is developed in a companion paper (arXiv:2607.09949).
8 pages; Lean 4 formalization at https://github.com/jarfo/min-modulus