Representatives.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Many distinct weights at one prescribed cardinality

The first representative-selection step in the low-deficiency survival proof. Complementation allows the selected cardinality to be at most half the domain. All cardinalities count distinct integer weights, not subset occurrences.

def OAI.LowSpaceSubsetSum.sumsAtSize line 23
theorem OAI.LowSpaceSubsetSum.mem_sumsAtSize line 26
theorem OAI.LowSpaceSubsetSum.weight_complement line 31
theorem OAI.LowSpaceSubsetSum.sumsAtSize_complement line 41
theorem OAI.LowSpaceSubsetSum.sumsAtSize_complement_card line 62
theorem OAI.LowSpaceSubsetSum.distinctSumCount_le_sum_sizes line 70
theorem OAI.LowSpaceSubsetSum.exists_many_distinct_weights_at_size line 83
Source documentation
Pigeonhole selection of one size, followed by complementation if necessary.
```
theorem exists_many_distinct_weights_at_size (a : ι → ℤ) (V : Finset ι) :
    ∃ k ≤ V.card / 2,
      distinctSumCount a V ≤ (V.card + 1) * (sumsAtSize a V k).card := by
…
```
Mentions: OAI.LowSpaceSubsetSum.distinctSumCount, OAI.LowSpaceSubsetSum.sumsAtSize
theorem OAI.LowSpaceSubsetSum.two_pow_card_sub_deficiency line 99
Source documentation
The exact exponential form of the distinct-weight count.
```
theorem two_pow_card_sub_deficiency (a : ι → ℤ) (V : Finset ι) :
    (2 : ℝ) ^ ((V.card : ℝ) - deficiency a V) = distinctSumCount a V := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency, OAI.LowSpaceSubsetSum.distinctSumCount
theorem OAI.LowSpaceSubsetSum.exists_representative_size line 105
Source documentation
The representation proof's first distinct-weight lower bound.
```
theorem exists_representative_size (a : ι → ℤ) (V : Finset ι) :
    ∃ k ≤ V.card / 2,
      (2 : ℝ) ^ ((V.card : ℝ) - deficiency a V) / (V.card + 1) ≤
        (sumsAtSize a V k).card := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency, OAI.LowSpaceSubsetSum.sumsAtSize
theorem OAI.LowSpaceSubsetSum.sumsAtSize_card_le_third_entropy line 119
Source documentation
Subsets of size at most one third cannot supply more than the corresponding entropy bound, regardless of repeated values in the input.
```
theorem sumsAtSize_card_le_third_entropy (a : ι → ℤ) (V : Finset ι) {k : ℕ}
    (hV : 0 < V.card) (hk : 3 * k ≤ V.card) :
    ((sumsAtSize a V k).card : ℝ) ≤
      (2 : ℝ) ^ ((V.card : ℝ) * binaryEntropy (1 / 3)) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.sumsAtSize, OAI.LowSpaceSubsetSum.binaryEntropy
theorem OAI.LowSpaceSubsetSum.exists_representative_size_range line 142
Source documentation
Once a block supplies enough distinct sums, the size selected by pigeonhole lies strictly above one third of that block and at most one half. These are exactly the guesses used by the representation trial.
```
theorem exists_representative_size_range (a : ι → ℤ) (V : Finset ι)
    (hV : 0 < V.card)
    (hcount : (2 : ℝ) ^ ((V.card : ℝ) * binaryEntropy (1 / 3)) <
      (distinctSumCount a V : ℝ) / (V.card + 1)) :
    ∃ k, V.card < 3 * k ∧ k ≤ V.card / 2 ∧
      (distinctSumCount a V : ℝ) / (V.card + 1) ≤ (sumsAtSize a V k).card := by
…
```
Mentions: OAI.LowSpaceSubsetSum.binaryEntropy, OAI.LowSpaceSubsetSum.distinctSumCount, OAI.LowSpaceSubsetSum.sumsAtSize

theorem OAI.LowSpaceSubsetSum.eventually_small_deficiency_size_range line 157

Source documentation

The small-deficiency regime eventually excludes the lower third. The margin 1/1500 is absolute, so this assertion is uniform in the weights.

theorem eventually_small_deficiency_size_range :
    ∀ᶠ m : ℕ in Filter.atTop, ∀ (a : ι → ℤ) (V : Finset ι), V.card = m →
      deficiency a V ≤ (33 / 500 : ℝ) * m →
      ∃ k, V.card < 3 * k ∧ k ≤ V.card / 2 ∧
        (2 : ℝ) ^ ((V.card : ℝ) - deficiency a V) / (V.card + 1) ≤
          (sumsAtSize a V k).card := by
…

Mentions: OAI.LowSpaceSubsetSum.deficiency, OAI.LowSpaceSubsetSum.sumsAtSize

theorem OAI.LowSpaceSubsetSum.half_mixer_deficiency_threshold line 195
Source documentation
The manuscript's absolute threshold makes tau = .0078n at most .066s for every size-s mixer half; the floor in m is included.
```
theorem half_mixer_deficiency_threshold {n : ℕ} (hn : 2200 ≤ n) :
    (39 / 5000 : ℝ) * n ≤ (33 / 500 : ℝ) * (mixerSize n / 2 : ℕ) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize