OAI/Computability/MaxCut/Games/IncidenceExtraction.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

The next definitions separate local strategies from arbitrary joint strategies. Each question reconstruction and each answer extraction has access to only one player's question. A value conditioned on by an analysis may occur as a fixed parameter of a LocalSimulation; it cannot become an additional random input.

  1. abbrev OAI.MaxCutGames.Soundness.IncidenceExtraction.Triple line 8
  2. def OAI.MaxCutGames.Soundness.IncidenceExtraction.xorTriple line 10
  3. structure OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence line 12
  4. def OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence.accepts line 16
  5. def OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence.namedAccepts line 23

    Source documentation

    The incidence predicate as a game on the actual questions (o,n), with the retained slot left internal to the verifier.

    def Incidence.namedAccepts {Occurrence Name : Type}
    (g : Incidence Occurrence Name) (o : Occurrence) (n : Name)
    (a : Triple) (b : Bool) : Prop :=
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence, OAI.MaxCutGames.Soundness.IncidenceExtraction.Triple

  6. theorem OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence.accepts_implies_namedAccepts line 28
  7. theorem OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence.namedAccepts_iff_accepts line 36

    Source documentation

    Distinct names make the named-variable predicate equivalent to the sampled retained-slot predicate, without revealing that slot to either strategy.

    theorem Incidence.namedAccepts_iff_accepts {Occurrence Name : Type}
    (g : Incidence Occurrence Name)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (o : Occurrence) (i : Fin 3) (a : Triple) (b : Bool) :
    g.namedAccepts o (g.name o i) a b ↔ g.accepts o i a b := by
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence, OAI.MaxCutGames.Soundness.IncidenceExtraction.Triple

  8. structure OAI.MaxCutGames.Soundness.IncidenceExtraction.FullPoint line 47
  9. def OAI.MaxCutGames.Soundness.IncidenceExtraction.FullPoint.valid line 51
  10. structure OAI.MaxCutGames.Soundness.IncidenceExtraction.PartnerPoint line 56
  11. def OAI.MaxCutGames.Soundness.IncidenceExtraction.AugmentedAccepts line 61

    Source comment

    Only the single positions matter to the extracted incidence game.
    def AugmentedAccepts {Position Occurrence Name : Type}
    (g : Incidence Occurrence Name) (u : Position → Occurrence)
    (active : Position → Prop) (slot : Position → Fin 3)
    (eA : FullPoint Position) (eB : PartnerPoint Position) : Prop :=
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence, OAI.MaxCutGames.Soundness.IncidenceExtraction.FullPoint, OAI.MaxCutGames.Soundness.IncidenceExtraction.PartnerPoint

  12. def OAI.MaxCutGames.Soundness.IncidenceExtraction.RepeatedAccepts line 68
  13. theorem OAI.MaxCutGames.Soundness.IncidenceExtraction.augmented_accepts_implies_repeated_accepts line 76

    Source documentation

    Acceptance of the augmented projection game implies acceptance of every incidence coordinate in any subset of the active positions.

    theorem augmented_accepts_implies_repeated_accepts
    {Position Occurrence Name : Type}
    (g : Incidence Occurrence Name) (u : Position → Occurrence)
    (active inside : Position → Prop) (slot : Position → Fin 3)
    (eA : FullPoint Position) (eB : PartnerPoint Position)
    (hinside : ∀ j, inside j → active j)
    (haccept : AugmentedAccepts g u active slot eA eB) :
    RepeatedAccepts g u slot inside eA.coords eB.single := by
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence, OAI.MaxCutGames.Soundness.IncidenceExtraction.FullPoint, OAI.MaxCutGames.Soundness.IncidenceExtraction.PartnerPoint, OAI.MaxCutGames.Soundness.IncidenceExtraction.AugmentedAccepts, OAI.MaxCutGames.Soundness.IncidenceExtraction.RepeatedAccepts

  14. theorem OAI.MaxCutGames.Soundness.IncidenceExtraction.augmented_accepts_implies_named_repeated_accepts line 93

    Source documentation

    The same containment stated on the occurrence/name question vectors actually given to the two repeated-game players.

    theorem augmented_accepts_implies_named_repeated_accepts
    {Position RepeatPosition Occurrence Name : Type}
    (g : Incidence Occurrence Name) (u : Position → Occurrence)
    (active : Position → Prop) (slot : Position → Fin 3)
    (embed : RepeatPosition → Position)
    (eA : FullPoint Position) (eB : PartnerPoint Position)
    (hinside : ∀ r, active (embed r))
    (haccept : AugmentedAccepts g u active slot eA eB) :
    ∀ r, g.namedAccepts (u (embed r))
      (g.name (u (embed r)) (slot (embed r)))
      (eA.coords (embed r)) (eB.single (embed r)) := by
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence, OAI.MaxCutGames.Soundness.IncidenceExtraction.FullPoint, OAI.MaxCutGames.Soundness.IncidenceExtraction.PartnerPoint, OAI.MaxCutGames.Soundness.IncidenceExtraction.AugmentedAccepts

  15. structure OAI.MaxCutGames.Soundness.IncidenceExtraction.Game line 119
  16. structure OAI.MaxCutGames.Soundness.IncidenceExtraction.Strategies line 122
  17. def OAI.MaxCutGames.Soundness.IncidenceExtraction.Strategies.wins line 126
  18. structure OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation line 130
  19. def OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation.induced line 142
  20. theorem OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation.induced_wins line 154

    Source documentation

    A local simulation transports every deterministic strategy and contains its winning event pointwise. No shared access to the questions is used.

    theorem LocalSimulation.induced_wins
    {InnerQA InnerQB InnerA InnerB OuterQA OuterQB OuterA OuterB : Type}
    {inner : Game InnerQA InnerQB InnerA InnerB}
    {outer : Game OuterQA OuterQB OuterA OuterB}
    (r : LocalSimulation inner outer)
    (s : Strategies OuterQA OuterQB OuterA OuterB)
    (qa : InnerQA) (qb : InnerQB)
    (hwins : s.wins outer (r.questionA qa) (r.questionB qb)) :
    (r.induced s).wins inner qa qb :=
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Game, OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation, OAI.MaxCutGames.Soundness.IncidenceExtraction.Strategies

  21. theorem OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation.seeded_induced_wins line 167

    Source documentation

    Fixing strategy randomness gives another local deterministic strategy; the simulation proof applies to every seed, before any averaging.

    theorem LocalSimulation.seeded_induced_wins
    {InnerQA InnerQB InnerA InnerB OuterQA OuterQB OuterA OuterB Seed : Type}
    {inner : Game InnerQA InnerQB InnerA InnerB}
    {outer : Game OuterQA OuterQB OuterA OuterB}
    (r : LocalSimulation inner outer)
    (strategy : Seed → Strategies OuterQA OuterQB OuterA OuterB)
    (seed : Seed) (qa : InnerQA) (qb : InnerQB)
    (hwins : (strategy seed).wins outer (r.questionA qa) (r.questionB qb)) :
    (r.induced (strategy seed)).wins inner qa qb :=
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Game, OAI.MaxCutGames.Soundness.IncidenceExtraction.LocalSimulation, OAI.MaxCutGames.Soundness.IncidenceExtraction.Strategies

  22. def OAI.MaxCutGames.Soundness.ConcreteExtraction.slotIndex line 189
  23. def OAI.MaxCutGames.Soundness.ConcreteExtraction.tripleCoordinates line 194
  24. theorem OAI.MaxCutGames.Soundness.ConcreteExtraction.parity_coordinates line 197
  25. theorem OAI.MaxCutGames.Soundness.ConcreteExtraction.retained_coordinates line 200
  26. def OAI.MaxCutGames.Soundness.ConcreteExtraction.fullPoint line 204
  27. def OAI.MaxCutGames.Soundness.ConcreteExtraction.partnerPoint line 208
  28. theorem OAI.MaxCutGames.Soundness.ConcreteExtraction.actual_projection_accepts line 214

    Source documentation

    Concrete projection acceptance implies the coordinate-level acceptance relation used to extract a repeated incidence strategy.

    theorem actual_projection_accepts
    {P O N : Type} (g : IncidenceExtraction.Incidence O N) (u : P → O)
    (active : P → Bool) (slot : P → PartnerProjection.Slot)
    (x : PartnerProjection.SourcePoint (fun j => g.rhs (u j)))
    (y : PartnerProjection.PartnerPoint (fun j => g.rhs (u j)) active)
    (hone : x.homogeneous = true)
    (hproject : PartnerProjection.project (fun j => g.rhs (u j)) active slot x = y) :
    IncidenceExtraction.AugmentedAccepts g u (fun j => active j = true)
      (fun j => slotIndex (slot j)) (fullPoint x) (partnerPoint y) := by
