OAI/Computability/MaxCut/Games/Incidence.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

Actual finite incidence-game probabilities for Proposition 4.3. The referee samples an occurrence and one of three slots independently and uniformly. Alice sees its occurrence; Bob sees only its variable name.

  1. structure OAI.MaxCutGames.Reduction.Incidence.Triple line 12
  2. def OAI.MaxCutGames.Reduction.Incidence.parity line 18
  3. def OAI.MaxCutGames.Reduction.Incidence.matchingSlots line 20
  4. def OAI.MaxCutGames.Reduction.Incidence.acceptedSlots line 26

    Source documentation

    Invalid Alice answers lose in every slot.

    def acceptedSlots (a b : Triple) (rhs : Bool) : Nat :=
…

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Triple

  5. def OAI.MaxCutGames.Reduction.Incidence.failedEquation line 29
  6. def OAI.MaxCutGames.Reduction.Incidence.bestResponse line 33

    Source documentation

    Copy a satisfying Bob triple; otherwise flip its first bit.

    def bestResponse (b : Triple) (rhs : Bool) : Triple :=
…

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Triple

  7. theorem OAI.MaxCutGames.Reduction.Incidence.local_count_bound line 36
  8. theorem OAI.MaxCutGames.Reduction.Incidence.best_response_exact line 43
  9. structure OAI.MaxCutGames.Reduction.Incidence.Equation line 48
  10. inductive OAI.MaxCutGames.Reduction.Incidence.Slot line 54
  11. def OAI.MaxCutGames.Reduction.Incidence.nameAt line 60
  12. def OAI.MaxCutGames.Reduction.Incidence.bitAt line 65
  13. def OAI.MaxCutGames.Reduction.Incidence.questionPredicate line 71

    Source documentation

    A predicate of the actual questions and answers, with no hidden slot input.

    def questionPredicate (e : Equation Variable) (name : Variable)
    (alice : Triple) (bob : Bool) : Prop :=
…

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Equation, OAI.MaxCutGames.Reduction.Incidence.Triple

  14. theorem OAI.MaxCutGames.Reduction.Incidence.question_predicate_at_slot line 79

    Source documentation

    Cloning supplies exactly the distinctness needed to recover a slot from its name.

    theorem question_predicate_at_slot (e : Equation Variable)
    (distinct₁₂ : e.first ≠ e.second) (distinct₁₃ : e.first ≠ e.third)
    (distinct₂₃ : e.second ≠ e.third) (alice : Triple) (bob : Bool) (slot : Slot) :
    questionPredicate e (nameAt e slot) alice bob ↔
      parity alice = e.rhs ∧ bitAt alice slot = bob := by
…

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Equation, OAI.MaxCutGames.Reduction.Incidence.Triple, OAI.MaxCutGames.Reduction.Incidence.Slot, OAI.MaxCutGames.Reduction.Incidence.questionPredicate, OAI.MaxCutGames.Reduction.Incidence.nameAt, OAI.MaxCutGames.Reduction.Incidence.parity, OAI.MaxCutGames.Reduction.Incidence.bitAt

  15. def OAI.MaxCutGames.Reduction.Incidence.bobTriple line 89

    Source documentation

    Bob receives only a variable name: the strategy has no occurrence input.

    def bobTriple (g : Variable → Bool) (e : Equation Variable) : Triple :=
