ParameterSelection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The outer error parameters are fixed before the latent gadget or its alphabet. We use the same positive reciprocal integer for the latent noise budget and the rounding tolerance. This permitted specialization makes uniform occurrence rounding an exact fixed-copy operation. The later parity error is chosen only after the tuple length has been fixed.

structure OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters line 19
theorem OAI.UniqueGamesTheorem.ParameterSelection.exists_outerParameters line 37
Source documentation
Choose the alphabet-independent exponent and both rational budgets using only the two prescribed real errors.
```
theorem exists_outerParameters (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    Nonempty (OuterParameters ε δ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters
def OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters.pStar line 54
theorem OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters.pStar_pos line 56
theorem OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters.pStar_lt_one line 58
theorem OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters.exists_parity_error line 61
theorem OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters.matrix_error_budget line 80
Source documentation
Both matrix-test completeness losses fit the budget fixed before the alphabet, for the later chosen positive tuple length.
```
theorem matrix_error_budget (k : ℕ) (hk : 0 < k) (ξ : ℚ)
    (hξ : ξ ≤ P.epsilon0 / (2 * k * P.repetitions)) :
    (k : ℚ) * ξ + P.pStar / 2 ≤ P.epsilon0 / P.repetitions := by
…
```