OAI/Computability/UniqueGames/Reduction/FinalParametersLemmas.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Existence of the finite numerical choices in Section 4.1. All errors and search tests here are rational, including the fourth-power test in (4.1).

  1. def OAI.UniqueGamesTheorem.Integration.FinalParameters.rho line 23
  2. def OAI.UniqueGamesTheorem.Integration.FinalParameters.levelConstant line 24
  3. def OAI.UniqueGamesTheorem.Integration.FinalParameters.alpha line 25
  4. def OAI.UniqueGamesTheorem.Integration.FinalParameters.beta line 26
  5. def OAI.UniqueGamesTheorem.Integration.FinalParameters.theta line 27
  6. def OAI.UniqueGamesTheorem.Integration.FinalParameters.repetitionRate line 28
  7. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.levelConstant_pos line 30
  8. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.rho_pos line 34
  9. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.theta_pos line 38
  10. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.repetitionRate_bounds line 43
  11. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.exists_symbol_dimension line 48

    Source documentation

    Selecting the exponent as a multiple of four supplies an exact rational fourth root. No approximation of a real root enters the parameter search.

    theorem exists_symbol_dimension (r : Nat) {δ : ℚ} (hδ : 0 < δ) :
    ∃ s : Nat, r + 1 < s ∧ ∃ u : ℚ,
      0 < u ∧ u ^ 4 = rho r s ∧ levelConstant r * u ≤ δ / 8 := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.FinalParameters.rho, OAI.UniqueGamesTheorem.Integration.FinalParameters.levelConstant

  12. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.exists_repetition_and_dimension line 66

    Source documentation

    The repetition length is chosen first; the comparison dimension is then large enough for both the subset experiment and its squared error bound.

    theorem exists_repetition_and_dimension (L q : Nat) {θ : ℚ}
    (hθ : 0 < θ) (hq : 0 < q) :
    ∃ t k : Nat, 0 < t ∧ t ≤ k ∧
      (1 - zeroProbability L * (1 - repetitionRate)) ^ t < decoderThreshold θ q ∧
      16 * (t : ℚ) ^ 2 * 2 ^ (t * L) ≤ (k : ℚ) * θ ^ 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.FinalParameters.repetitionRate

  13. def OAI.UniqueGamesTheorem.Integration.FinalParameters.gamma line 83
  14. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.gamma_bounds line 85
  15. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.exists_source_error line 95
  16. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.exists_parameters line 104
  17. theorem OAI.UniqueGamesTheorem.Integration.FinalParameters.completeness_budget line 129

    Source documentation

    The completeness budget uses the same comparison dimension as the other parameters. This identity is exact, without rounding of rational errors.

    theorem completeness_budget {ε : ℚ} {k : Nat} (hk : 0 < k) :
    (k : ℚ) * gamma ε k + (ε / 2) / 2 = ε / 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.FinalParameters.gamma

  18. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.rho_eq_two_div_pow line 149
  19. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.rho_real_eq_two_div_pow line 156
  20. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.beta_eq_div line 160
  21. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.theta_real_product line 168

    Source documentation

    The exact signal threshold used by selection, expressed in real scalars. There is no loss between the rational parameter search and this product.

    theorem theta_real_product (δ : ℚ) (r s : Nat) :
    (theta δ r s : ℝ) =
      ((δ : ℝ) / (8 * (2 : ℝ) ^ s * 2 ^ (s * s))) *
        ((rho r s : ℝ) / (2 * (2 : ℝ) ^ (r * s))) := by
…
  22. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.fourth_root_as_rpow line 174
  23. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.exists_symbol_dimension_real line 181
  24. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.kernelProbability_real line 191

    Source documentation

    Casting the finite experiment changes only its scalar values, retaining the same noise indices and the same event.

    theorem kernelProbability_real {s d : Nat}
    (g : UniqueGamesTheorem.Reduction.ActualSource.SplitGadget s d)
    {P : Type} [AddCommGroup P] [Module F2 P] [DecidableEq P]
    (S : (Vector s × Vector d) →ₗ[F2] P) :
    (SplitGadget.kernelProbability g S : ℝ) =
      Finset.univ.expect (fun i => if S (g.noise i) = 0 then (1 : ℝ) else 0) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.SplitGadget, OAI.UniqueGamesTheorem.Integration.SplitGadget.kernelProbability

  25. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.kernelProbability_real_le line 205
  26. theorem OAI.UniqueGamesTheorem.Integration.RealBounds.comparison_square_budget line 215
  27. def OAI.UniqueGamesTheorem.Integration.SourceParameters.rate line 232
  28. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.rate_bounds line 234
  29. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.fourth_power_comparison line 240
  30. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.four_bit_rate_comparison line 259

    Source documentation

    The answer alphabet product is 16, so its binary logarithm is four. This converts the genuine repetition theorem's real exponent to a rational base raised to the integral repetition length.

    theorem four_bit_rate_comparison {gap : ℚ}
    (hgap : 0 < gap) (hgap1 : gap ≤ 1) (n : Nat) :
    (1 - (gap : ℝ) ^ 3 / 6000) ^ ((n : ℝ) / 4) ≤ (rate gap : ℝ) ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.SourceParameters.rate

  31. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.logTwo_sixteen line 274
  32. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.game_repetition_rate line 282

    Source documentation

    The actual finite game's repetition rate, with its answer cardinality checked as an ordinary finite count. No repetition estimate is assumed.

    theorem game_repetition_rate {Q₁ Q₂ A₁ A₂ : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A₁] [Fintype A₂]
    [Nonempty A₁] [Nonempty A₂] [DecidableEq Q₁] [DecidableEq Q₂]
    (G : UniqueGamesTheorem.Foundations.Games.Game Q₁ Q₂ A₁ A₂)
    {gap : ℚ} (hgap : 0 < gap) (hgap1 : gap ≤ 1)
    (hcards : Fintype.card A₁ * Fintype.card A₂ = 16)
    (hvalue : G.value ≤ 1 - (gap : ℝ)) (n : Nat) :
    (G.repetition n).value ≤ (rate gap : ℝ) ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Integration.SourceParameters.rate

  33. def OAI.UniqueGamesTheorem.Integration.SourceParameters.sourceThreshold line 300
  34. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.sourceThreshold_pos line 302
  35. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.exists_repetition_length line 307
  36. def OAI.UniqueGamesTheorem.Integration.SourceParameters.repetitionLength line 314

    Source documentation

    Exact rational search, independent of the input formula.

    def repetitionLength (gap δ : ℚ) (hgap : 0 < gap) (hgap1 : gap ≤ 1)
    (hδ : 0 < δ) (D : Nat) (hD : 0 < D) : Nat :=
…
  37. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.repetitionLength_spec line 318
  38. theorem OAI.UniqueGamesTheorem.Integration.SourceParameters.repetitionLength_real_bound line 324