…

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Equation, OAI.MaxCutGames.Reduction.Incidence.Triple

  16. def OAI.MaxCutGames.Reduction.Incidence.acceptedCount line 93

    Source documentation

    An occurrence index supplies Alice's full question and its equation.

    def acceptedCount (equations : Index → Equation Variable)
    (g : Variable → Bool) (alice : Index → Triple) : List Index → Nat
  | [] => 0
  | i :: rest =>
    acceptedSlots (alice i) (bobTriple g (equations i)) (equations i).rhs +
      acceptedCount equations g alice rest

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Equation, OAI.MaxCutGames.Reduction.Incidence.Triple, OAI.MaxCutGames.Reduction.Incidence.acceptedSlots, OAI.MaxCutGames.Reduction.Incidence.bobTriple

  17. def OAI.MaxCutGames.Reduction.Incidence.failureCount line 100
  18. theorem OAI.MaxCutGames.Reduction.Incidence.total_count_bound line 107
  19. def OAI.MaxCutGames.Reduction.Incidence.optimalAlice line 118
  20. theorem OAI.MaxCutGames.Reduction.Incidence.optimal_alice_exact line 122
  21. theorem OAI.MaxCutGames.Reduction.Incidence.fixed_bob_optimum line 134

    Source documentation

    Exact finite-count form of max_Alice Pr[accept | Bob = g] = 1 - u(g)/3.

    theorem fixed_bob_optimum (equations : Index → Equation Variable)
    (g : Variable → Bool) (occurrences : List Index) :
    ∃ alice : Index → Triple,
      acceptedCount equations g alice occurrences + failureCount equations g occurrences =
        3 * occurrences.length ∧
      ∀ other : Index → Triple,
        acceptedCount equations g other occurrences ≤
          acceptedCount equations g alice occurrences := by
…

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Equation, OAI.MaxCutGames.Reduction.Incidence.Triple, OAI.MaxCutGames.Reduction.Incidence.acceptedCount, OAI.MaxCutGames.Reduction.Incidence.failureCount

  22. theorem OAI.MaxCutGames.Reduction.Incidence.soundness_191_over_192 line 148
  23. theorem OAI.MaxCutGames.Reduction.Incidence.game_soundness_191_over_192 line 156

    Source documentation

    The same bound holds for every deterministic pair when every Bob assignment has the gap.

    theorem game_soundness_191_over_192 (equations : Index → Equation Variable)
    (occurrences : List Index)
    (source_gap : ∀ g : Variable → Bool,
      occurrences.length ≤ 64 * failureCount equations g occurrences) :
    ∀ (g : Variable → Bool) (alice : Index → Triple),
      64 * acceptedCount equations g alice occurrences ≤ 191 * occurrences.length := by
…

    Mentions: OAI.MaxCutGames.Reduction.Incidence.Equation, OAI.MaxCutGames.Reduction.Incidence.failureCount, OAI.MaxCutGames.Reduction.Incidence.Triple, OAI.MaxCutGames.Reduction.Incidence.acceptedCount

  24. def OAI.MaxCutGames.Reduction.SourceIncidence.toIncidence line 171
  25. theorem OAI.MaxCutGames.Reduction.SourceIncidence.failedEquation_eq line 174
  26. theorem OAI.MaxCutGames.Reduction.SourceIncidence.failureCount_eq line 181
  27. def OAI.MaxCutGames.Reduction.SourceIncidence.occurrenceList line 192

    Source documentation

    The full occurrence is the displayed equation together with a fresh index.

    def occurrenceList (source : List (CloneGap.Equation Name)) :=
…

    Mentions: OAI.MaxCutGames.Reduction.CloneGap.Equation

  28. theorem OAI.MaxCutGames.Reduction.SourceIncidence.cloned_occurrence_gap line 195
  29. theorem OAI.MaxCutGames.Reduction.SourceIncidence.source_to_incidence_soundness line 214
  30. abbrev OAI.MaxCutGames.Reduction.FiniteSource.Name line 230
  31. def OAI.MaxCutGames.Reduction.FiniteSource.clonedSource line 232
  32. abbrev OAI.MaxCutGames.Reduction.FiniteSource.Occurrence line 234
  33. def OAI.MaxCutGames.Reduction.FiniteSource.occurrences line 236
  34. def OAI.MaxCutGames.Reduction.FiniteSource.rawEquation line 239
  35. def OAI.MaxCutGames.Reduction.FiniteSource.finiteName line 244

    Source documentation

    Total conversion; membership proofs below establish that every index used by the construction is already below 48, so the remainder changes none.

    def finiteName (s : ActualSource.Source) (v : Fin s.«variables» × Nat) : Name s :=
…

    Mentions: OAI.MaxCutGames.Reduction.ActualSource.Source, OAI.MaxCutGames.Reduction.FiniteSource.Name

  36. def OAI.MaxCutGames.Reduction.FiniteSource.mapEquation line 247
  37. def OAI.MaxCutGames.Reduction.FiniteSource.equation line 250
  38. theorem OAI.MaxCutGames.Reduction.FiniteSource.satisfied_map line 253
  39. theorem OAI.MaxCutGames.Reduction.FiniteSource.mem_cart line 256
  40. theorem OAI.MaxCutGames.Reduction.FiniteSource.distinctTriple_bounds line 266
  41. theorem OAI.MaxCutGames.Reduction.FiniteSource.distinctTriples_nonempty line 273
  42. theorem OAI.MaxCutGames.Reduction.FiniteSource.cloned_member_properties line 278
  43. theorem OAI.MaxCutGames.Reduction.FiniteSource.raw_properties line 289
  44. theorem OAI.MaxCutGames.Reduction.FiniteSource.finiteName_injective_on line 298
  45. theorem OAI.MaxCutGames.Reduction.FiniteSource.names_distinct line 304
  46. theorem OAI.MaxCutGames.Reduction.FiniteSource.raw_map_occurrences line 313
  47. theorem OAI.MaxCutGames.Reduction.FiniteSource.occurrences_length line 317
  48. theorem OAI.MaxCutGames.Reduction.FiniteSource.clonedSource_nonempty line 321
  49. instance OAI.MaxCutGames.Reduction.FiniteSource.(instance at line 327) line 327
  50. theorem OAI.MaxCutGames.Reduction.FiniteSource.indexed_failure_count line 330
  51. theorem OAI.MaxCutGames.Reduction.FiniteSource.indexed_gap line 337
  52. theorem OAI.MaxCutGames.Reduction.FiniteSource.indexed_completeness_count line 346
  53. def OAI.MaxCutGames.Reduction.FiniteSource.incidenceEquation line 357
  54. theorem OAI.MaxCutGames.Reduction.FiniteSource.incidence_question_predicate line 360
  55. theorem OAI.MaxCutGames.Reduction.FiniteSource.incidence_failure_gap line 369
  56. theorem OAI.MaxCutGames.Reduction.FiniteSource.incidence_soundness line 379
  57. def OAI.MaxCutGames.Reduction.FiniteSource.nameEquiv line 388

    Source documentation

    Executable row-major encoding of the finite clone names.

    def nameEquiv (s : ActualSource.Source) : Name s ≃ Fin (s.«variables» * 48) :=
…

    Mentions: OAI.MaxCutGames.Reduction.ActualSource.Source, OAI.MaxCutGames.Reduction.FiniteSource.Name

  58. def OAI.MaxCutGames.Reduction.FiniteSource.cloned line 391
  59. theorem OAI.MaxCutGames.Reduction.FiniteSource.cloned_length line 397
  60. theorem OAI.MaxCutGames.Reduction.FiniteSource.cloned_distinct line 402
  61. theorem OAI.MaxCutGames.Reduction.FiniteSource.count_ofFn line 409
  62. theorem OAI.MaxCutGames.Reduction.FiniteSource.cloned_gap line 416
  63. theorem OAI.MaxCutGames.Reduction.FiniteSource.cloned_completeness_count line 431
  64. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.sum_bool_indicator_eq_count_ofFn line 453
  65. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.expect_bool_indicator_eq_count_ofFn line 462

    Source documentation

    Uniform Boolean-event probability is the indexed list's exact occurrence count.

    theorem expect_bool_indicator_eq_count_ofFn {n : Nat} (p : Fin n → Bool) :
    Finset.univ.expect (fun i : Fin n => if p i then (1 : ℚ) else 0) =
      ((List.ofFn p).countP id : ℚ) / n := by
