Buckets.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Equal-weight records and exact dictionary capacities

An additional prime can distinguish unequal weights, but cannot distinguish different masks of equal weight. These deterministic bounds handle that case, including the full-mask endpoint of the right-prefix refinement.

instance OAI.LowSpaceSubsetSum.(instance at line 19) line 19
theorem OAI.LowSpaceSubsetSum.same_weight_card_le_masks line 25
Source documentation
Equal-weight records are uniquely identified by their top masks.
```
theorem same_weight_card_le_masks (U : Finset (Entry ι)) (x : ℤ) :
    (U.filter fun e => e.value = x).card ≤ (U.image Entry.mask).card := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry

theorem OAI.LowSpaceSubsetSum.same_weight_card_le_choose line 42

Source documentation

Prescribed mask size bounds all equal-weight records by a binomial count.

theorem same_weight_card_le_choose (U : Finset (Entry ι)) (top : Finset ι)
    (k : ℕ) (hmask : ∀ e ∈ U, e.mask ⊆ top ∧ e.mask.card = k) (x : ℤ) :
    (U.filter fun e => e.value = x).card ≤ top.card.choose k := by
…

Mentions: OAI.LowSpaceSubsetSum.Entry

theorem OAI.LowSpaceSubsetSum.full_mask_same_weight_card_le_one line 55
Source documentation
Fixing both the exact weight and the entire mask leaves at most one key.
```
theorem full_mask_same_weight_card_le_one (U : Finset (Entry ι))
    (x : ℤ) (D : Finset ι) :
    (U.filter fun e => e.value = x ∧ e.mask = D).card ≤ 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry
theorem OAI.LowSpaceSubsetSum.bucket_card_le_of_parts line 69
Source documentation
The complete bucket fits when both its equal- and unequal-weight parts fit. This counts keys, rather than raw tuples producing those keys.
```
theorem bucket_card_le_of_parts (U : Finset (Entry ι)) (x : ℤ) (C A B : ℕ)
    (hneq : (U.filter fun e => e.value ≠ x).card ≤ A)
    (heq : (U.filter fun e => e.value = x).card ≤ B) (hcap : A + B ≤ C) :
    U.card ≤ C := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry