SeparatorCoverage.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coverage probability of the actual four-block checker

def OAI.LowSpaceSubsetSum.SeparatorCheck.theta line 16
Source documentation
The one-draw success probability for the prescribed left count.
```
def theta (e c : ℕ) : ℝ :=
…
```
abbrev OAI.LowSpaceSubsetSum.SeparatorCheck.Draws line 19
def OAI.LowSpaceSubsetSum.SeparatorCheck.sampledFamilies line 24
Source documentation
Sample occurrences keep their indices, including repeated subsets.
```
def sampledFamilies {e c : Fin 4 → ℕ} (draws : Draws g e c) :
    Fin 4 → Array (Finset (Fin g)) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.SeparatorCheck.Draws
theorem OAI.LowSpaceSubsetSum.SeparatorCheck.sampled_covered_iff line 28
theorem OAI.LowSpaceSubsetSum.SeparatorCheck.coverage_probability line 49
Source documentation
All four families cover any fixed admissible pair with the paper's 1-4 exp(-10) probability under the actual independent sampling law.
```
theorem coverage_probability (e c : Fin 4 → ℕ) (x y : Record g)
    (heven : 2 ∣ g) (hd : Disjoint x.mask y.mask)
    (hc : ∀ i, (localMask i x.mask).card = c i)
    (hhalf : ∀ i, c i + (localMask i y.mask).card = g / 2)
    (hce : ∀ i, c i ≤ e i) (heg : ∀ i, e i ≤ g)
    (hfeas : ∀ i, e i - c i ≤ g / 2) :
    1 - 4 * Real.exp (-10) ≤ finiteUniformProbability
      (fun draws : Draws g e c => Covered (sampledFamilies draws) x y) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.SeparatorCheck.Record, OAI.LowSpaceSubsetSum.SeparatorCheck.localMask, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.SeparatorCheck.Draws, OAI.LowSpaceSubsetSum.SeparatorCheck.Covered, OAI.LowSpaceSubsetSum.SeparatorCheck.sampledFamilies

theorem OAI.LowSpaceSubsetSum.SeparatorCheck.acceptance_probability line 89

Source documentation

Applying the executable checker preserves this fixed-pair success bound.

theorem acceptance_probability (n : ℕ) (e c : Fin 4 → ℕ) (target : ℤ)
    (xs ys : List (Record g)) (hsize : xs.length + ys.length ≤ 2 ^ n)
    (x y : Record g) (hx : x ∈ xs) (hy : y ∈ ys)
    (hw : x.value + y.value = target)
    (heven : 2 ∣ g) (hd : Disjoint x.mask y.mask)
    (hc : ∀ i, (localMask i x.mask).card = c i)
    (hhalf : ∀ i, c i + (localMask i y.mask).card = g / 2)
    (hce : ∀ i, c i ≤ e i) (heg : ∀ i, e i ≤ g)
    (hfeas : ∀ i, e i - c i ≤ g / 2) :
    1 - 4 * Real.exp (-10) ≤ finiteUniformProbability
      (fun draws : Draws g e c => (run n (sampledFamilies draws) target xs ys).accepted = true) :=
…

Mentions: OAI.LowSpaceSubsetSum.SeparatorCheck.Record, OAI.LowSpaceSubsetSum.SeparatorCheck.localMask, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.SeparatorCheck.Draws, OAI.LowSpaceSubsetSum.SeparatorCheck.run, OAI.LowSpaceSubsetSum.SeparatorCheck.sampledFamilies