Minimum modulus for the unique multiset-sum problem
José A. R. Fonollosa
math.CO
Jul 9, 2026 · v1
TL;DR
The main theorem (both bounds) determining the least valid modulus for the super-increasing set is formalized and kernel-checked in Lean 4/Mathlib.
Abstract
Fix $n \ge 2$. A set $A = \{a_0 < a_1 < \dots < 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 \pmod N$. For the super-increasing set $A = \{2^k - 1 : 0 \le k \le n-1\}$ we determine the least valid modulus exactly: $\Nmin(n) = 2^{\,n} - 2^{\lfloor \log_2 n \rfloor}$ for all $n \ge 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 \times 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 \approx 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 [2].
Problem
A set of n residues in Z_N is 'valid' if the all-ones multiset is the only size-n multiset from it summing to the total mod N. The goal is to determine the least valid modulus for the super-increasing set A = {2^k - 1 : 0 ≤ k ≤ n-1}, which controls the transform size for an exact permanent evaluation.
Approach
The validity condition is reduced to a statement about representations by binary coins with fixed digit sum. A sharp minimal-digit-sum lemma (via greedy representations and popcount) yields an upper bound by an induction on multiples with no case analysis. A master achievability criterion and explicit witness construction give the matching lower bound. The full Main Theorem for all n ≥ 2 is formalized and kernel-checked in Lean 4 with Mathlib, using no unproven assumptions beyond Mathlib's standard axioms.
Results
For every n ≥ 2 the least valid modulus is N_min(n) = 2^n - 2^{⌊log₂ n⌋}. The Lean statement nmin_eq certifies this as the least element of the valid set, with the step lemma formalized as gmin_step and the four lower-bound witnesses constructed directly.