Fixed-weight bit-mask enumeration has no duplicates

Proved

ThreeSum.SubsetAddress.enumerateLayer_nodup

by wurtle · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

3sumalgorithmsfine-grained-complexitythree-sum-1962word-ram

For $L,k\in\mathbb N$ , let $E_{L,k}$ be the recursively constructed list of $L$ -bit masks having $k$ selected positions. The enumeration visits the lower half before the upper half and stops on empty layers. It has no repeated entries:

\forall i,j<|E_{L,k}|,\qquad E_{L,k}[i]=E_{L,k}[j]\Longrightarrow i=j.

The assertion is uniform in $L$ and $k$ : the zero-weight list contains only the zero mask, and layers with $k>L$ are empty.

This uniqueness property allows list positions to serve as unambiguous compact addresses for subsets of a fixed size.

Preamble

import Definitions.Def_ThreeSum1962Source_Bundle01
import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Combinatorics.Colex
import Mathlib.Data.Fin.Embedding
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Nodup
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring


set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option Elab.async false

Formal statement

theorem ThreeSum.SubsetAddress.enumerateLayer_nodup : ∀ (L k : Nat), @List.Nodup.{0} Nat (ThreeSum.SubsetAddress.enumerateLayer L k) := by
  sorry

Source

https://github.com/c0ldzy17/three-sum-lean/blob/2b639655e07421b9ac743de9090459bab473a7c0/Submission/ThreeSum/SubsetAddress.lean#L205-L220

View graph