Minimum modulus for the unique multiset-sum problem
José A. R. Fonollosa
math.CO
Jul 9, 2026 · v2
TL;DR
The full Main Theorem determining the least valid modulus for the unique multiset-sum problem is formalized and kernel-checked in Lean 4/Mathlib.
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).
Problem
For the super-increasing set A = {2^k - 1} of n residues in Z_N, determine the least modulus N for which the all-ones multiset is the unique size-n multiset summing to the target. This validity condition governs the smallest transform for exact permanent evaluation.
Approach
The problem is reduced to representations by binary coins with fixed digit sum. A sharp minimal-digit-sum lemma and a single-step estimate drive an induction proving the upper bound (validity at N = 2^n - 2^{floor(log2 n)}), while explicit collisions establish the lower bound. The full Main Theorem (both directions, for all n >= 2) is formalized in Lean 4 with Mathlib, with the greedy digit sum defined by a bit-peeling recursion and the step lemma as gmin_step; the statement nmin_eq is kernel-checked with only Mathlib's standard axioms.
Results
The least valid modulus is exactly N_min(n) = 2^n - 2^{floor(log2 n)} for all n >= 2, machine-checked in Lean. A companion result shows elementary abelian 2-groups (Z_2)^{n-1} of smaller order also admit unique-multiset-sum families, so no cyclic group is optimal.