…

    Mentions: OAI.MaxCutGames.Soundness.IncidenceExtraction.Incidence, OAI.MaxCutGames.Soundness.PartnerProjection.Slot, OAI.MaxCutGames.Soundness.PartnerProjection.SourcePoint, OAI.MaxCutGames.Soundness.PartnerProjection.PartnerPoint, OAI.MaxCutGames.Soundness.PartnerProjection.project, OAI.MaxCutGames.Soundness.IncidenceExtraction.AugmentedAccepts, OAI.MaxCutGames.Soundness.ConcreteExtraction.slotIndex, OAI.MaxCutGames.Soundness.ConcreteExtraction.fullPoint, OAI.MaxCutGames.Soundness.ConcreteExtraction.partnerPoint

  29. theorem OAI.MaxCutGames.Soundness.ConcreteExtraction.actual_projection_implies_named_repetition line 237
  30. abbrev OAI.MaxCutGames.Reduction.ActualHomogeneous.E line 262
  31. abbrev OAI.MaxCutGames.Reduction.ActualHomogeneous.Ambient line 263
  32. def OAI.MaxCutGames.Reduction.ActualHomogeneous.tau line 265
  33. def OAI.MaxCutGames.Reduction.ActualHomogeneous.hBasis line 266
  34. def OAI.MaxCutGames.Reduction.ActualHomogeneous.firstBasis line 267
  35. def OAI.MaxCutGames.Reduction.ActualHomogeneous.secondBasis line 268
  36. def OAI.MaxCutGames.Reduction.ActualHomogeneous.coordinateBasis line 269
  37. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.tau_hBasis line 272
  38. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.tau_firstBasis line 273
  39. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.tau_secondBasis line 274
  40. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.pair_fst_ite line 276
  41. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.pair_snd_ite line 278
  42. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.coordinate_decomposition line 281
  43. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.linearMap_expansion line 291
  44. def OAI.MaxCutGames.Reduction.ActualHomogeneous.homogeneous line 298
  45. def OAI.MaxCutGames.Reduction.ActualHomogeneous.embed line 318
  46. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.embed_mem line 332
  47. def OAI.MaxCutGames.Reduction.ActualHomogeneous.equivalence line 341
  48. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.finrank_E line 363
  49. theorem OAI.MaxCutGames.Reduction.ActualHomogeneous.finrank_homogeneous line 366
  50. inductive OAI.MaxCutGames.Reduction.ActualCanonical.Record line 382
  51. def OAI.MaxCutGames.Reduction.ActualCanonical.recordEquiv line 388
  52. instance OAI.MaxCutGames.Reduction.ActualCanonical.(instance at line 400) line 400
  53. abbrev OAI.MaxCutGames.Reduction.ActualCanonical.Data line 403
  54. def OAI.MaxCutGames.Reduction.ActualCanonical.pivot line 406
  55. def OAI.MaxCutGames.Reduction.ActualCanonical.translate line 409
  56. def OAI.MaxCutGames.Reduction.ActualCanonical.normalize line 410
  57. def OAI.MaxCutGames.Reduction.ActualCanonical.record line 412
  58. def OAI.MaxCutGames.Reduction.ActualCanonical.data line 420
  59. def OAI.MaxCutGames.Reduction.ActualCanonical.standardTriple line 424
  60. def OAI.MaxCutGames.Reduction.ActualCanonical.canonical line 427
  61. def OAI.MaxCutGames.Reduction.ActualCanonical.ambientEval line 431
  62. def OAI.MaxCutGames.Reduction.ActualCanonical.Represents line 435
  63. theorem OAI.MaxCutGames.Reduction.ActualCanonical.add_self line 439
  64. theorem OAI.MaxCutGames.Reduction.ActualCanonical.add_both line 445
  65. theorem OAI.MaxCutGames.Reduction.ActualCanonical.pivot_translate line 451
  66. theorem OAI.MaxCutGames.Reduction.ActualCanonical.normalize_translate line 457
  67. theorem OAI.MaxCutGames.Reduction.ActualCanonical.record_translate line 464
  68. theorem OAI.MaxCutGames.Reduction.ActualCanonical.data_gauge line 470
  69. theorem OAI.MaxCutGames.Reduction.ActualCanonical.data_global_shift line 480
  70. theorem OAI.MaxCutGames.Reduction.ActualCanonical.canonical_shift line 488
  71. theorem OAI.MaxCutGames.Reduction.ActualCanonical.ambientEval_hBasis line 502
  72. theorem OAI.MaxCutGames.Reduction.ActualCanonical.ambientEval_firstBasis line 507
  73. theorem OAI.MaxCutGames.Reduction.ActualCanonical.ambientEval_secondBasis line 519
  74. theorem OAI.MaxCutGames.Reduction.ActualCanonical.standard_represents line 532

    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.MaxCutGames.Reduction.ActualCanonical.Represents, OAI.MaxCutGames.Reduction.ActualCanonical.standardTriple

  75. theorem OAI.MaxCutGames.Reduction.ActualCanonical.extension_coefficients line 539

    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.MaxCutGames.Reduction.ActualCanonical.Represents

  76. theorem OAI.MaxCutGames.Reduction.ActualCanonical.canonical_eq_of_extension line 551

    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.MaxCutGames.Reduction.ActualCanonical.Represents, OAI.MaxCutGames.Reduction.ActualCanonical.canonical, OAI.MaxCutGames.Reduction.ActualCanonical.data

  77. theorem OAI.MaxCutGames.Reduction.ActualCanonical.extension_independent line 566
  78. def OAI.MaxCutGames.Reduction.ActualCanonical.singletonTriple line 574
  79. theorem OAI.MaxCutGames.Reduction.ActualCanonical.pivot_singleton line 577
  80. theorem OAI.MaxCutGames.Reduction.ActualCanonical.record_singleton line 582
  81. theorem OAI.MaxCutGames.Reduction.ActualCanonical.singleton_global_adjustment line 589
  82. theorem OAI.MaxCutGames.Reduction.ActualCanonical.singleton_locality line 595

    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.MaxCutGames.Reduction.ActualCanonical.record, OAI.MaxCutGames.Reduction.ActualCanonical.singletonTriple

  83. def OAI.MaxCutGames.Soundness.ActualCanonicalPullback.selectedFree line 617
  84. def OAI.MaxCutGames.Soundness.ActualCanonicalPullback.ambientCoefficients line 624
  85. def OAI.MaxCutGames.Soundness.ActualCanonicalPullback.freePullback line 631
  86. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.ofBit_and line 637
  87. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.inverse_homogeneous line 640
  88. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.inverse_first line 644
  89. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.inverse_second line 648
  90. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.inverse_retained_free line 652
  91. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.freePullback_expansion line 666
  92. def OAI.MaxCutGames.Soundness.ActualCanonicalPullback.outsideInsideEquiv line 680
  93. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.sum_outside_inside line 691
  94. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.raw_represents line 702
  95. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.canonical_raw_pullback line 730
  96. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.ambientCoefficients_single line 740
  97. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.ambientCoefficients_full_eq line 749
  98. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.raw_data_locality line 757

    Source documentation

    Raw canonical data is determined by the full displayed occurrences and retained variable names. Hidden single occurrences and slot indices vanish.

    theorem raw_data_locality [DecidableEq R] {Id Name : Type}
    (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (occ occ' : Fin k → Id) (slot slot' : Fin k → Slot)
    (gamma : RawCoefficients J R)
    (hfull : ∀ j, j ∉ J → occ j = occ' j)
    (hsingle : ∀ j, j ∈ J → names (occ j) (ConcreteExtraction.slotIndex (slot j)) =
      names (occ' j) (ConcreteExtraction.slotIndex (slot' j))) :
    ActualCanonical.data occ names rhs (gamma none) (ambientCoefficients J R gamma slot) =
      ActualCanonical.data occ' names rhs (gamma none) (ambientCoefficients J R gamma slot') := by
