OAI/Computability/MaxCut/Encoding/ActualAdviceSampling.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The stochastic clean upper bound applies to the literal agreement of the two actual local decoders. The equality below retains every sampled mask, all occurrence/position draws, and both independently uniform target maps.

  1. theorem OAI.MaxCutGames.Decoder.ActualAdviceSampling.product_probability line 25
  2. theorem OAI.MaxCutGames.Decoder.ActualAdviceSampling.fixedMapSuccess_eq_product line 34
  3. theorem OAI.MaxCutGames.Decoder.ActualAdviceSampling.fixedMapSuccess_eq_observed line 55
  4. def OAI.MaxCutGames.Decoder.ActualAdviceSampling.sampledAgreement line 79

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness

  5. theorem OAI.MaxCutGames.Decoder.ActualAdviceSampling.actualSuccess_eq_sampledAgreement line 95
  6. theorem OAI.MaxCutGames.Decoder.ActualAdviceSampling.sampledAgreement_average_bound line 113

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Clean.IncidenceGap.parityValue, OAI.MaxCutGames.Decoder.ActualAdviceSampling.sampledAgreement, OAI.MaxCutGames.Clean.IncidenceGap.slotLaw

  7. theorem OAI.MaxCutGames.Decoder.ActualSeedPointwise.rawProjection_congr_slots line 153
  8. theorem OAI.MaxCutGames.Decoder.ActualSeedPointwise.supported_congr_slots line 173
  9. theorem OAI.MaxCutGames.Decoder.ActualSeedPointwise.observedAgreement_changePositions line 188

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.AdviceExperiment.Draw, OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement

  10. theorem OAI.MaxCutGames.Decoder.ActualSeedPointwise.seedAgreement_pointwise line 208

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.PaddedLaw.ProjectionChoice, OAI.MaxCutGames.Decoder.PaddedLaw.choiceMask, OAI.MaxCutGames.Decoder.PaddedLaw.choiceSlots, OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement

  11. theorem OAI.MaxCutGames.Decoder.ActualSeedPointwise.seedAgreement_repack_at_inline_ActualSeedPointwise line 228
  12. theorem OAI.MaxCutGames.Decoder.ActualSeedPointwise.seedAgreement_repack line 257

    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.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.PaddedLaw.choiceMask, OAI.MaxCutGames.Decoder.AdviceLaw.choicesOfMaskSlots, OAI.MaxCutGames.Decoder.VisiblePolicies.observedAgreement, OAI.MaxCutGames.Decoder.AdviceLaw.seedToActualDraw

  13. theorem OAI.MaxCutGames.Decoder.ActualSeedSampling.uniform_occurrence_slots line 310
  14. def OAI.MaxCutGames.Decoder.ActualSeedSampling.drawAgreement line 324

    Source documentation

    A named pointwise observable makes the finite expectation permutations explicit without changing the actual sampled draw.

    def drawAgreement (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) (mask : Fin k → Bool)
    (occ : Fin k → Fin S.occurrences) (slots : Fin k → Fin 3)
    (TM :
      (RawPartnerTarget.RawPoint (Clean.NativeExperiment.maskSet mask) →ₗ[F2] Vector d) ×
      (RawPartnerTarget.RawPoint (Clean.NativeExperiment.maskSet mask) →ₗ[F2] Alphabet s)) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Clean.NativeExperiment.maskSet

  15. theorem OAI.MaxCutGames.Decoder.ActualSeedSampling.sampledAgreement_eq_separated line 337
  16. theorem OAI.MaxCutGames.Decoder.ActualSeedSampling.fullSeedLaw_eq_sampledAgreement line 375

    Source documentation

    Exact sampler join: the complete hidden seed used by conditioning has the same success as the genuine local-policy experiment used by the upper bound, with no extra hidden-data conditioning on either side.

    theorem fullSeedLaw_eq_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)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) :
    (AdviceLaw.fullSeedLaw (V := Alphabet s × Vector d)
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.AdviceLaw.fullSeedLaw

  17. theorem OAI.MaxCutGames.Decoder.ActualSeedSampling.fullSeedLaw_upper line 413
  18. theorem OAI.MaxCutGames.Decoder.ActualMatrixContradiction.univ_fintype_eq_inline_ActualMatrixContradiction line 450
  19. def OAI.MaxCutGames.Decoder.ActualMatrixContradiction.expectationOf_inline_ActualMatrixContradiction line 454
  20. theorem OAI.MaxCutGames.Decoder.ActualMatrixContradiction.card_to_natCard_inline_ActualMatrixContradiction line 458
  21. theorem OAI.MaxCutGames.Decoder.ActualMatrixContradiction.law_expectation_eq line 462
  22. theorem OAI.MaxCutGames.Decoder.ActualMatrixContradiction.contradiction line 471