MinModulus.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 2 contain sorry, 0 declared as axioms

Minimum modulus for the unique multiset-sum problem

References:

arxiv/2607.08366 Minimum modulus for the unique multiset-sum problem by José A. R. Fonollosa
jarfo/min-modulus, the author's Lean development of the paper's Main Theorem. Section 7 of the paper describes it.

The paper's Main Theorem fixes the super-increasing set $\{2^k - 1\}$ and pins the least modulus at which it is valid. Conjecture 1 says no other set of $n$ residues does better, and is open.

Imports (1)

FormalConjecturesUtil

def Arxiv.«2607.08366».IsValidMod A is valid mod N when the all-ones multiset is the only multiset of size #A drawn from A whose sum matches ∑ a ∈ A, a line 47 source
Source documentation
A is valid mod N when the all-ones multiset is the only multiset of size #A drawn from A whose sum matches ∑ a ∈ A, a.
m a is how many copies of a the multiset uses. The all-ones multiset has m a = 1 for every a ∈ A; values outside A do not affect the sums.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, ZMod
Proof uses: Eq, Finset.sum, Finset.card, HMul.hMul, Membership.mem, OfNat.ofNat
16 instances, coercions and auxiliary constants left out.
```
def IsValidMod (A : Finset (ZMod N)) : Prop :=
…
```
def Arxiv.«2607.08366».minModulus The candidate least modulus admitting a valid set of n residues, conjecturally $2^n - 2^{\lfloor\log_2 n\rfloor}$ line 53 source
Source documentation
The candidate least modulus admitting a valid set of n residues, conjecturally $2^n - 2^{\lfloor\log_2 n\rfloor}$.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HSub.hSub, HPow.hPow, OfNat.ofNat, Nat.log
7 instances, coercions and auxiliary constants left out.
```
def minModulus (n : ℕ) : ℕ := 2 ^ n - 2 ^ (Nat.log 2 n)
…
```
theorem Arxiv.«2607.08366».not_isValidMod_iff Invalidity has a multiplicity witness that differs from one at an element of the set line 57 source
Source documentation
Invalidity has a multiplicity witness that differs from one at an element of the set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, ZMod, Iff, Not, Arxiv.«2607.08366».IsValidMod, Exists, And, Eq, Finset.sum, Finset.card, HMul.hMul, Membership.mem, Ne, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, funext, iff_self
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem not_isValidMod_iff (A : Finset (ZMod N)) :
    ¬ IsValidMod A ↔ ∃ m : ZMod N → ℕ,
      (∑ a ∈ A, m a = #A) ∧ (∑ a ∈ A, (m a : ZMod N) * a = ∑ a ∈ A, a) ∧
        ∃ a ∈ A, m a ≠ 1 := by
…
```
Mentions: Arxiv.«2607.08366».IsValidMod
theorem Arxiv.«2607.08366».minModulus_pos The candidate modulus is positive for every positive set size line 65 source
Source documentation
The candidate modulus is positive for every positive set size.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Arxiv.«2607.08366».minModulus
Proof uses: Nat.sub_pos_of_lt, HPow.hPow, Nat.log, Nat.pow_lt_pow_right, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.log_lt_self, Nat.ne_of_gt
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem minModulus_pos {n : ℕ} (hn : 0 < n) : 0 < minModulus n := by
…
```
Mentions: Arxiv.«2607.08366».minModulus
theorem Arxiv.«2607.08366».minModulus_lt_two_pow The candidate modulus is strictly below the full power of two line 71 source
Source documentation
The candidate modulus is strictly below the full power of two.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Arxiv.«2607.08366».minModulus, HPow.hPow, OfNat.ofNat
Proof uses: Nat.sub_lt, Nat.log, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem minModulus_lt_two_pow (n : ℕ) : minModulus n < 2 ^ n := by
…
```
Mentions: Arxiv.«2607.08366».minModulus
theorem Arxiv.«2607.08366».min_modulus Conjecture 1 (Fonollosa, 2026) sorry line 85 source
Source documentation
Conjecture 1 (Fonollosa, 2026). For every $n \geq 2$ and every $N < 2^n - 2^{\lfloor \log_2 n\rfloor}$, no set of $n$ residues mod $N$ is valid.
Equivalently the super-increasing set $\{2^k - 1 : 0 \leq k \leq n-1\}$ attains the least valid modulus, which is minModulus n.
0 < N excludes N = 0, where ZMod 0 is ℤ rather than a finite modulus and {1, 2} is valid, which would make the statement false for a reason unrelated to the question.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, LT.lt, Arxiv.«2607.08366».minModulus, Finset, ZMod, Eq, Finset.card, Not, Arxiv.«2607.08366».IsValidMod
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem min_modulus :
    answer(sorry) ↔ ∀ n N : ℕ, 2 ≤ n → 0 < N → N < minModulus n →
      ∀ A : Finset (ZMod N), #A = n → ¬ IsValidMod A := by
…
```
Mentions: Arxiv.«2607.08366».minModulus, Arxiv.«2607.08366».IsValidMod
theorem Arxiv.«2607.08366».exists_isValidMod_minModulus sorry line 98 source
depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Finset, ZMod, Arxiv.«2607.08366».minModulus, And, Eq, Finset.card, Arxiv.«2607.08366».IsValidMod
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«2607.08366».one_sum_eq The all-ones multiset always has the right size and the right sum, so IsValidMod is a uniqueness statement rather than an existence one line 105 source
Source documentation
The all-ones multiset always has the right size and the right sum, so IsValidMod is a uniqueness statement rather than an existence one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, ZMod, And, Eq, Finset.sum, OfNat.ofNat, Finset.card, HMul.hMul
Proof uses: And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, Finset.sum_const, mul_one, eq_self, Finset.sum_congr, Eq.refl, Membership.mem, Nat.cast_one, one_mul
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem one_sum_eq (A : Finset (ZMod N)) :
    ∑ _a ∈ A, (1 : ℕ) = #A ∧ ∑ a ∈ A, ((1 : ℕ) : ZMod N) * a = ∑ a ∈ A, a :=
…
```
theorem Arxiv.«2607.08366».isValidMod_of_subsingleton Documented declaration: isValidMod_of_subsingleton line 112 source
Source documentation
A set with fewer than two elements is valid for a silly reason, so the conjecture asks about 2 ≤ n: with #A ≤ 1 the only multiset of size #A drawn from A is the all-ones one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, ZMod, LE.le, Finset.card, OfNat.ofNat, Arxiv.«2607.08366».IsValidMod
Proof uses: Eq, Finset.sum, HMul.hMul, Membership.mem, Singleton.singleton, Iff.mpr, And, Finset.eq_singleton_iff_unique_mem, And.intro, Iff.mp, Finset.card_le_one, Eq.mp, congr, congrArg, Finset.sum_singleton, Finset.card_singleton, Eq.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem isValidMod_of_subsingleton {A : Finset (ZMod N)} (hA : #A ≤ 1) : IsValidMod A := by
…
```
Mentions: Arxiv.«2607.08366».IsValidMod