…

    Mentions: OAI.MaxCutGames.Soundness.ConcreteExtraction.slotIndex, OAI.MaxCutGames.Soundness.ActualCanonicalPullback.ambientCoefficients

  99. theorem OAI.MaxCutGames.Soundness.ActualCanonicalPullback.canonical_private_input_locality line 786

    Source documentation

    Lemma 6.2 for the actual pullbacks in the shared F₂ coordinate model.

    theorem canonical_private_input_locality [DecidableEq R]
    {Id Name : Type} [DecidableEq Id] [DecidableEq Name]
    (names : Id → Fin 3 → Name) (rhs : Id → F2)
    (occ occ' : Fin k → Id) (slot slot' : Fin k → Slot)
    (gamma : RawCoefficients J R)
    (hfull : ∀ j, j ∉ J → occ j = occ' j)
    (hsingle : ∀ j, j ∈ J → names (occ j) (ConcreteExtraction.slotIndex (slot j)) =
      names (occ' j) (ConcreteExtraction.slotIndex (slot' j))) :
    ActualCanonical.canonical occ names rhs
      (freePullback (fun j => toBit (rhs (occ j))) J R gamma slot) =
    ActualCanonical.canonical occ' names rhs
      (freePullback (fun j => toBit (rhs (occ' j))) J R gamma slot') := by
…

    Mentions: OAI.MaxCutGames.Soundness.ConcreteExtraction.slotIndex, OAI.MaxCutGames.Soundness.ActualCanonicalPullback.freePullback