OAI/Computability/UniqueGames/Gadgets/NonlinearRecurrenceLemmas.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Detection survives the logical-kernel quotient

A full family of logical characters on the quotient pulls back to a full lift on the original stage. Its detection event is the same pointwise. Combining this with the proved left-inverse construction gives detection of every linear map injective on the quotient's logical subspace.

  1. def OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.change line 23
  2. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.change_zero line 27
  3. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.compLeft_surjective line 31
  4. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.aggregate_single line 38
  5. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.child_outputs_perturb line 46
  6. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.parent_output_perturb line 57
  7. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.expect_change_at_index line 65

    Source documentation

    The exact conditional-uniform and coordinate-marginal law for a fixed selected index and fixed child perturbation.

    theorem expect_change_at_index (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
    (hlam : Function.Surjective lam) (C : P → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h)
    (F : X × B → B) (i : I) (a : P) :
    (𝔼 u : I → P,
      change F (aggregate J (fun j => C (u j))) (J i (C (u i + a) - C (u i)))) =
      𝔼 x : P, 𝔼 z : X × B, change F z (J i (C (x + a) - C x)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.change

  8. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.kernel_all line 109

    Source documentation

    The averaged block kernel includes zero differences by multiplication with their nonzero indicator.

    theorem kernel_all (J : I → B →ₗ[k] X × B) (F : X × B → B) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 → (𝔼 i, 𝔼 z : X × B, change F z (J i d)) = ρ)
    (d : B) :
    (𝔼 i, 𝔼 z : X × B, change F z (J i d)) = ρ * (if d ≠ 0 then 1 else 0) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.change

  9. theorem OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.parent_change_recurrence line 121

    Source documentation

    One exact nonlinear recurrence on the actual product input and the actual single-coordinate noise. The only remaining block obligation is hk.

    theorem parent_change_recurrence {N : Type*} [Fintype N]
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (hlam : Function.Surjective lam)
    (C : P → B) (hC : ∀ u h, C (u + e h) = C u + lam h)
    (F : X × B → B) (noise : N → P) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 → (𝔼 i, 𝔼 z : X × B, change F z (J i d)) = ρ) :
    (𝔼 i, 𝔼 n : N, 𝔼 u : I → P,
      if F (aggregate J (fun j => C ((u + (Pi.single i (noise n) : I → P)) j))) ≠
        F (aggregate J (fun j => C (u j))) then (1 : ℚ) else 0) =
      ρ * (𝔼 n : N, 𝔼 x : P, if C (x + noise n) ≠ C x then (1 : ℚ) else 0) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.change

  10. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.shifts line 169
  11. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.shiftEquiv line 171
  12. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.shiftEquiv_coe line 174
  13. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.embed_shiftEquiv_symm line 177
  14. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.logical line 181
  15. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.logical_shiftEquiv line 184
  16. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.logical_surjective line 188
  17. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.equivariant line 193
  18. abbrev OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space line 200
  19. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.projection line 202
  20. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.projection_surjective line 205
  21. instance OAI.UniqueGamesTheorem.Gadget.StageQuotient.spaceFinite line 208
  22. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.shift line 211
  23. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.shift_injective line 214
  24. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.shift_logical line 217
  25. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.output line 223
  26. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.output_projection line 226
  27. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.output_equivariant line 229
  28. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.noise line 235

    Source documentation

    Original finite noise choices, pushed through the actual quotient map.

    noncomputable def noise (s : Stage k B) : s.Noise → Space s :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space

  29. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.noise_change_iff line 238
  30. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.character_logical line 243
  31. theorem OAI.UniqueGamesTheorem.Gadget.StageQuotient.noise_detection_iff line 247
  32. def OAI.UniqueGamesTheorem.Gadget.StageQuotient.toStage line 253

    Source documentation

    The quotient is again a finite stage; its logical map is now the identity.

    noncomputable def toStage [Finite B] (s : Stage k B) : Stage k B where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  33. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_equiv line 278
  34. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_eq_sum_indicator line 285
  35. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_prod_average line 296

    Source documentation

    Uniform probability on a product is the average of the second-coordinate probabilities. No nonemptiness hypotheses are needed for this identity.

    theorem probability_prod_average {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]
    (p : Ω → Ξ → Prop) :
    probability (fun z : Ω × Ξ => p z.1 z.2) =
      (∑ x : Ω, probability (p x)) / (Fintype.card Ω : ℚ) := by
