OAI/Computability/UniqueGames/PCP/AlphabetRetractionLemmas.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Pull a graph predicate back through a surjective label decoder. This preserves every rejection count after decoding. A concrete section embeds the initial eight-label graph into the fixed 64-label alphabet used throughout amplification.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.pullback line 23
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.edgeSatisfied_pullback line 30
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.rejectionCount_pullback line 35
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.satisfiable_pullback_iff line 40
  5. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.Label64 line 52
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.decode64 line 54
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.encode64 line 56
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.decode_encode64 line 59
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.initial64 line 64
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.initial64_satisfiable_iff line 68
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.initial64_alphabet line 73
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetRetraction.initial64_inverse_size_gap line 76
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean line 95
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.energy line 97
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.correlation line 99
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.averagingOperator line 102
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.iterateOperator line 105
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeProfile line 110
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity line 113
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.markedStep line 116
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass line 120
  22. structure OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate line 124
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_eq_sum_div_card line 135
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_equiv line 139
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_prod line 143
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_const line 148
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_add line 151
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_sub line 155
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_mul_left line 159
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_mul_right line 163
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_nonnegative line 167
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_mono line 170
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.energy_nonnegative line 173
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.correlation_sq_le line 177

    Source documentation

    The finite Cauchy--Schwarz inequality, in the chosen normalized convention.

    theorem correlation_sq_le (f g : A → ℝ) :
    correlation f g ^ 2 ≤ energy f * energy g :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.correlation, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.energy

  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.energy_sub_const line 181
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.correlation_sub_const line 190
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_operator line 208
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.operator_sub_const line 218
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_iterate line 226
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.iterate_sub_const line 232
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean_markedStep line 241

    Source documentation

    Reversal moves the first marked edge to its endpoint. The profile therefore appears at the endpoint, before the gap remaining vertex transitions.

    theorem mean_markedStep (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (f : V → ℝ) :
    mean (markedStep G bad f) = correlation (edgeProfile bad) f := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.markedStep, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.correlation, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeProfile

  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass_eq_correlation line 269
  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.iterate_energy_bound line 276
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.zero_mean_correlation_bound line 291
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.correlation_centered line 306
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity_eq_edge_mean line 321

    Source documentation

    Density is exactly the uniform probability of a marked directed port-edge.

    theorem edgeDensity_eq_edge_mean (bad : V × D → Bool) :
    edgeDensity bad = mean (fun e => if bad e then (1 : ℝ) else 0) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.mean

  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity_eq_card line 328

    Source documentation

    The edge convention counts each directed port once, including parallel edges and loops. Thus the density is literally the marked-edge cardinal ratio.

    theorem edgeDensity_eq_card (bad : V × D → Bool) :
    edgeDensity bad =
      ((Finset.univ.filter (fun e => bad e = true)).card : ℝ) /
        (Fintype.card (V × D) : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity

  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeProfile_nonnegative line 336
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeProfile_le_one line 340
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity_nonnegative line 348
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity_le_one line 351
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeProfile_energy_le_density line 357
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeProfile_centered_energy line 364
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass_le_sharp line 375

    Source documentation

    Sharp return bound. No division by the bad-edge density occurs, so the empty bad set is covered. gap = 0 gives the adjacent-edge upper bound epsilon.

    theorem returnMass_le_sharp (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (gap : Nat) :
    returnMass G bad gap ≤ edgeDensity bad ^ 2 +
      lambda ^ gap * (edgeDensity bad * (1 - edgeDensity bad)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity

  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass_le line 392

    Source documentation

    The simple bound used in the second-moment estimate.

    theorem returnMass_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (gap : Nat) :
    returnMass G bad gap ≤ edgeDensity bad ^ 2 + edgeDensity bad * lambda ^ gap := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity

  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.adjacent_returnMass_le line 402
  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.geometric_sum_le line 414

    Source documentation

    The finite geometric-series bound that absorbs forward and reverse returns. It applies to every finite window, with no limiting probability argument.

    theorem geometric_sum_le (lambda : ℝ) (h0 : 0 ≤ lambda) (h1 : lambda < 1) (n : Nat) :
    (∑ k ∈ Finset.range n, lambda ^ k) ≤ 1 / (1 - lambda) := by
…
  58. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.sum_returnMass_le line 430

    Source documentation

    The return contribution from one marked edge, over a finite forward window.

    theorem sum_returnMass_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (n : Nat) :
    (∑ gap ∈ Finset.range n, returnMass G bad gap) ≤
      (n : ℝ) * edgeDensity bad ^ 2 + edgeDensity bad / (1 - lambda) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity

  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.triangular_returnMass_sum_le line 452

    Source documentation

    Sum over all distinct ordered-time pairs, counting each pair once. The row for the later edge j has gaps 0,...,j-1.

    theorem triangular_returnMass_sum_le (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (n : Nat) :
    (∑ j ∈ Finset.range n, ∑ gap ∈ Finset.range j, returnMass G bad gap) ≤
      ((n : ℝ) * ((n : ℝ) - 1) / 2) * edgeDensity bad ^ 2 +
        (n : ℝ) * (edgeDensity bad / (1 - lambda)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity

  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.secondMoment_return_envelope line 474

    Source documentation

    The exact finite envelope needed after expanding the square of the hit count. The diagonal contributes n * epsilon; both off-diagonal triangles contribute twice the return sum. The actual walk-event identity is supplied by PoweringMoment and PoweringReturn.

    theorem secondMoment_return_envelope (G : PortGraph V D) (lambda : ℝ)
    (certificate : SpectralCertificate G lambda) (bad : V × D → Bool)
    (reversal : ∀ e, bad (G.rot e) = bad e) (n : Nat) :
    (n : ℝ) * edgeDensity bad +
        2 * (∑ j ∈ Finset.range n, ∑ gap ∈ Finset.range j, returnMass G bad gap) ≤
      (n : ℝ) * edgeDensity bad *
        (1 + 2 / (1 - lambda) + ((n : ℝ) - 1) * edgeDensity bad) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.edgeDensity, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.returnMass

  61. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.zeroFrequency line 520
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cubeXor_cancel_right line 522
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cubeXor_assoc line 527
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cubeXor_zeroFrequency line 533
  65. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.xorTranslation line 539

    Source documentation

    Uniform cube measure is invariant under this explicit xor translation.

    def xorTranslation (y : Cube I) : Cube I ≃ Cube I where
…
  66. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.rotate line 545
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.rotate_involutive line 548
  68. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyGraph line 554

    Source documentation

    The undirected regular port graph generated by the indexed cube vectors.

    def cayleyGraph (g : D → Cube I) : PortGraph (Cube I) D where
…
  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyGraph_rot line 562
  70. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.splitPortWord line 566

    Source documentation

    Expose the first actual port in a finite port word.

    def splitPortWord (n : Nat) : (Fin (n + 1) → D) ≃ D × (Fin n → D) where
…
  71. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.powerGenerators line 575

    Source documentation

    The generator of a powered port is the xor of its original port word.

    def powerGenerators (g : D → Cube I) : (n : Nat) → (Fin n → D) → Cube I
  | 0, _ => zeroFrequency
  | n + 1, p => cubeXor (g (p 0)) (powerGenerators g n (fun j => p j.succ))

/-- These are actual walk displacements, including repeated vertices and ports. -/

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.zeroFrequency

  72. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.wordEnd_eq_powerGenerators line 580

    Source documentation

    These are actual walk displacements, including repeated vertices and ports.

    theorem wordEnd_eq_powerGenerators (g : D → Cube I) (n : Nat)
    (x : Cube I) (p : Fin n → D) :
    wordEnd (cayleyGraph g) n x p = cubeXor x (powerGenerators g n p) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.powerGenerators

  73. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyAverage line 595

    Source documentation

    Average along the actual outgoing ports of the Cayley graph.

    def cayleyAverage (g : D → Cube I) (f : Cube I → ℝ) (x : Cube I) : ℝ :=
…
  74. def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue line 599

    Source documentation

    The eigenvalue is the empirical bias of the generator characters.

    def eigenvalue (g : D → Cube I) (s : Cube I) : ℝ :=
…
  75. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.averagingOperator_cayleyGraph line 603
  76. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.coefficient_zeroFrequency line 606
  77. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.coefficient_xorTranslation line 611

    Source documentation

    Change variables through xor translation in the actual Fourier average.

    theorem coefficient_xorTranslation (f : Cube I → ℝ) (s v : Cube I) :
    coefficient (fun x => f (cubeXor x v)) s = walsh s v * coefficient f s := by
…
  78. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyAverage_walsh line 633

    Source documentation

    Each Walsh character is an eigenvector of the actual Cayley averaging.

    theorem cayleyAverage_walsh (g : D → Cube I) (s x : Cube I) :
    cayleyAverage g (walsh s) x = eigenvalue g s * walsh s x := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyAverage, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue

  79. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.coefficient_cayleyAverage line 642

    Source documentation

    Full Walsh diagonalization, obtained by swapping the two finite averages.

    theorem coefficient_cayleyAverage (g : D → Cube I) (f : Cube I → ℝ) (s : Cube I) :
    coefficient (cayleyAverage g f) s = eigenvalue g s * coefficient f s := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyAverage, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue

  80. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue_powerGenerators line 660

    Source documentation

    Uniform finite port-word splitting multiplies the actual eigenvalues.

    theorem eigenvalue_powerGenerators (g : D → Cube I) (n : Nat) (s : Cube I) :
    eigenvalue (powerGenerators g n) s = eigenvalue g s ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.powerGenerators

  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.power_port_card line 686

    Source documentation

    The port degree of the powered graph is the exact number of port words.

    theorem power_port_card (n : Nat) :
    Fintype.card (Fin n → D) = Fintype.card D ^ n := by
…
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.seven_power_port_card line 690
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayley_energy_contraction line 698

    Source documentation

    A bias bound on all nonconstant generator characters contracts the actual mean-zero function energy. The constant coefficient is eliminated by its exact identification with the mean, and every other coefficient is bounded termwise.

    theorem cayley_energy_contraction (g : D → Cube I) (lambda : ℝ) (_hlambda : 0 ≤ lambda)
    (hbias : ∀ s : Cube I, s ≠ zeroFrequency → |eigenvalue g s| ≤ lambda)
    (f : Cube I → ℝ) (hmean : (𝔼 x, f x) = 0) :
    (𝔼 x, cayleyAverage g f x ^ 2) ≤ lambda ^ 2 * (𝔼 x, f x ^ 2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.zeroFrequency, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyAverage

  84. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayley_spectralCertificate line 732

    Source documentation

    The Fourier proof supplies the graph certificate used in return bounds.

    theorem cayley_spectralCertificate (g : D → Cube I) (lambda : ℝ)
    (hlambda : 0 ≤ lambda) (hlambdaone : lambda < 1)
    (hbias : ∀ s : Cube I, s ≠ zeroFrequency → |eigenvalue g s| ≤ lambda) :
    SpectralReturn.SpectralCertificate (cayleyGraph g) lambda where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.zeroFrequency, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyGraph

  85. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.power_eigenvalue_bound line 743
  86. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.sevenStep_halfCertificate line 755

    Source documentation

    Seven actual generator steps turn one-half character bias into 2⁻⁷.

    theorem sevenStep_halfCertificate (g : D → Cube I)
    (hbias : ∀ s : Cube I, s ≠ zeroFrequency → |eigenvalue g s| ≤ (1 / 2 : ℝ)) :
    SpectralReturn.SpectralCertificate (cayleyGraph (powerGenerators g 7))
      ((1 / 2 : ℝ) ^ 7) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.zeroFrequency, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.eigenvalue, OAI.UniqueGamesTheorem.Foundations.PCP.SpectralReturn.SpectralCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.cayleyGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CayleySpectral.powerGenerators