OAI/Computability/UniqueGames/Reduction/ActualCanonicalLemmas.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Reduction.ActualCanonical.Record line 19
  2. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.recordEquiv line 25
  3. instance OAI.UniqueGamesTheorem.Reduction.ActualCanonical.(instance at line 37) line 37
  4. abbrev OAI.UniqueGamesTheorem.Reduction.ActualCanonical.Data line 40
  5. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.pivot line 43
  6. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.translate line 46
  7. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.normalize line 47
  8. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.record line 49
  9. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.data line 57
  10. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.standardTriple line 61
  11. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.canonical line 64
  12. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.ambientEval line 68
  13. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.Represents line 72
  14. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.add_self line 76
  15. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.add_both line 82
  16. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.pivot_translate line 88
  17. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.normalize_translate line 94
  18. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.record_translate line 101
  19. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.data_gauge line 107
  20. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.data_global_shift line 117
  21. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.canonical_shift line 125
  22. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.ambientEval_hBasis line 139
  23. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.ambientEval_firstBasis line 144
  24. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.ambientEval_secondBasis line 156
  25. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.standard_represents line 169

    Source documentation

    Every actual linear map has the claimed ambient coefficient extension.

    theorem standard_represents (b : Fin k → F2) (X : E k →ₗ[F2] R) :
    Represents b (X (hBasis k)) (standardTriple X) X := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualCanonical.Represents, OAI.UniqueGamesTheorem.Reduction.ActualCanonical.standardTriple

  26. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.extension_coefficients line 176

    Source documentation

    Equality on the homogeneous space forces the free-coordinate identities.

    theorem extension_coefficients (b : Fin k → F2) (z : R) (a : Fin k → Fin 3 → R)
    (X : E k →ₗ[F2] R) (h : Represents b z a X) :
    X (hBasis k) = z + ∑ j, b j • a j 2 ∧
      ∀ j, X (firstBasis j) = a j 0 + a j 2 ∧
        X (secondBasis j) = a j 1 + a j 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualCanonical.Represents

  27. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.canonical_eq_of_extension line 188

    Source documentation

    Every ambient extension of a genuine map gives the same canonical data.

    theorem canonical_eq_of_extension (occ : Fin k → Id) (names : Id → Fin 3 → Name)
    (rhs : Id → F2) (z : R) (a : Fin k → Fin 3 → R) (X : E k →ₗ[F2] R)
    (h : Represents (fun j => rhs (occ j)) z a X) :
    canonical occ names rhs X = data occ names rhs z a := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualCanonical.Represents, OAI.UniqueGamesTheorem.Reduction.ActualCanonical.canonical, OAI.UniqueGamesTheorem.Reduction.ActualCanonical.data

  28. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.extension_independent line 203
  29. def OAI.UniqueGamesTheorem.Reduction.ActualCanonical.singletonTriple line 211
  30. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.pivot_singleton line 214
  31. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.record_singleton line 219
  32. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.singleton_global_adjustment line 226
  33. theorem OAI.UniqueGamesTheorem.Reduction.ActualCanonical.singleton_locality line 232

    Source documentation

    The hidden occurrence and its internal slot cannot affect a retained single-variable record. The occurrence need not differ from other positions.

    theorem singleton_locality (names : Id → Fin 3 → Name) (e e' : Id)
    (i i' : Fin 3) (c : R) (hname : names e i = names e' i') :
    record names e (singletonTriple i c) = record names e' (singletonTriple i' c) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualCanonical.record, OAI.UniqueGamesTheorem.Reduction.ActualCanonical.singletonTriple

  34. def OAI.UniqueGamesTheorem.Reduction.CloneGap.cart line 247
  35. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_const line 250
  36. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_cart line 254
  37. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.length_cart line 265
  38. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_cart_left line 270
  39. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_cart_right line 274
  40. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_cart_le line 278
  41. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_union_le line 291
  42. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_remove line 299
  43. abbrev OAI.UniqueGamesTheorem.Reduction.CloneGap.Index line 307
  44. def OAI.UniqueGamesTheorem.Reduction.CloneGap.indices line 308
  45. def OAI.UniqueGamesTheorem.Reduction.CloneGap.triples line 309
  46. def OAI.UniqueGamesTheorem.Reduction.CloneGap.collision line 310
  47. def OAI.UniqueGamesTheorem.Reduction.CloneGap.distinctTriples line 312
  48. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.length_indices line 314
  49. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.length_triples line 315
  50. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_index_eq_le line 318
  51. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_collision_le line 328
  52. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.majority_exists line 357
  53. def OAI.UniqueGamesTheorem.Reduction.CloneGap.allAgree line 371
  54. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.count_agree_distinct line 374
  55. structure OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation line 391
  56. def OAI.UniqueGamesTheorem.Reduction.CloneGap.satisfied line 397
  57. def OAI.UniqueGamesTheorem.Reduction.CloneGap.clone line 400
  58. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.lift_preserves line 403
  59. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.clone_names_distinct line 406
  60. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.agree_failure line 417
  61. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.failed_occurrence_clones line 427
  62. def OAI.UniqueGamesTheorem.Reduction.CloneGap.majorityBit line 443
  63. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.majorityBit_count line 445
  64. def OAI.UniqueGamesTheorem.Reduction.CloneGap.cloneList line 457
  65. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.length_cloneList line 460
  66. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.cloneList_failure_lower line 469
  67. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.clone_gap line 488
  68. theorem OAI.UniqueGamesTheorem.Reduction.CloneGap.clone_completeness_count line 507