AmplificationIteration.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The finite iteration and size arithmetic for an amplification transformation. The transformation itself must be supplied by the actual graph construction; these theorems do not assert that such a transformation exists. In particular, the polynomial size estimate below is not a machine runtime certificate.

def OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.run line 19
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.min_double_min line 23
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.run_gap line 31
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.run_preserves line 46
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.run_size line 53
def OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.rounds line 63
Source documentation
A concrete logarithmic iteration count, including the zero input.
```
def rounds (n : Nat) : Nat := Nat.log2 n + 1
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.rounds_large line 65
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.rounds_power_le line 69
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.blowup_rounds_le line 75
Source documentation
The constant blowup raised to the actual iteration count is polynomial in n.
```
theorem blowup_rounds_le {C degree n : Nat} (hn : 0 < n) (hC : C ≤ 2 ^ degree) :
    C ^ rounds n ≤ (2 * n) ^ degree := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.rounds
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.run_size_polynomial line 83
theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.run_reaches_cap line 91
Source documentation
An inverse-size initial gap reaches the fixed threshold after the concrete loop.
```
theorem run_reaches_cap {X : Type*} (step : X → X) (gap : X → ℝ)
    (cap : ℝ) (hc : 0 ≤ cap) (hc1 : cap ≤ 1)
    (amplifies : ∀ x, min (2 * gap x) cap ≤ gap (step x))
    (n : Nat) (x : X) (hg : 0 ≤ gap x) (hstart : 1 ≤ (n : ℝ) * gap x) :
    cap ≤ gap (run step (rounds n) x) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.run, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationIteration.rounds