The rank within a fixed subset layer is injective

Proved

ThreeSum.SubsetAddress.layerRank_injective

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

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

Let $L,k,m,n$ be natural numbers. Assume $m$ and $n$ encode subsets of $\{0,\ldots,L-1\}$ of cardinality $k$ ; equivalently, both integers are less than $2^L$ and have exactly $k$ set bits. Let $\rho_{L,k}$ denote the recursive rank within this fixed-cardinality layer, with masks lacking the highest bit placed before masks containing it. Then

\rho_{L,k}(m)=\rho_{L,k}(n)\quad\Longrightarrow\quad m=n.

Thus a layer rank uniquely identifies its valid subset mask, as required for compact subset addressing.

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
import Theorems.Thm_ThreeSum_SubsetAddress_layerRank_lt


set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option Elab.async false

Formal statement

theorem ThreeSum.SubsetAddress.layerRank_injective : ∀ {L k m n : Nat} (hm : ThreeSum.SubsetAddress.IsMask L k m) (hn : ThreeSum.SubsetAddress.IsMask L k n)
  (he : @Eq.{1} Nat (ThreeSum.SubsetAddress.layerRank L k m) (ThreeSum.SubsetAddress.layerRank L k n)), @Eq.{1} Nat m n := by
  sorry

Source

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

View graph