RepresentationExtraPrime.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The concrete extra-prime parameter and its hashing bounds

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.filterDeficit_mono line 16
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.filterDeficit_nonneg line 22
def OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeRate line 26
Source documentation
This is the manuscript's maximum over the three ordered mixers.
```
def extraPrimeRate (z : Layout n) : ℝ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeRate_max line 29
def OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeParameter line 37
Source documentation
The actual integer sampling parameter, including both floors.
```
def extraPrimeParameter (z : Layout n) : ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeParameter_eq line 41
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeRate_bounds line 49
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeParameter_bounds line 59
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeParameter_range line 82
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrime_density line 94
Source documentation
Rejection sampling in the full bit range has inverse-polynomial density.
```
theorem extraPrime_density (z : Layout n) (hn : 100 ≤ n) :
    1 / (4 * (n : ℝ)) ≤
      ((primeRange (R.extraPrimeParameter z)).card : ℝ) /
        (2 : ℝ) ^ R.extraPrimeParameter z := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.primeRange
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrime_size line 111
Source documentation
Every sampled extra prime has the manuscript's actual size bounds.
```
theorem extraPrime_size (z : Layout n) (hn : 100 ≤ n) {q : ℕ}
    (hq : q ∈ primeRange (R.extraPrimeParameter z)) :
    (2 : ℝ) ^ R.extraPrimeRate z / (inputScale R.input : ℝ) ^ 2 ≤ q ∧
      (q : ℝ) ≤ (2 : ℝ) ^ R.extraPrimeRate z := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.inputScale

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrime_collision line 145

Source documentation

Prime hashing bound with the paper's simplified cubic input-scale factor.

theorem extraPrime_collision (z : Layout n) (hn : 100 ≤ n) (X : Finset ℤ)
    (hbits : ∀ x ∈ X, ∀ y ∈ X, (x - y).natAbs < 2 ^ (2 * inputScale R.input)) :
    PairwiseCollisionBound (primeRange (R.extraPrimeParameter z))
      (primeProbability (R.extraPrimeParameter z)) X
      (fun q x => x % (q : ℤ))
      ((inputScale R.input : ℝ) ^ 3 / (2 : ℝ) ^ R.extraPrimeRate z) := by
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.PairwiseCollisionBound, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.primeProbability

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrime_product_collision line 180
Source documentation
Using the full parent modulus adds no coprimality assumption: a collision modulo its product with q is in particular a collision modulo q.
```
theorem extraPrime_product_collision (z : Layout n) (hn : 100 ≤ n)
    (p0 : ℕ) (X : Finset ℤ)
    (hbits : ∀ x ∈ X, ∀ y ∈ X, (x - y).natAbs < 2 ^ (2 * inputScale R.input)) :
    PairwiseCollisionBound (primeRange (R.extraPrimeParameter z))
      (primeProbability (R.extraPrimeParameter z)) X
      (fun q x => x % ((p0 : ℤ) * q))
      ((inputScale R.input : ℝ) ^ 3 / (2 : ℝ) ^ R.extraPrimeRate z) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.PairwiseCollisionBound, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.primeProbability