OAI/Computability/UniqueGames/Decoding/ActualAdviceStochasticBridgeLemmas.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Actual randomized point policies are transported locally into Boolean answer kernels. Complete response tables are selected only after public advice is fixed and before the remaining questions. No global deterministic policy independent of public advice is asserted or needed for this upper bound.

  1. instance OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.sourceAnswerNonempty line 34
  2. instance OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.targetAnswerNonempty line 35
  3. structure OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.Policies line 38
  4. def OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.extendTargetKernel line 45
  5. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.extendTargetKernel_apply line 55
  6. def OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.firstResponse line 64
  7. def OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.secondResponse line 72
  8. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.decodeFirstMap_actual line 82
  9. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.decodeSecondMap_actual line 102
  10. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.firstResponse_actual line 113
  11. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.secondResponse_actual line 125
  12. def OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.fixedMapSuccess line 138

    Source documentation

    Two private finite answer draws, after receiving the respective actual question and linear row map. Acceptance is equality under the real projection.

    def fixedMapSuccess (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N) (policy : Policies k g D)
    (J : Finset (Fin k)) (Y : RawPoint J →ₗ[F2] D) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.Policies

  13. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.fixedMapSuccess_le line 147
  14. def OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.responses line 191
  15. def OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.success line 199
  16. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.success_le_native_stochastic line 206
  17. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.success_le_some_native line 230
  18. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBound.deterministic_success_le_dimension line 256
  19. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBound.stochastic_success_le_dimension line 274

    Source documentation

    Arbitrary local randomized point policies obey the same bound. Complete deterministic response tables may be chosen after the public mask/advice is fixed, but before the remaining question pair is drawn.

    theorem stochastic_success_le_dimension (coordinates : D ≃ₗ[F2] (Q → F2))
    (g : IncidenceExtraction.Incidence O N) (ω : FiniteDistribution O)
    (policy : ActualAdviceStochasticBridge.Policies k g D)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (hopt : IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5)
    (dimW rs : ℕ) (hcard : Fintype.card D ≤ 2 ^ (dimW + rs)) :
    ActualAdviceStochasticBridge.success (IncidenceGap.slotLaw ω) g policy β hβ₀ hβ₁ ≤
      (1 - (β / (2 : ℝ) ^ (dimW + rs)) / 3600) ^ k := by
…

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.Policies, OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue, OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.success, OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw

  20. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBound.stochastic_success_le_dimension_finite line 290
  21. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.visibleMap line 331

    Source documentation

    The precise visible table (T,A M), with the second component in its actual attainable range. The argument order is complement, hidden matrix.

    def visibleMap (A : K →ₗ[F2] R) {J : Finset (Fin k)}
    (T : RawPoint J →ₗ[F2] W) (M : RawPoint J →ₗ[F2] K) :
    RawPoint J →ₗ[F2] (W × A.range) :=
…
  22. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.visibleMap_apply line 337
  23. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.rawMapPairCoefficientsEquiv line 341
  24. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.visibleMap_raw line 348
  25. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.uniform_visible_maps line 355

    Source documentation

    Equality for every observable proves the whole joint visible-map law.

    theorem uniform_visible_maps (A : K →ₗ[F2] R) (J : Finset (Fin k))
    (H : (RawPoint J →ₗ[F2] (W × A.range)) → ℝ) :
    (𝔼 TM : (RawPoint J →ₗ[F2] W) × (RawPoint J →ₗ[F2] K),
      H (visibleMap A TM.1 TM.2)) =
      𝔼 Y : RawPoint J →ₗ[F2] (W × A.range), H Y := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.visibleMap

  26. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.uniform_visible_maps_expectation line 371
  27. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.actualSuccess line 385

    Source documentation

    Actual success starts with genuinely sampled hidden and complement maps. The iid incidence law includes every slot choice, including unused choices at full positions. Policies receive only their respective visible table.

    def actualSuccess (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N) (A : K →ₗ[F2] R)
    (policy : ActualAdviceStochasticBridge.Policies k g (W × A.range))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) : ℝ :=