…
  36. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_prod_average_right line 308

    Source documentation

    The same product identity, averaging in the other order.

    theorem probability_prod_average_right {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]
    (p : Ω → Ξ → Prop) :
    probability (fun z : Ω × Ξ => p z.1 z.2) =
      (∑ y : Ξ, probability (fun x : Ω => p x y)) /
        (Fintype.card Ξ : ℚ) := by
…
  37. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_coordinate line 320

    Source documentation

    Every coordinate of a uniformly chosen function has the uniform marginal. Pointwise transpositions biject the evaluation fibers.

    theorem probability_coordinate {I X : Type*} [Fintype I] [Fintype X]
    (i : I) (p : X → Prop) :
    probability (fun g : I → X => p (g i)) = probability p := by
…
  38. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_coordinate_prod line 350

    Source documentation

    Coordinate projection preserves the joint uniform law with an independent finite noise sample.

    theorem probability_coordinate_prod {I X N : Type*}
    [Fintype I] [Fintype X] [Fintype N] (i : I) (p : X → N → Prop) :
    probability (fun z : (I → X) × N => p (z.1 i) z.2) =
      probability (fun z : X × N => p z.1 z.2) := by
…
  39. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_prod_reorder line 362

    Source documentation

    Grouping the same three uniform choices in another order.

    theorem probability_prod_reorder {Ω I N : Type*}
    [Fintype Ω] [Fintype I] [Fintype N] (p : Ω → I → N → Prop) :
    probability (fun z : Ω × (I × N) => p z.1 z.2.1 z.2.2) =
      probability (fun z : I × (Ω × N) => p z.2.1 z.1 z.2.2) := by
…
  40. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_prod_eq_of_const line 375

    Source documentation

    If each conditional probability is the same, their uniform average is that common value.

    theorem probability_prod_eq_of_const {Ω Ξ : Type*}
    [Fintype Ω] [Fintype Ξ] [Nonempty Ω]
    (p : Ω → Ξ → Prop) (q : ℚ) (h : ∀ x, probability (p x) = q) :
    probability (fun z : Ω × Ξ => p z.1 z.2) = q := by
