OAI/Computability/UniqueGames/Gadgets/ActualGadgetLemmas.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Actual finite binary-vector-space gadgets and their uniform experiments. The existence statement is the target of the recursive construction, not an assumed theorem. Noise is indexed by a nonempty finite type; repeated vector values therefore keep their intended multiplicities.

  1. abbrev OAI.UniqueGamesTheorem.Gadget.ActualGadget.F2 line 19
  2. structure OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data line 21
  3. def OAI.UniqueGamesTheorem.Gadget.ActualGadget.failureIndicator line 41

    Source documentation

    The actual output-change indicator before taking a finite average.

    noncomputable def failureIndicator (g : Data C) (sample : g.Ambient × g.NoiseIndex) : ℚ := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data

  4. def OAI.UniqueGamesTheorem.Gadget.ActualGadget.stabilityError line 46

    Source documentation

    Uniform ambient input, independently uniform noise-list index.

    noncomputable def stabilityError (g : Data C) : ℚ :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data

  5. def OAI.UniqueGamesTheorem.Gadget.ActualGadget.kernelIndicator line 50

    Source documentation

    The actual zero-image event for a linear map.

    noncomputable def kernelIndicator (g : Data C) {P : Type}
    [AddCommGroup P] [Module F2 P] (S : g.Ambient →ₗ[F2] P) (i : g.NoiseIndex) : ℚ := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data, OAI.UniqueGamesTheorem.Gadget.ActualGadget.F2

  6. def OAI.UniqueGamesTheorem.Gadget.ActualGadget.kernelError line 55
  7. theorem OAI.UniqueGamesTheorem.Gadget.ActualGadget.stabilityError_nonneg line 59
  8. theorem OAI.UniqueGamesTheorem.Gadget.ActualGadget.stabilityError_le_one line 66
  9. theorem OAI.UniqueGamesTheorem.Gadget.ActualGadget.kernelError_nonneg line 73
  10. theorem OAI.UniqueGamesTheorem.Gadget.ActualGadget.kernelError_le_one line 81
  11. def OAI.UniqueGamesTheorem.Gadget.ActualGadget.leaf line 90

    Source documentation

    The actual identity leaf, with every symbol vector used once as noise.

    def leaf (C : Type) [AddCommGroup C] [Module F2 C] [Fintype C] : Data C where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.F2, OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data

  12. def OAI.UniqueGamesTheorem.Gadget.ActualGadget.Satisfies line 100

    Source documentation

    The stability and dispersion claim of Theorem 3.4 for fixed errors and rank.

    def Satisfies (g : Data C) (ζ ν : ℚ) (r : Nat) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data

  13. def OAI.UniqueGamesTheorem.Gadget.ActualGadget.StableNonlinearDispersion line 106

    Source documentation

    The mathematical existence target.

    def StableNonlinearDispersion : Prop :=
…
  14. def OAI.UniqueGamesTheorem.Gadget.StageData.toData line 129

    Source documentation

    The normalized stage's actual data, with its original finite noise choices. Passing the inclusion explicitly avoids dependent casts of the shift carrier.

    def toData (s : Stage (ZMod 2) C) (embed : C →ₗ[ZMod 2] s.Input)
    (hinj : Function.Injective embed)
    (hEquiv : ∀ u c, s.output (u + embed c) = s.output u + c) : ActualGadget.Data C where
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data

  15. theorem OAI.UniqueGamesTheorem.Gadget.StageData.count_probability_eq_expect line 143

    Source documentation

    Intrinsic count probability and uniform finite expectation are identical.

    theorem count_probability_eq_expect {Ω : Type*} [Fintype Ω] (p : Ω → Prop) :
    Enlargement.probability p = 𝔼 x : Ω, if p x then (1 : ℚ) else 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

  16. theorem OAI.UniqueGamesTheorem.Gadget.StageData.count_probability_eq_harmonic line 150
  17. theorem OAI.UniqueGamesTheorem.Gadget.StageData.stabilityError_toData line 158
  18. theorem OAI.UniqueGamesTheorem.Gadget.StageData.stabilityError_toData_count line 172
  19. theorem OAI.UniqueGamesTheorem.Gadget.StageData.error_eq_count_probability line 189
  20. theorem OAI.UniqueGamesTheorem.Gadget.StageData.kernelError_toData_count line 202
  21. theorem OAI.UniqueGamesTheorem.Gadget.StageData.kernelError_eq_one_sub_detection line 216

    Source documentation

    The common interface's zero-image error is exactly the complement of the nonzero-image detection probability.

    theorem kernelError_eq_one_sub_detection (s : Stage (ZMod 2) C) [Fintype s.Noise]
    (embed : C →ₗ[ZMod 2] s.Input) (hinj : Function.Injective embed)
    (hEquiv : ∀ u c, s.output (u + embed c) = s.output u + c)
    {E : Type} [AddCommGroup E] [Module (ZMod 2) E] (T : s.Input →ₗ[ZMod 2] E) :
    ActualGadget.kernelError (toData s embed hinj hEquiv) T =
      1 - Enlargement.probability (fun n : s.Noise => T (s.noise n) ≠ 0) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage, OAI.UniqueGamesTheorem.Gadget.ActualGadget.kernelError, OAI.UniqueGamesTheorem.Gadget.StageData.toData, OAI.UniqueGamesTheorem.Gadget.Enlargement.probability

  22. theorem OAI.UniqueGamesTheorem.Gadget.StageData.kernelError_le_of_detection line 237
  23. def OAI.UniqueGamesTheorem.Gadget.EnlargementEndpoint.data line 278
  24. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementEndpoint.data_satisfies line 288

    Source documentation

    Base stability and base detection suffice for the complete enlarged gadget. Its detection error is the fixed constant 7/8.

    theorem data_satisfies (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) (p : ℚ)
    (hchange : probability (fun z : V × N => C (z.1 + noise z.2) ≠ C z.1) ≤ p)
    (hbase : ∀ (E : Type) [AddCommGroup E] [Module (ZMod 2) E]
      (U : V →ₗ[ZMod 2] E), Function.Injective (U.comp i) →
        1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0)) :
    ActualGadget.Satisfies (data i hi C hC noise hdim b₀ hb₀) p (7 / 8)
      (Module.finrank (ZMod 2) B + 2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.Satisfies, OAI.UniqueGamesTheorem.Gadget.EnlargementEndpoint.data

  25. theorem OAI.UniqueGamesTheorem.Gadget.EnlargementEndpoint.exists_data line 319

    Source documentation

    For every permitted logical space there is an actual gadget. The rank threshold dim B + 2 and all base data are independent of that space.

    theorem exists_data (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) (p : ℚ)
    (hchange : probability (fun z : V × N => C (z.1 + noise z.2) ≠ C z.1) ≤ p)
    (hbase : ∀ (E : Type) [AddCommGroup E] [Module (ZMod 2) E]
      (U : V →ₗ[ZMod 2] E), Function.Injective (U.comp i) →
        1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0)) :
    ∃ g : ActualGadget.Data K,
      ActualGadget.Satisfies g p (7 / 8) (Module.finrank (ZMod 2) B + 2) :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data, OAI.UniqueGamesTheorem.Gadget.ActualGadget.Satisfies