Minimum modulus for the unique multiset-sum problem

Formalization of the paper Minimum modulus for the unique multiset-sum problem, with an application to computing the permanent (J. A. R. Fonollosa, 2026) for the super-increasing set A = {2^i − 1 : 0 ≤ i < n}.

Everything is stated in k-space (the paper's k = c + 1 variables), over ℕ: a candidate multiset is k : ℕ → ℕ with digit sum ∑_{i<n} k i = n, and validity mod N says the only such k with ∑ k_i·a_i ≡ ∑ a_i [MOD N] is all-ones. The paper's signed multiples V = ±jN enter only through the congruence M ≡ 2^n − 1 [MOD N] on M = ∑ k_i 2^i, so no integers appear.

Contents:

• definitions: a, dsum, val, Supp, Valid
• representation constructors (existence half of the paper's master achievability criterion, Prop. 1): ones_rep, ones_erase_rep, exists_rep_le, exists_rep_lt, exists_rep_compl, and contiguity dsum_succ_of_lt / exists_dsum_eq
• theoremB (paper §6, optimality / lower bound) — complete
• gmin and the greedy minimality bound gmin_le_dsum (paper Lemma 3, downward half), the step lemma gmin_step (paper Lemma 4) and the j-induction bound slack (popcount-free, no range restriction)
• ones_unique (paper Lemma 2)
• theoremA (paper §5, validity / upper bound) — complete
• nmin_eq — the main theorem Nmin(n) = 2^n − 2^⌊log₂ n⌋ — complete, no axioms beyond propext / Classical.choice / Quot.sound

def MinModulus.a (i : ℕ) : ℕ

The super-increasing set: a i = 2^i − 1.

Equations

• MinModulus.a i = 2 ^ i - 1

def MinModulus.dsum (n : ℕ) (k : ℕ → ℕ) : ℕ

Digit sum of k on [0, n).

Equations

• MinModulus.dsum n k = ∑ i ∈ Finset.range n, k i

def MinModulus.val (n : ℕ) (k : ℕ → ℕ) : ℕ

Value of k on [0, n) with power-of-two coins (paper: M = Σ k_i 2^i).

Equations

• MinModulus.val n k = ∑ i ∈ Finset.range n, k i * 2 ^ i

def MinModulus.Supp (n : ℕ) (k : ℕ → ℕ) : Prop

k is supported on [0, n).

Equations

• MinModulus.Supp n k = ∀ (i : ℕ), n ≤ i → k i = 0

def MinModulus.Valid (n N : ℕ) : Prop

Validity mod N (paper §2, problem statement): the all-ones vector is the only size-n multiset drawn from A whose sum is ≡ Σ a_i (mod N).

Equations

• MinModulus.Valid n N = ∀ (k : ℕ → ℕ), MinModulus.dsum n k = n → ∑ i ∈ Finset.range n, k i * MinModulus.a i ≡ ∑ i ∈ Finset.range n, MinModulus.a i [MOD N] → ∀ i < n, k i = 1

Basic identities

theorem MinModulus.sum_two_pow (w : ℕ) : ∑ i ∈ Finset.range w, 2 ^ i = 2 ^ w - 1

theorem MinModulus.sum_a_add_dsum (n : ℕ) (k : ℕ → ℕ) : ∑ i ∈ Finset.range n, k i * a i + dsum n k = val n k

The paper's Σ k_i a_i = M − Σ k_i identity, subtraction-free.

theorem MinModulus.not_valid_of_witness {n N M : ℕ} (hn : 1 ≤ n) (hne : M ≠ 2 ^ n - 1) (hmod : M ≡ 2 ^ n - 1 [MOD N]) (h : ∃ (k : ℕ → ℕ), val n k = M ∧ dsum n k = n) : ¬Valid n N

To refute validity it suffices to exhibit k with digit sum n and value M ≠ 2^n − 1 congruent to 2^n − 1 mod N.

Padding and top-coin composition

theorem MinModulus.supp_mono {e w : ℕ} (h : e ≤ w) {k : ℕ → ℕ} (hs : Supp e k) : Supp w k

theorem MinModulus.val_pad {e w : ℕ} (h : e ≤ w) {k : ℕ → ℕ} (hs : Supp e k) : val w k = val e k

theorem MinModulus.dsum_pad {e w : ℕ} (h : e ≤ w) {k : ℕ → ℕ} (hs : Supp e k) : dsum w k = dsum e k

theorem MinModulus.update_top (w c : ℕ) (k : ℕ → ℕ) (hs : Supp w k) : Supp (w + 1) (Function.update k w c) ∧ val (w + 1) (Function.update k w c) = val w k + c * 2 ^ w ∧ dsum (w + 1) (Function.update k w c) = dsum w k + c

Put c coins on the top index w of a representation supported below w.

def MinModulus.shift (c : ℕ) (k : ℕ → ℕ) : ℕ → ℕ

Shift a representation up one index, placing c at index 0.

Equations

• MinModulus.shift c k i = if i = 0 then c else k (i - 1)

theorem MinModulus.shift_supp {w c : ℕ} {k : ℕ → ℕ} (h : Supp w k) : Supp (w + 1) (shift c k)

theorem MinModulus.shift_val (w c : ℕ) (k : ℕ → ℕ) : val (w + 1) (shift c k) = 2 * val w k + c

theorem MinModulus.shift_dsum (w c : ℕ) (k : ℕ → ℕ) : dsum (w + 1) (shift c k) = dsum w k + c

Explicit representations (bases of the four witness families, paper §6)

theorem MinModulus.ones_rep (w : ℕ) : ∃ (k : ℕ → ℕ), Supp w k ∧ val w k = 2 ^ w - 1 ∧ dsum w k = w

The all-ones representation of 2^w − 1.

theorem MinModulus.ones_erase_rep {w e : ℕ} (he : e < w) : ∃ (k : ℕ → ℕ), Supp w k ∧ val w k = 2 ^ w - 1 - 2 ^ e ∧ dsum w k = w - 1

All-ones minus bit e: represents 2^w − 1 − 2^e with w − 1 coins.

theorem MinModulus.exists_rep_le (w x : ℕ) : x < 2 ^ w → ∃ (k : ℕ → ℕ), Supp w k ∧ val w k = x ∧ dsum w k ≤ w

Any x < 2^w has a representation on [0, w) with digit sum ≤ w.

theorem MinModulus.exists_rep_lt (w x : ℕ) : x < 2 ^ w - 1 → ∃ (k : ℕ → ℕ), Supp w k ∧ val w k = x ∧ dsum w k ≤ w - 1

Sharp version (paper §6, case (i)): x < 2^w − 1 needs at most w − 1 coins.

theorem MinModulus.exists_rep_compl (w s : ℕ) : s < 2 ^ w → s ≠ 0 → (¬∃ (e : ℕ), s = 2 ^ e) → ∃ (k : ℕ → ℕ), Supp w k ∧ val w k = 2 ^ w - 1 - s ∧ dsum w k ≤ w - 2

Complement representation (paper §6, case (iii)): if 0 ≠ s < 2^w is not a power of two, then 2^w − 1 − s needs at most w − 2 coins.

Contiguity (paper Lemma 3, upward direction)

theorem MinModulus.dsum_succ_of_lt {n M s : ℕ} (h : ∃ (k : ℕ → ℕ), val n k = M ∧ dsum n k = s) (hlt : s < M) : ∃ (k : ℕ → ℕ), val n k = M ∧ dsum n k = s + 1

Splitting step: a representation of M with digit sum s < M yields one with digit sum s + 1 (replace a coin 2^i, i ≥ 1, by two 2^{i-1}s).

theorem MinModulus.exists_dsum_eq {n M t : ℕ} (h : ∃ (k : ℕ → ℕ), val n k = M ∧ dsum n k ≤ t) (htM : t ≤ M) : ∃ (k : ℕ → ℕ), val n k = M ∧ dsum n k = t

From digit sum ≤ t to digit sum exactly t, provided t ≤ M (the paper's interval [s_min, M] of achievable digit sums).

Small arithmetic helpers

theorem MinModulus.succ_le_two_pow_pred (n : ℕ) : 3 ≤ n → n + 1 ≤ 2 ^ (n - 1)

Theorem B: optimality (paper §6)

theorem MinModulus.theoremB {n N : ℕ} (hn : 2 ≤ n) (hN2 : 2 ≤ N) (hNlt : N < 2 ^ n - 2 ^ Nat.log 2 n) : ¬Valid n N

Theorem B (lower bound): every modulus 2 ≤ N < 2^n − 2^⌊log₂ n⌋ is invalid for the super-increasing set. The four witness families of the paper: (i) N < 2^{n-1} — M = 2^n − 1 + N; (ii) N = 2^{n-1} — M = 2^{n-1} − 1 (a negative multiple, V = −N); (iii) gap s := 2^n − N not a power of two — M = 2^n − 1 + N; (iv) gap s = 2^e, ⌊log₂ n⌋ < e ≤ n−2 — M = 2^e − 1 (again V = −N), where 2^e − 1 ≥ n is exactly e > ⌊log₂ n⌋.

The greedy digit-sum lower bound (paper Lemma 3, minimality half)

gmin w M is the digit sum of the greedy representation of M with coins 2^0, …, 2^w: the binary digits of M below bit w plus the whole quotient ⌊M/2^w⌋ on the top coin. Everything is proved by induction on w, peeling one bit per step, so only literal /2 and %2 appear — omega-friendly. The step lemma gmin_step (paper Lemma 4) replaces the paper's popcount identities: slack iterates it over j, with no range restriction.

def MinModulus.gmin : ℕ → ℕ → ℕ

Greedy digit sum with coins 2^0..2^w (w+1 coin types).

Equations

• MinModulus.gmin 0 x✝ = x✝
• MinModulus.gmin w.succ x✝ = x✝ % 2 + MinModulus.gmin w (x✝ / 2)

theorem MinModulus.gmin_add_le (w x t : ℕ) : gmin w (x + t) ≤ gmin w x + t

Adding t to the target raises the greedy digit sum by at most t.

theorem MinModulus.gmin_add_pow (w X : ℕ) : gmin w (X + 2 ^ w) = gmin w X + 1

Adding the top coin raises the greedy digit sum by exactly 1.

theorem MinModulus.gmin_ones (w : ℕ) : gmin w (2 ^ (w + 1) - 1) = w + 1

Greedy digit sum of the all-ones target: gmin w (2^{w+1} − 1) = w + 1.

theorem MinModulus.gmin_step (w t M M' : ℕ) : t ≤ w → M' + 2 ^ t = M + 2 ^ (w + 1) → gmin w M + 1 ≤ gmin w M'

Step lemma (paper §5, Lemma 4): adding 2^{w+1} − 2^t (t ≤ w; subtraction encoded as M' + 2^t = M + 2^{w+1}) raises the greedy digit sum by at least 1. Induction on w, peeling one bit: for t ≥ 1 both sides keep their parity and the shifted instance is (w−1, t−1); for t = 0 the parity flips, and the odd-M branch pays two top coins via gmin_add_pow.

theorem MinModulus.slack {w t N : ℕ} (ht : t ≤ w) (hN : N + 2 ^ t = 2 ^ (w + 1)) (j : ℕ) : w + 1 + j ≤ gmin w (2 ^ (w + 1) - 1 + j * N)

Slack bound (paper §5): by induction on j from the step lemma, the positive-multiple target 2^{w+1} − 1 + j·N at a power-of-two gap (N + 2^t = 2^{w+1}, t ≤ w) has greedy digit sum at least w + 1 + j — the paper's s_min(M_j) ≥ n + j, for every j.

theorem MinModulus.unshift_val (w : ℕ) (k : ℕ → ℕ) : val (w + 1) k = k 0 + 2 * val w fun (i : ℕ) => k (i + 1)

Peel index 0 off a value (inverse of shift_val).

theorem MinModulus.unshift_dsum (w : ℕ) (k : ℕ → ℕ) : dsum (w + 1) k = k 0 + dsum w fun (i : ℕ) => k (i + 1)

Peel index 0 off a digit sum (inverse of shift_dsum).

theorem MinModulus.dsum_le_val (n : ℕ) (k : ℕ → ℕ) : dsum n k ≤ val n k

Each unit of digit sum contributes a coin worth at least 1.

theorem MinModulus.val_le_dsum_mul (n : ℕ) (k : ℕ → ℕ) : val n k ≤ dsum n k * 2 ^ (n - 1)

Each unit of digit sum contributes a coin worth at most 2^{n-1}.

theorem MinModulus.gmin_le_dsum (w : ℕ) (k : ℕ → ℕ) : gmin w (val (w + 1) k) ≤ dsum (w + 1) k

Greedy minimality (paper Lemma 3, downward half): the digit sum of any representation is at least the greedy digit sum of its value. Induction on the width: split the bottom coin k 0 = M % 2 + 2t; the 2t surplus carries up into the shifted representation, and gmin_add_le absorbs it.

theorem MinModulus.ones_unique (n : ℕ) (k : ℕ → ℕ) : val n k = 2 ^ n - 1 → dsum n k = n → ∀ i < n, k i = 1

Lemma 2 (paper §3): the all-ones vector is the only representation of 2^n − 1 with digit sum n. Descent on the bottom coin: parity forces k 0 = 1 + 2t, and the greedy bound on the shifted representation forces t = 0; recurse.

Theorem A and the main theorem

theorem MinModulus.theoremA {n : ℕ} (hn : 2 ≤ n) : Valid n (2 ^ n - 2 ^ Nat.log 2 n)

Theorem A (upper bound, paper §5): the super-increasing set is valid at N = 2^n − 2^⌊log₂ n⌋. Pass to M = val n k ≡ 2^n − 1 [MOD N] and split: M < 2^n − 1 falls below the floor (2^m ≤ n — the only place ⌊log₂⌋ enters); M = 2^n − 1 is ones_unique; and M = 2^n − 1 + jN has greedy digit sum at least n + j > n by slack — uniformly in j ≥ 1 and n ≥ 2, with no range restriction and no small-n cases.

theorem MinModulus.nmin_eq {n : ℕ} (hn : 2 ≤ n) : IsLeast {N : ℕ | 2 ≤ N ∧ Valid n N} (2 ^ n - 2 ^ Nat.log 2 n)

Main theorem: Nmin(n) = 2^n − 2^⌊log₂ n⌋ — it is valid there, and every smaller modulus (≥ 2) is invalid. (Modulo theoremA.)