…
  41. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.enlarged_single_copy_probability line 388

    Source documentation

    For a fixed selected injection, the enlargement's change event has exactly the base input/noise probability.

    theorem enlarged_single_copy_probability {F B K V N : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [AddCommGroup V] [Fintype V] [Fintype N]
    [Fintype (LinearInjection F B K)]
    (C : V → B) (a : N → V) (L : LinearInjection F B K) :
    probability (fun z : (LinearInjection F B K → V) × N =>
      enlargedOutput C (Function.update z.1 L (z.1 L + a z.2)) ≠
        enlargedOutput C z.1) =
      probability (fun z : V × N => C (z.1 + a z.2) ≠ C z.1) := by
…
  42. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.enlarged_random_copy_probability line 407

    Source documentation

    The same equality after selecting the injection uniformly as part of the noise sample. Its sample space is exactly product-input × (copy × base-noise).

    theorem enlarged_random_copy_probability {F B K V N : Type*} [Field F]
    [AddCommGroup B] [Module F B] [AddCommGroup K] [Module F K]
    [AddCommGroup V] [Fintype V] [Fintype N]
    [Fintype (LinearInjection F B K)] [Nonempty (LinearInjection F B K)]
    (C : V → B) (a : N → V) :
    probability (fun z : (LinearInjection F B K → V) ×
        (LinearInjection F B K × N) =>
      enlargedOutput C
        (Function.update z.1 z.2.1 (z.1 z.2.1 + a z.2.2)) ≠
          enlargedOutput C z.1) =
      probability (fun z : V × N => C (z.1 + a z.2) ≠ C z.1) := by
…
  43. abbrev OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.Copies line 435
  44. def OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.copiesFintype line 441

    Source documentation

    A concrete finite enumeration exists because an injection is determined by its finite function table.

    noncomputable def copiesFintype : Fintype (Copies B K) :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.Copies

  45. def OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productEmbed line 449
  46. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productEmbed_injective line 457
  47. def OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productStage line 466

    Source documentation

    The product before the quotient. Its finite noise sampler first chooses an injection uniformly, then independently chooses the original base noise.

    def productStage (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) : Stage (ZMod 2) K := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  48. def OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.build line 484

    Source documentation

    The final finite gadget, with K embedded as its actual shift space.

    def build (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) : Stage (ZMod 2) K :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  49. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.add_single_eq_update line 492
  50. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.change_iff line 502

    Source documentation

    The quotient and injection preserve each individual nonlinear change event exactly, before taking any finite averages.

    theorem change_iff (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) (x : Copies B K → V) (L : Copies B K) (n : N) :
    let s := productStage i hi C hC noise hdim b₀ hb₀
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.Copies, OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productStage

  51. def OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.copyObserver line 517

    Source documentation

    Restriction of a linear observer on the quotient to one base-input copy.

    def copyObserver {E : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    (T : StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀) →ₗ[ZMod 2] E)
    (L : Copies B K) : V →ₗ[ZMod 2] E :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space, OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productStage, OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.Copies

  52. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.copyObserver_shift line 527
  53. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.dual_pullback_eq_top_iff line 555
  54. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.detection_average line 563

    Source documentation

    Average detection over the actual injection-indexed base copies. The restriction threshold is the rank on the final embedded logical space.

    theorem detection_average {E : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    (hbase : ∀ U : V →ₗ[ZMod 2] E, Function.Injective (U.comp i) →
      1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0))
    (T : StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀) →ₗ[ZMod 2] E)
    (hr : Module.finrank (ZMod 2) B + 2 ≤ Module.finrank (ZMod 2)
      (LinearMap.range (T.comp (StageQuotient.shift
        (productStage i hi C hC noise hdim b₀ hb₀))))) :
    1 / 8 ≤
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space, OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productStage, OAI.UniqueGamesTheorem.Gadget.StageQuotient.shift

  55. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_projection line 592

    Source documentation

    Passing uniform input through the actual quotient preserves its law.

    theorem probability_projection (s : Stage (ZMod 2) K)
    [Fintype s.Input] [Fintype (StageQuotient.Space s)]
    (p : StageQuotient.Space s → Prop) :
    probability (fun x : s.Input => p (StageQuotient.projection s x)) = probability p := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space, OAI.UniqueGamesTheorem.Gadget.StageQuotient.projection

  56. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.probability_projection_prod line 603
  57. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.change_probability line 617

    Source documentation

    Nonlinear change probability is exactly the base probability after both the single-copy enlargement and quotient, on uniform quotient input.

    theorem change_probability (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    [Fintype (StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀))] :
    let s := productStage i hi C hC noise hdim b₀ hb₀
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space, OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productStage

  58. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.detection_probability line 648

    Source documentation

    The final noise sample is the actual product sampler and meets the stated rank-detection bound. No detection premise about the enlarged gadget is assumed.

    theorem detection_probability {E : Type*} [AddCommGroup E] [Module (ZMod 2) E]
    (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0)
    (hbase : ∀ U : V →ₗ[ZMod 2] E, Function.Injective (U.comp i) →
      1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0))
    (T : StageQuotient.Space (productStage i hi C hC noise hdim b₀ hb₀) →ₗ[ZMod 2] E)
    (hr : Module.finrank (ZMod 2) B + 2 ≤ Module.finrank (ZMod 2)
      (LinearMap.range (T.comp (StageQuotient.shift
        (productStage i hi C hC noise hdim b₀ hb₀))))) :
    1 / 8 ≤ probability (fun t : Copies B K × N =>
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space, OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.productStage, OAI.UniqueGamesTheorem.Gadget.StageQuotient.shift, OAI.UniqueGamesTheorem.Gadget.EnlargementConstruction.Copies

  59. def OAI.UniqueGamesTheorem.Gadget.QuotientDetection.pullbackFullLift line 694
  60. theorem OAI.UniqueGamesTheorem.Gadget.QuotientDetection.pullback_detection_iff line 709
  61. theorem OAI.UniqueGamesTheorem.Gadget.QuotientDetection.full_detection_after_quotient line 723

    Source documentation

    Any checked full-lift probability bound before quotienting applies to every full family on the actual quotient, on the same noise sampler.

    theorem full_detection_after_quotient (s : Stage k B) [Fintype s.Noise] (q : ℚ)
    (hfull : ∀ L : Lift s (⊤ : Submodule k (Module.Dual k B)),
      q ≤ probability (fun n => ∃ z, L.family z (s.noise n) ≠ 0))
    (ψ : Module.Dual k B →ₗ[k] Module.Dual k (StageQuotient.Space s))
    (hψ : IsFullLift (StageQuotient.shift s) ψ) :
    q ≤ characterDetection (StageQuotient.noise s) ψ := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space, OAI.UniqueGamesTheorem.Gadget.StageQuotient.shift, OAI.UniqueGamesTheorem.Gadget.StageQuotient.noise

  62. theorem OAI.UniqueGamesTheorem.Gadget.QuotientDetection.target_detection_after_quotient line 736

    Source documentation

    The form consumed by the injection enlargement: injectivity on the base logical alphabet suffices for the same detection probability.

    theorem target_detection_after_quotient (s : Stage k B) [Fintype s.Noise]
    {E : Type*} [AddCommGroup E] [Module k E] [DecidableEq E]
    (T : StageQuotient.Space s →ₗ[k] E) (q : ℚ)
    (hfull : ∀ L : Lift s (⊤ : Submodule k (Module.Dual k B)),
      q ≤ probability (fun n => ∃ z, L.family z (s.noise n) ≠ 0))
    (hinj : Function.Injective (T.comp (StageQuotient.shift s))) :
    q ≤ probability (fun n => T (StageQuotient.noise s n) ≠ 0) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.StageQuotient.Space, OAI.UniqueGamesTheorem.Gadget.Lift, OAI.UniqueGamesTheorem.Gadget.StageQuotient.shift, OAI.UniqueGamesTheorem.Gadget.StageQuotient.noise

  63. def OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.average line 765
  64. theorem OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.average_eq_expect line 769
  65. def OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error line 780

    Source documentation

    Uniform finite input and the stage's actual uniform finite noise choices.

    noncomputable def error (s : Stage k B) : ℚ := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  66. theorem OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error_eq_expect line 785
  67. theorem OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.base_error line 798
  68. theorem OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.next_error line 827

    Source documentation

    The exact one-level law for the actual stage constructor.

    theorem next_error (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 →
      (𝔼 i, 𝔼 z : X × B,
        NonlinearRecurrence.change (fun p => p.2 + Q p.1) z (J i d)) = ρ)
    (s : Stage k B) : error (Stage.next J hJ Q s) = ρ * error s := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.change, OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error, OAI.UniqueGamesTheorem.Gadget.Stage.next

  69. theorem OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.iterate_error line 849

    Source documentation

    Solving the proved recurrence, with the actual height-zero probability.

    theorem iterate_error (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 →
      (𝔼 i, 𝔼 z : X × B,
        NonlinearRecurrence.change (fun p => p.2 + Q p.1) z (J i d)) = ρ)
    (n : ℕ) : error (Stage.iterate J hJ Q n) =
      (1 - 1 / (Fintype.card B : ℚ)) * ρ ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.aggregate, OAI.UniqueGamesTheorem.Gadget.NonlinearRecurrence.change, OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error, OAI.UniqueGamesTheorem.Gadget.Stage.iterate

  70. theorem OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.quotient_error line 864

    Source documentation

    The quotient uses the original noise choices and preserves their full uniform-input change probability.

    theorem quotient_error (s : Stage k B) : error (StageQuotient.toStage s) = error s := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.StageNoiseRecurrence.error, OAI.UniqueGamesTheorem.Gadget.StageQuotient.toStage