…
  28. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.actualSuccess_eq_cleanSuccess line 397
  29. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.drawDistribution line 416
  30. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.paddedDistribution line 430
  31. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.paddedDistribution_totalVariation_eq_slope line 437

    Source documentation

    Padding adds an independent uniform affine intercept. The full map's variation is therefore exactly the sparse slope variation used in constants.

    theorem paddedDistribution_totalVariation_eq_slope (rhs : Fin k → Bool) (β : ℝ)
    (hβ : 0 ≤ β) (hβ' : β ≤ 1) :
    (paddedDistribution (V := V) rhs β hβ hβ').totalVariation
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.paddedDistribution

  32. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.paddedDistribution_totalVariation line 446
  33. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.withKernel line 460

    Source documentation

    Keep the common outer datum while sampling its conditional table law.

    def withKernel (μ : FiniteDistribution Ω) (p : Ω → FiniteDistribution Y) :
    FiniteDistribution (Ω × Y) where
…
  34. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.withKernel_totalVariation line 469
  35. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.withKernel_totalVariation_le line 485
  36. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.wholeAdvice_totalVariation line 501

    Source documentation

    Whole (occurrences, public advice, Mπ,Tπ) comparison. The product codomain represents the two genuine sampled maps; occurrence weights are arbitrary and remain in both laws. The public law can in particular be uniform on all row maps. Projection choices are averaged out before this comparison.

    theorem wholeAdvice_totalVariation {k : ℕ} {Id A V : Type}
    [Fintype Id] [Fintype A] [AddCommGroup V] [Module F2 V] [Fintype V]
    [Fintype (ActualHomogeneous.E k →ₗ[F2] V)]
    (occurrences : FiniteDistribution (Fin k → Id)) (publicLaw : FiniteDistribution A)
    (rhs : Id → Bool) (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) :
    (withKernel (occurrences.product publicLaw)
      (fun ua => paddedDistribution (V := V) (fun j => rhs (ua.1 j)) β hβ hβ')).totalVariation
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.withKernel, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.paddedDistribution

  37. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.wholeAdvice_totalVariation_eq_slope line 516

    Source documentation

    Common occurrence/public randomness preserves the exact slope variation.

    theorem wholeAdvice_totalVariation_eq_slope {k : ℕ} {Id A V : Type}
    [Fintype Id] [Fintype A] [AddCommGroup V] [Module F2 V] [Fintype V]
    [Fintype (ActualHomogeneous.E k →ₗ[F2] V)]
    (occurrences : FiniteDistribution (Fin k → Id)) (publicLaw : FiniteDistribution A)
    (rhs : Id → Bool) (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) :
    (withKernel (occurrences.product publicLaw)
      (fun ua => paddedDistribution (V := V) (fun j => rhs (ua.1 j)) β hβ hβ')).totalVariation
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.withKernel, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.paddedDistribution

  38. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.wholeAdvice_totalVariation_le_slope line 532
  39. instance OAI.UniqueGamesTheorem.Decoder.AdviceLaw.observedRowsFintype line 552
  40. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.observed_hidden_independent line 558

    Source documentation

    After fixing the mask, public map and complement table, the uniform hidden matrix has independent uniform attainable rows and private kernel coordinates. The observation fixes only A M, not M or a chosen witness.

    theorem observed_hidden_independent (J : Finset (Fin k)) (A : K →ₗ[F2] R)
    (f : AdviceFibers.ObservedRow (E := RawPoint J) A → ℝ)
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow

  41. abbrev OAI.UniqueGamesTheorem.Decoder.AdviceLaw.ProjectionSeed line 575

    Source documentation

    The actual two-stage sampler retains both its projection choices and its uniform map on that projected target. Thus target advice is not forgotten.

    abbrev ProjectionSeed (k : ℕ) (V : Type) [AddCommGroup V] [Module F2 V] :=
…
  42. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.projectionSeedDistribution line 579
  43. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.projectSeedMap line 590
  44. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.projectionSeed_expectation line 596
  45. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.projectionSeed_pushforward line 620
  46. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seedToActualDraw line 640

    Source documentation

    Convert the actual two-stage seed into the full hidden experiment. The second summand of the seed remains available for the target-side observation.

    def seedToActualDraw (occ : Fin k → Id) (A : K →ₗ[F2] R)
    (s : ProjectionSeed k (K × W)) : AdviceExperiment.Draw k Id K W R where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.ProjectionSeed, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw

  47. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seed_projection line 649
  48. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seed_padded_pair line 655
  49. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seed_left_observation line 662
  50. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seed_right_observation line 671
  51. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choiceDistribution line 684
  52. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.maskSlotChoice line 691

    Source documentation

    Full positions discard their auxiliary slot; singleton positions retain it.

    def maskSlotChoice (p : Bool × Fin 3) : PaddedLaw.ProjectionChoice :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice

  53. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.maskSlotChoice_pushforward line 694
  54. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choicesOfMaskSlots line 705
  55. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choices_expectation line 712

    Source documentation

    The Option sampler is exactly the Bernoulli-mask sampler with independent uniform slots at every position, including the full positions. This identity allows arbitrary functions of the retained choices.

    theorem choices_expectation {k : ℕ} (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (H : (Fin k → PaddedLaw.ProjectionChoice) → ℝ) :
    ((choiceDistribution β hβ hβ').iid k).expectation H =
      ((bernoulli β hβ hβ').iid k).expectation (fun mask =>
        (FiniteDistribution.uniform (Fin k → Fin 3)).expectation (fun slots =>
          H (choicesOfMaskSlots mask slots))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choiceDistribution, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choicesOfMaskSlots

  56. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choices_mask line 723
  57. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choices_active_slot line 731
  58. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.projectionSeed_mask_slots_expectation line 738

    Source documentation

    The same identity with the entire original target map retained. This is the full two-stage seed law, not merely the law of its padded marginal.

    theorem projectionSeed_mask_slots_expectation {k : ℕ} {V : Type}
    [AddCommGroup V] [Module F2 V] [Fintype V]
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (H : ProjectionSeed k V → ℝ) :
    (projectionSeedDistribution β hβ hβ').expectation H =
      ((bernoulli β hβ hβ').iid k).expectation (fun mask =>
        (FiniteDistribution.uniform (Fin k → Fin 3)).expectation (fun slots =>
          (FiniteDistribution.uniform
            (RawPoint (PaddedLaw.choiceMask (choicesOfMaskSlots mask slots)) →ₗ[F2] V)).expectation
              (fun Y => H ⟨choicesOfMaskSlots mask slots, Y⟩))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.ProjectionSeed, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.projectionSeedDistribution, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceMask, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choicesOfMaskSlots

  59. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.product_pushforward_withKernel line 769
  60. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeedLaw line 795

    Source documentation

    A finite hidden sample whose actual Draw is seedToActualDraw.

    def fullSeedLaw {k : ℕ} {Id A V : Type} [Fintype Id] [Fintype A]
    [AddCommGroup V] [Module F2 V] [Fintype V]
    (occurrences : FiniteDistribution (Fin k → Id)) (publicLaw : FiniteDistribution A)
    (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) :=
…
  61. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeedPad line 801
  62. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeed_pad_law line 806
  63. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeed_totalVariation line 822
  64. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeed_totalVariation_eq_slope line 835
  65. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeed_totalVariation_le_slope line 850
  66. abbrev OAI.UniqueGamesTheorem.Decoder.AdviceLaw.FullSeed line 868
  67. abbrev OAI.UniqueGamesTheorem.Decoder.AdviceLaw.CompleteData line 875

    Source documentation

    Complete visible conditioning data: occurrences, public map, projection choices, the entire complement map, and precisely the attainable rows.

    abbrev CompleteData (k : ℕ) (Id K W R : Type)
    [AddCommGroup K] [Module F2 K] [AddCommGroup W] [Module F2 W]
    [AddCommGroup R] [Module F2 R] :=
…
  68. abbrev OAI.UniqueGamesTheorem.Decoder.AdviceLaw.PrivateMap line 883
  69. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.targetObservationEquiv line 886
  70. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeedCoordinatesEquiv line 897

    Source documentation

    A global bijection retains all actual visible data, with exactly one uniform kernel-valued matrix left after conditioning.

    def fullSeedCoordinatesEquiv :
    FullSeed k Id K W R ≃ Σ d : CompleteData k Id K W R, PrivateMap d :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.FullSeed, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.CompleteData, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.PrivateMap

  71. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve line 908
  72. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeAssemble line 911
  73. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve_eq line 915
  74. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeAssemble_eq line 920
  75. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve_assemble line 925
  76. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeFiberEquiv line 931

    Source documentation

    Exact equivalence for a fiber of the complete observation, not just the marginal row observation. This is the input for finite conditioning.

    def completeFiberEquiv (d : CompleteData k Id K W R) :
    PrivateMap d ≃ {s : FullSeed k Id K W R // completeObserve s = d} :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.CompleteData, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.PrivateMap, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.FullSeed, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve

  77. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeFiberEquiv_val line 936
  78. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeDraw line 940

    Source documentation

    The actual Draw obtained from the complete-data fiber coordinates.

    def completeDraw (d : CompleteData k Id K W R) (N : PrivateMap d) :
    AdviceExperiment.Draw k Id K W R where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.CompleteData, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.PrivateMap, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw

  79. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeDraw_seed line 949
  80. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeDraw_rows line 953
  81. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeDraw_left line 958
  82. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeDraw_right line 969
  83. def OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeWeight line 981
  84. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeed_weight_observed line 991

    Source documentation

    The actual law has exactly constant point weights on every fiber of all observed data, even for arbitrary occurrence and public-map laws.

    theorem fullSeed_weight_observed (occurrences : FiniteDistribution (Fin k → Id))
    (publicLaw : FiniteDistribution (K →ₗ[F2] R)) (β : ℝ)
    (hβ : 0 ≤ β) (hβ' : β ≤ 1) (s : FullSeed k Id K W R) :
    (fullSeedLaw (V := K × W) occurrences publicLaw β hβ hβ').weight s =
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceLaw.FullSeed, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeedLaw

  85. theorem OAI.UniqueGamesTheorem.Decoder.AdviceLaw.fullSeed_weight_fiber line 998