RepresentationBucketBounds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Deterministic capacity bounds for the designated representation buckets

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.spread_deficiency_difference line 16
Source documentation
The executable spread test bounds every deficiency difference.
```
theorem spread_deficiency_difference (z : Layout n)
    (hs : mixerSpreadTest (R.signedWeights z) (R.orderedMixers z) n) (i j : Fin 3) :
    deficiency R.originalWeights (R.orderedMixers z j) -
      deficiency R.originalWeights (R.orderedMixers z i) ≤ (n : ℝ) / 2000 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.mixerSpreadTest, OAI.LowSpaceSubsetSum.deficiency
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrime_entry_gap line 33
Source documentation
The numerical extra-prime margin is derived from the actual spread test.
```
theorem extraPrime_entry_gap (z : Layout n) (g : Guesses n) (hn : 10000 ≤ n)
    (hs : mixerSpreadTest (R.signedWeights z) (R.orderedMixers z) n) :
    (3 / 2000 : ℝ) * n ≤ R.extraPrimeRate z -
      (R.resourceLambda z g - (199 / 1000 : ℝ) * n) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.mixerSpreadTest
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.representation_bucket_loss line 75
Source documentation
The main-branch bit-scale test absorbs the entire polynomial collision loss, with the actual rounded capacity and the strict exponent margin.
```
theorem representation_bucket_loss (z : Layout n) (g : Guesses n) (hn : 20000 ≤ n)
    (hs : mixerSpreadTest (R.signedWeights z) (R.orderedMixers z) n)
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000) :
    4 * (inputScale R.input : ℝ) ^ 203 *
      (2 : ℝ) ^ (R.resourceLambda z g - R.extraPrimeRate z) /
        (compressionDictionaryCapacity n : ℝ) ≤ 1 / 10 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.mixerSpreadTest, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawEntry_mask_spec line 114
Source documentation
Every actual valid entry retains the prescribed top-mask size.
```
theorem rawEntry_mask_spec (z : Layout n) (g : Guesses n) (f : R.Partitions z)
    (B : Fin n → Fin 2 × Fin 4) (j : Fin 2) (e : Entry (Fin n))
    (he : e ∈ RepresentationUniverse.validEntries (R.signedWeights z) (R.rawLeaf z g f B j)) :
    e.mask ⊆ R.orderedMixers z 0 ∧ e.mask.card = representationCount n g (j != 0) 0 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries, OAI.LowSpaceSubsetSum.representationCount

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.left_equalWeight_bound line 132

Source documentation

The equal-weight exponent on the left is bounded by .194736 n.

theorem left_equalWeight_bound (z : Layout n) (g : Guesses n) (f : R.Partitions z)
    (B : Fin n → Fin 2 × Fin 4) (hn : 100 ≤ n) (X : Finset (Entry (Fin n)))
    (hX : X ⊆ RepresentationUniverse.validEntries (R.signedWeights z) (R.rawLeaf z g f B 0))
    (x : Entry (Fin n)) :
    ((sameWeightKeys X Entry.value x).card : ℝ) ≤
      (2 : ℝ) ^ ((24342 / 125000 : ℝ) * n) := by
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries, OAI.LowSpaceSubsetSum.sameWeightKeys

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.left_equalWeight_half_capacity line 162
Source documentation
The actual rounded dictionary capacity leaves half its space for equal weights in the left solution bucket.
```
theorem left_equalWeight_half_capacity (z : Layout n) (g : Guesses n) (f : R.Partitions z)
    (B : Fin n → Fin 2 × Fin 4) (hn : 1000 ≤ n) (X : Finset (Entry (Fin n)))
    (hX : X ⊆ RepresentationUniverse.validEntries (R.signedWeights z) (R.rawLeaf z g f B 0))
    (x : Entry (Fin n)) :
    ((sameWeightKeys X Entry.value x).card : ℝ) ≤ (compressionDictionaryCapacity n : ℝ) / 2 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries, OAI.LowSpaceSubsetSum.sameWeightKeys, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.right_fullMask_half_capacity line 180
Source documentation
At a full right-mask prefix, at most one exact key has the chosen weight.
```
theorem right_fullMask_half_capacity (X : Finset (Entry (Fin n))) (w : ℤ)
    (D : Finset (Fin n)) (hn : 1000 ≤ n) :
    ((X.filter fun e => e.value = w ∧ e.mask = D).card : ℝ) ≤
      (compressionDictionaryCapacity n : ℝ) / 2 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity