ActualSeedPointwise.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Pointwise and uniform-law identification of the retained projection seed with the actual decoder draw. Auxiliary slots at full positions affect neither the projection nor the displayed target question. The entire target map is retained when it is repacked into its independent hidden and complement components.

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedPointwise.rawProjection_congr_slots line 26
theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedPointwise.supported_congr_slots line 46

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedPointwise.observedAgreement_changePositions line 61

Source documentation

This applies to every hidden draw, with all its other data fixed.

theorem observedAgreement_changePositions (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)
    (draw : AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector rs))
    (slot : Fin k → PartnerProjection.Slot)
    (hslot : ∀ j, j ∈ draw.singletons → draw.positions j = slot j) :
    VisiblePolicies.observedAgreement S labeling good draw =
      VisiblePolicies.observedAgreement S labeling good { draw with positions := slot } := by
…

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

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedPointwise.seedAgreement_pointwise line 81

Source documentation

Seed and actual-draw agreement before averaging any sampled map.

theorem seedAgreement_pointwise (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)
    (occ : Fin k → Fin S.occurrences) (A : Alphabet s →ₗ[F2] Vector rs)
    (choices : Fin k → PaddedLaw.ProjectionChoice)
    (slot : Fin k → PartnerProjection.Slot)
    (hslot : ∀ j, j ∈ PaddedLaw.choiceMask choices →
      PaddedLaw.choiceSlots choices j = slot j)
    (Y : RawPartnerTarget.RawPoint (PaddedLaw.choiceMask choices) →ₗ[F2]
      (Alphabet s × Vector d)) :
    VisiblePolicies.observedAgreement S labeling good
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.ProjectionChoice, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceMask, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceSlots, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedPointwise.seedAgreement_repack_at line 101

theorem OAI.UniqueGamesTheorem.Decoder.ActualSeedPointwise.seedAgreement_repack line 130

Source documentation

Exact uniform-law identification with Bernoulli-mask and iid-slot sampling. All dependent mask transport is confined to this theorem.

theorem seedAgreement_repack (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)
    (occ : Fin k → Fin S.occurrences) (A : Alphabet s →ₗ[F2] Vector rs)
    (mask : Fin k → Bool) (slots : Fin k → Fin 3) :
    (FiniteDistribution.uniform
      (RawPartnerTarget.RawPoint
        (PaddedLaw.choiceMask (AdviceLaw.choicesOfMaskSlots mask slots)) →ₗ[F2]
          (Alphabet s × Vector d))).expectation (fun Y =>
            VisiblePolicies.observedAgreement S labeling good
              (AdviceLaw.seedToActualDraw occ A
…

Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.LeftInput, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.ResponseWitness, OAI.UniqueGamesTheorem.Decoder.PaddedLaw.choiceMask, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.choicesOfMaskSlots, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seedToActualDraw