Amplification.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed repetition schedule

The numerical amplification estimate from the final section of A Low-Space Algorithm for Worst-Case Subset Sum. The per-round failure bound must be proved for the actual trials before this estimate applies.

theorem OAI.LowSpaceSubsetSum.amplification_bound line 19
Source documentation
The failure estimate for u^120 fresh rounds with success at least u^-110. The bound applies to any nonnegative per-round failure probability q below the stated threshold.
```
theorem amplification_bound {u : ℕ} (hu : 2 ≤ u) {q : ℝ}
    (hq0 : 0 ≤ q) (hq : q ≤ 1 - 1 / (u : ℝ) ^ 110) :
    q ^ (u ^ 120) < (1 / 3 : ℝ) := by
…
```