…
  66. def OAI.MaxCutGames.Reduction.IncidenceProbability.slotOfFin line 468
  67. def OAI.MaxCutGames.Reduction.IncidenceProbability.slotPredicate line 471
  68. instance OAI.MaxCutGames.Reduction.IncidenceProbability.(instance at line 476) line 476
  69. def OAI.MaxCutGames.Reduction.IncidenceProbability.slotAcceptance line 479
  70. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.slot_predicate_is_question_predicate line 482
  71. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.sum_slot_acceptance line 490
  72. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.expect_slot_acceptance line 504
  73. def OAI.MaxCutGames.Reduction.IncidenceProbability.acceptanceProbability line 513
  74. def OAI.MaxCutGames.Reduction.IncidenceProbability.failureProbability line 518
  75. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.acceptance_probability_eq_expected_count line 522
  76. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.acceptance_probability_nonnegative line 531
  77. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.acceptance_probability_le_one line 539
  78. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.acceptance_plus_failure_third_le_one line 547
  79. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.deterministic_soundness line 560
  80. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.failureCount_eq_countP line 567
  81. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.failure_count_finRange_eq_count_ofFn line 579
  82. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.failure_probability_eq_count_finRange line 590
  83. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.failure_gap_of_count_gap line 602
  84. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.soundness_from_count_gap line 613
  85. def OAI.MaxCutGames.Reduction.IncidenceProbability.randomizedAcceptance line 622

    Source documentation

    A finite randomized strategy, with the common coin including both private coins.

    def randomizedAcceptance [Fintype Coin] (equations : Index → Equation Variable)
    (weight : Coin → ℚ) (alice : Coin → Index → Triple)
    (bob : Coin → Variable → Bool) : ℚ :=
…
  86. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.randomized_soundness line 627
  87. instance OAI.MaxCutGames.Reduction.IncidenceProbability.tripleFintype line 644
  88. instance OAI.MaxCutGames.Reduction.IncidenceProbability.tripleInhabited line 651
  89. def OAI.MaxCutGames.Reduction.IncidenceProbability.deterministicValue line 654

    Source documentation

    The actual game value is the maximum over all deterministic local strategies.

    noncomputable def deterministicValue [Fintype Variable]
    (equations : Index → Equation Variable) : ℚ := by
…
  90. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.acceptance_le_value line 661
  91. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.value_attained line 669
  92. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.value_soundness line 678
  93. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.randomized_acceptance_le_value line 687
  94. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.randomized_value_attained line 703

    Source documentation

    Constant choices of an optimal strategy attain the value under any normalized coin law.

    theorem randomized_value_attained [Fintype Variable] [Fintype Coin]
    (equations : Index → Equation Variable) (weight : Coin → ℚ)
    (weight_sum : ∑ c, weight c = 1) :
    ∃ (alice : Coin → Index → Triple) (bob : Coin → Variable → Bool),
      randomizedAcceptance equations weight alice bob = deterministicValue equations := by
…

    Mentions: OAI.MaxCutGames.Reduction.IncidenceProbability.randomizedAcceptance, OAI.MaxCutGames.Reduction.IncidenceProbability.deterministicValue

  95. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.cloned_failure_probability_gap line 712
  96. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.cloned_value_soundness line 722

    Source documentation

    Actual finite incidence-game value after the concrete 48-clone construction.

    theorem cloned_value_soundness (s : ActualSource.Source)
    (source_gap : ∀ A : Fin s.«variables» → Bool,
      s.sourceList.length ≤ 4 * s.sourceList.countP (fun e => !CloneGap.satisfied e A)) :
    deterministicValue (FiniteSource.incidenceEquation s) ≤ (191 : ℚ) / 192 := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualSource.Source, OAI.MaxCutGames.Reduction.CloneGap.satisfied, OAI.MaxCutGames.Reduction.IncidenceProbability.deterministicValue, OAI.MaxCutGames.Reduction.FiniteSource.incidenceEquation

  97. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.cloned_randomized_soundness line 728
  98. def OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.uniformDistribution line 747
  99. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.uniform_probability_eq_rat_expect line 755
  100. def OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.functionalTriple line 767
  101. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.functionalTriple_bitAt line 769
  102. def OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.extractionIncidence line 773
  103. def OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.DistinctNames line 778
  104. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.extraction_names_injective line 783
  105. def OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.foundationGame line 795
  106. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.foundation_success_eq_rat_acceptance line 804
  107. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.foundation_value_soundness line 834
  108. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.foundation_value_le_one_sub_gap_third line 846
  109. def OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.sourceEquation line 860
  110. def OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.sourceGame line 863
  111. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.source_failure_probability line 867
  112. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.source_value_le_one_sub_gap_third line 875
  113. theorem OAI.MaxCutGames.Reduction.IncidenceProbability.FoundationBridge.cloned_foundation_value_soundness line 884