OAI/Computability/UniqueGames/PCP/FinalConstantsLemmas.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

The actual fixed-parameter graph transformation in one PCP amplification round. It preprocesses the input graph, checks all edges of each bounded walk using local endpoint labels, and applies the checked constant-query alphabet reduction. The bounded address list is explicit fixed data shared by every input graph.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.alphabet line 15
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.compositionLoss line 16
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.denominator line 17
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowHalf line 18
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowSize line 19
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.smoothingScale line 20
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.endpointLength line 21
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.walkLength line 22
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.gain line 24
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.cap line 25
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.denominator_positive line 27
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowHalf_positive line 30
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.walkLength_positive line 33
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.gain_large line 36
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.cap_positive line 43
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.cap_le_one line 46
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.composed_gap line 52

    Source documentation

    The exact fixed constants make a whole round double the input gap until the fixed positive threshold cap is reached.

    theorem composed_gap (epsilon : ℝ) (he : 0 ≤ epsilon) :
    min (2 * epsilon) cap ≤
      gain * min (epsilon / (Preprocessing.sizeFactor : ℝ))
        (1 / (walkLength : ℝ)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.cap, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.gain, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.sizeFactor, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.walkLength

  18. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Label line 89
  19. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Addresses line 90
  20. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.PoweredAlphabet line 91
  21. instance OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.(instance at line 94) line 94
  22. instance OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.(instance at line 95) line 95
  23. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.PoweredDart line 100
  24. instance OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.(instance at line 104) line 104
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.selectors line 106
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.powered line 113
  27. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Vertex line 119
  28. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Dart line 124
  29. instance OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.(instance at line 127) line 127
  30. instance OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.(instance at line 136) line 136
  31. instance OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.(instance at line 139) line 139
  32. def OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.graph line 141
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.powered_completeness line 146
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.completeness line 159
  35. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.Alphabet line 184
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.card_alphabet line 186
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.card_alphabet_eq_final line 189
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.center_eq line 193

    Source documentation

    The actual six-bit alphabet gives the endpoint length fixed for the round.

    theorem center_eq :
    PoweringSoundness.center (Fintype.card Alphabet) FinalConstants.windowHalf =
      FinalConstants.endpointLength := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.center, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowHalf, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.endpointLength

  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.walkLength_eq line 200

    Source documentation

    Prefix, pivot and suffix together have the fixed odd walk length.

    theorem walkLength_eq :
    2 * PoweringSoundness.center (Fintype.card Alphabet) FinalConstants.windowHalf + 1 =
      FinalConstants.walkLength := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.center, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowHalf, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.walkLength

  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.spectral_denominator_eq line 207

    Source documentation

    The spectral denominator is exactly 66 at the fixed return parameter.

    theorem spectral_denominator_eq :
    (1 + 2 / (1 - (31 / 32 : ℝ))) + 1 = 66 := by
…
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.gain_eq line 213

    Source documentation

    Dividing the actual powering coefficient by the composition loss gives the round coefficient exactly. The large window parameter is not evaluated.

    theorem gain_eq :
    PoweringSoundness.gain 64 FinalConstants.windowHalf (31 / 32) / 12288 =
      FinalConstants.gain := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.gain, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowHalf, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.gain

  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.gain_card_eq line 231
  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.scaled_bound_eq line 239

    Source documentation

    Both the coefficient and cap in the actual estimate match the fixed round constants, for every real error parameter.

    theorem scaled_bound_eq (ε : ℝ) :
    (PoweringSoundness.gain (Fintype.card Alphabet) FinalConstants.windowHalf (31 / 32) *
        min ε
          (1 / ((2 * PoweringSoundness.center (Fintype.card Alphabet)
            FinalConstants.windowHalf + 1 : Nat) : ℝ))) / 12288 =
      FinalConstants.gain * min ε FinalConstants.cap := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.gain, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowHalf, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.center, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.gain, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.cap

  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.composed_scaled_gap line 251

    Source documentation

    The composed powering and alphabet-reduction coefficient yields the fixed doubling bound after the checked preprocessing loss.

    theorem composed_scaled_gap (ε : ℝ) (hε : 0 ≤ ε) :
    min (2 * ε) FinalConstants.cap ≤
      (PoweringSoundness.gain (Fintype.card Alphabet) FinalConstants.windowHalf (31 / 32) *
        min (ε / (Preprocessing.sizeFactor : ℝ))
          (1 / ((2 * PoweringSoundness.center (Fintype.card Alphabet)
            FinalConstants.windowHalf + 1 : Nat) : ℝ))) / 12288 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.cap, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.gain, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFinalConstants.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.FinalConstants.windowHalf, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.sizeFactor, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringSoundness.center