OAI/Computability/UniqueGames/Decoding/ActualAdviceUpperLemmas.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

The clean-coordinate upper bound for the actual private-decoding policies. At every fixed public map A, the visible coefficient space is Vector d × A.range. Its cardinality is at most 2^(d+rs), including when A is rank deficient. The true independent uniform maps T,M, the Bernoulli mask, and all iid occurrence/position draws are retained by the proved sampling equality, before averaging over the uniform public map.

  1. instance OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.publicMapFintype line 35
  2. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.sourceIncidence line 40

    Source documentation

    The ordinary game uses actual occurrence IDs and actual variable names.

    def sourceIncidence (S : Source) :
    IncidenceExtraction.Incidence (Fin S.occurrences) (Fin S.variables) where
…
  3. abbrev OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.Visible line 45
  4. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.complementMap line 47
  5. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.rowMap line 52
  6. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.fullInput line 58

    Source documentation

    Decode only the data visible to the first player.

    def fullInput (S : Source) (A : Alphabet s →ₗ[F2] Vector rs)
    (occ : Fin k → Fin S.occurrences)
    (Y : ActualHomogeneous.E k →ₗ[F2] Visible d A) :
    VisiblePolicies.LeftInput S k s d (Vector rs) where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.Visible, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput

  7. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.projectedInput line 68

    Source documentation

    Decode only the displayed question and the visible row/complement maps.

    def projectedInput (S : Source) (A : Alphabet s →ₗ[F2] Vector rs)
    (J : Finset (Fin k)) (O : RawPrivateTable.SupportedV J (ActualGame.names S))
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] Visible d A) :
    VisiblePolicies.RightInput S J s d (Vector rs) where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.Visible, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.RightInput

  8. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.policies line 79

    Source documentation

    Actual observation-local stochastic policies, in the exact advice space used by the clean-coordinate experiment. Public A is fixed before questions.

    def policies (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (A : Alphabet s →ₗ[F2] Vector rs) :
    Clean.ActualAdviceStochasticBridge.Policies k (sourceIncidence S) (Visible d A) where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.Policies, OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.sourceIncidence, OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.Visible

  9. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.actualDraw line 90

    Source documentation

    The real draw corresponding to a fixed mask and the independently sampled complement and hidden matrices.

    def actualDraw (S : Source) (A : Alphabet s →ₗ[F2] Vector rs)
    (J : Finset (Fin k)) (occ : Fin k → Fin S.occurrences)
    (slot : Fin k → PartnerProjection.Slot)
    (T : RawPartnerTarget.RawPoint J →ₗ[F2] Vector d)
    (M : RawPartnerTarget.RawPoint J →ₗ[F2] Alphabet s) :
    AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector rs) where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.Draw

  10. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.fullInput_actual line 103
  11. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.projectedInput_actual line 113
  12. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.policyAgreement_actual line 126

    Source documentation

    The product of the two local policy kernels is literally the private decoder's observed agreement probability, before any expectations are taken.

    theorem policyAgreement_actual (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (A : Alphabet s →ₗ[F2] Vector rs) (J : Finset (Fin k))
    (occ : Fin k → Fin S.occurrences) (slot : Fin k → PartnerProjection.Slot)
    (T : RawPartnerTarget.RawPoint J →ₗ[F2] Vector d)
    (M : RawPartnerTarget.RawPoint J →ₗ[F2] Alphabet s) :
    (((policies S labeling good A).first J occ
        ((AdviceLaw.visibleMap A T M).comp
          (RawPrivateTable.projection J (ActualGame.rhs S) occ slot))).product
      ((policies S labeling good A).second J
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.policies, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.visibleMap

  13. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.source_projection_eq line 150

    Source documentation

    The clean experiment's indexed slot is exactly the actual bit projection; this includes the third-position parity intercept.

    theorem source_projection_eq (S : Source) (J : Finset (Fin k))
    (draw : Fin k → Fin S.occurrences × Fin 3) :
    Clean.ActualAdviceBridge.projection (sourceIncidence S) J draw =
      RawPrivateTable.projection J (ActualGame.rhs S) (fun j => (draw j).1)
        (fun j => Clean.ActualAdviceBridge.indexSlot (draw j).2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.projection, OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.sourceIncidence, OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.indexSlot

  14. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.fixed_public_map_bound line 158
  15. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.public_map_average_bound line 173

    Source documentation

    Rank deficiency is allowed separately at every public-map outcome.

    theorem public_map_average_bound
    {O N : Type} [Fintype O] [DecidableEq O] [Fintype N] [DecidableEq N]
    (g : IncidenceExtraction.Incidence O N) (ω : FiniteDistribution O)
    (policy : (A : Alphabet s →ₗ[F2] Vector rs) →
      Clean.ActualAdviceStochasticBridge.Policies k g (Visible d A))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (hopt : Clean.IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5) :
    (FiniteDistribution.uniform (Alphabet s →ₗ[F2] Vector rs)).expectation
        (fun A => AdviceLaw.actualSuccess (Clean.IncidenceGap.slotLaw ω) g A
          (policy A) β hβ₀ hβ₁) ≤
      (1 - (β / (2 : ℝ) ^ (d + rs)) / 3600) ^ k := by
…

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceStochasticBridge.Policies, OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.Visible, OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.actualSuccess, OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw

  16. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.actual_source_average_bound line 196

    Source documentation

    The actual policies selected from the two separate observations obey the bound under uniform occurrence IDs and every independent private response.

    theorem actual_source_average_bound (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (distinct : ∀ o i j, (sourceIncidence S).name o i =
      (sourceIncidence S).name o j → i = j)
    (hopt : Clean.IncidenceGap.parityValue (sourceIncidence S)
      (FiniteDistribution.uniform (Fin S.occurrences)) ≤ (4 : ℝ) / 5) :
    (FiniteDistribution.uniform (Alphabet s →ₗ[F2] Vector rs)).expectation
        (fun A => AdviceLaw.actualSuccess
          (Clean.IncidenceGap.slotLaw (FiniteDistribution.uniform (Fin S.occurrences)))
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.ActualAdviceUpper.sourceIncidence, OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.actualSuccess, OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw

  17. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceSampling.product_probability line 240
  18. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceSampling.fixedMapSuccess_eq_product line 249
  19. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceSampling.fixedMapSuccess_eq_observed line 270
  20. def OAI.UniqueGamesTheorem.Decoder.ActualAdviceSampling.sampledAgreement line 294

    Source documentation

    The actual experiment, before identifying its visible-map marginal with the clean-coordinate law. The two private answer draws are already averaged inside observedAgreement.

    def sampledAgreement (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (μ : FiniteDistribution (Fin S.occurrences × Fin 3))
    (A : Alphabet s →ₗ[F2] Vector rs)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness

  21. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceSampling.actualSuccess_eq_sampledAgreement line 310
  22. theorem OAI.UniqueGamesTheorem.Decoder.ActualAdviceSampling.sampledAgreement_average_bound line 328

    Source documentation

    The dimension bound for the true average of the actual observation-local decoders, including all ranks of the uniformly sampled public row map.

    theorem sampledAgreement_average_bound (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (distinct : ∀ o i j, (sourceIncidence S).name o i =
      (sourceIncidence S).name o j → i = j)
    (hopt : Clean.IncidenceGap.parityValue (sourceIncidence S)
      (FiniteDistribution.uniform (Fin S.occurrences)) ≤ (4 : ℝ) / 5) :
    (FiniteDistribution.uniform (Alphabet s →ₗ[F2] Vector rs)).expectation
      (fun A => sampledAgreement S labeling good
        (Clean.IncidenceGap.slotLaw (FiniteDistribution.uniform (Fin S.occurrences)))
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue, OAI.UniqueGamesTheorem.Decoder.ActualAdviceSampling.sampledAgreement, OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw

  23. theorem OAI.UniqueGamesTheorem.Decoder.ActualConditionalLaw.probability_condition_complete line 377
  24. theorem OAI.UniqueGamesTheorem.Decoder.ActualConditionalLaw.observedAgreement_completeDraw line 404

    Source documentation

    Both provers' answers, and their equality predicate, are fixed on the complete observation fiber. Only the hidden matrix varies within that fiber.

    theorem observedAgreement_completeDraw (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector r) → VisiblePolicies.ResponseWitness k → Prop)
    (data : AdviceLaw.CompleteData k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r))
    (N N' : AdviceLaw.PrivateMap data) :
    VisiblePolicies.observedAgreement S labeling good (AdviceLaw.completeDraw data N) =
      VisiblePolicies.observedAgreement S labeling good (AdviceLaw.completeDraw data N') := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.CompleteData, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.PrivateMap, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeDraw

  25. def OAI.UniqueGamesTheorem.Decoder.ActualConditionalLaw.datumAgreement line 416
  26. theorem OAI.UniqueGamesTheorem.Decoder.ActualConditionalLaw.datumAgreement_nonneg line 422
  27. theorem OAI.UniqueGamesTheorem.Decoder.ActualConditionalLaw.observedAgreement_seed line 431

    Source documentation

    The actual success observable factors through the complete visible datum; this justifies integrating a lower bound over visible-witness probability.

    theorem observedAgreement_seed (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector r) → VisiblePolicies.ResponseWitness k → Prop)
    (x : AdviceLaw.FullSeed k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector r)) :
    VisiblePolicies.observedAgreement S labeling good
      (AdviceLaw.seedToActualDraw x.1.1 x.1.2 x.2) =
        datumAgreement S labeling good (AdviceLaw.completeObserve x) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.FullSeed, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seedToActualDraw, OAI.UniqueGamesTheorem.Decoder.ActualConditionalLaw.datumAgreement, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve

  28. abbrev OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.Seed line 472
  29. abbrev OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.Datum line 475
  30. def OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.law line 478
  31. def OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.draw line 484
  32. def OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.pad line 487
  33. def OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.slice line 491
  34. def OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.targetHit line 496
  35. theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.pad_eq line 502

    Source documentation

    The padded comparison contains both complete affine component maps.

    theorem pad_eq (S : Source) (k s d r : ℕ) (x : Seed S k s d r) :
    pad S k s d r x =
      (((draw x).occurrences, AdviceExperiment.paddedComplement (ActualGame.rhs S) (draw x)),
        (LinearMap.toMatrix' (draw x).rowMap,
          MatrixCoordinates.mapEquiv k s (AdviceExperiment.paddedMatrix (ActualGame.rhs S) (draw x)))) :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.Seed, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.pad, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.draw, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.paddedComplement, OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.paddedMatrix

  36. theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.slice_eq_selectedEvent line 509
  37. theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.targetHit_eq_selectedMatch line 520
  38. theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.slice_good line 533

    Source documentation

    Positive selected-slice mass automatically supplies actual good left advice; goodness is not an independent projected experiment assumption.

    theorem slice_good (S : Source) (k s d r : ℕ)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) (α : ℝ)
    (x : Seed S k s d r) (hx : slice S k s d r labeling α x = true) :
    SelectedPolicies.GoodAdvice S labeling α
      (AdviceExperiment.leftObservation (ActualGame.rhs S) (draw x)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.Seed, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.slice, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.GoodAdvice, OAI.UniqueGamesTheorem.Decoder.AdviceExperiment.leftObservation, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.draw