StochasticBound.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Local randomized advice responses are bounded using complete independently sampled response tables. The verifier questions are the actual weighted pushforward of the occurrence/position draw, with the complete private row input retained on each side. No response sees the opposite private question.

The outer mask and coefficient tuple may be fixed before selecting either response kernel. Revealing these data only strengthens this upper bound; they contain no clean question or agreement event. The quantitative game-repetition rate is a separate input to the final averaging lemma.

def OAI.UniqueGamesTheorem.Clean.StochasticBound.actualGame line 35

Source documentation

The common weighted-game interface for the actual fixed-advice experiment.

def actualGame (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R)) :
    Game (ZeroInformation.FirstInput P R O) (ZeroInformation.SecondInput P R O N)
      (ActualProjection.FirstAnswer P) (ActualProjection.SecondAnswer P) :=
…

abbrev OAI.UniqueGamesTheorem.Clean.StochasticBound.fixedAdviceGame line 44

theorem OAI.UniqueGamesTheorem.Clean.StochasticBound.success_eq_fixedAdviceSuccess line 49

Source documentation

The two deterministic strategy representations have exactly the same winning probability under the explicitly constructed question law.

theorem success_eq_fixedAdviceSuccess
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (strategy : Strategy (ZeroInformation.FirstInput P R O)
      (ZeroInformation.SecondInput P R O N)
      (ActualProjection.FirstAnswer P) (ActualProjection.SecondAnswer P)) :
    (actualGame μ J g gamma).success strategy =
      UpperBound.fixedAdviceSuccess μ J g gamma ⟨strategy.1, strategy.2⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.StochasticBound.actualGame, OAI.UniqueGamesTheorem.Clean.UpperBound.fixedAdviceSuccess

theorem OAI.UniqueGamesTheorem.Clean.StochasticBound.exists_deterministic_ge_stochastic line 66

Source documentation

Each stochastic local response has a deterministic complete response table with at least its success probability. The table is chosen before the questions.

theorem exists_deterministic_ge_stochastic
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (responses₁ : ZeroInformation.FirstInput P R O →
      FiniteDistribution (ActualProjection.FirstAnswer P))
    (responses₂ : ZeroInformation.SecondInput P R O N →
      FiniteDistribution (ActualProjection.SecondAnswer P)) :
    ∃ strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N),
…

theorem OAI.UniqueGamesTheorem.Clean.StochasticBound.fixed_advice_stochastic_le_repeated_value line 85
abbrev OAI.UniqueGamesTheorem.Clean.StochasticBound.Responses line 101
Source documentation
A pair of response kernels, each indexed only by its own complete input.
```
abbrev Responses (P R O N : Type) [Fintype P] [DecidableEq P] :=
…
```
def OAI.UniqueGamesTheorem.Clean.StochasticBound.nativeStochasticSuccess line 107
Source documentation
The native experiment samples a mask, then the actual coefficient tuple. The kernels may depend on these public choices but not on an opposite input.
```
def nativeStochasticSuccess (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (responses : (mask : Fin k → Bool) →
      RawCoefficients (NativeExperiment.maskSet mask) (ZeroInformation.Bits R) →
      Responses (Fin k) R O N) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.NativeExperiment.maskSet, OAI.UniqueGamesTheorem.Clean.StochasticBound.Responses
theorem OAI.UniqueGamesTheorem.Clean.StochasticBound.expectation_mono line 119

theorem OAI.UniqueGamesTheorem.Clean.StochasticBound.native_stochastic_le_deterministic line 128

Source documentation

The deterministic witness family is indexed by the pre-question public data only. No single global deterministic strategy is claimed here.

theorem native_stochastic_le_deterministic
    (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (responses : (mask : Fin k → Bool) →
      RawCoefficients (NativeExperiment.maskSet mask) (ZeroInformation.Bits R) →
      Responses (Fin k) R O N) :
    ∃ strategy : NativeExperiment.MaskStrategy k R O N,
      nativeStochasticSuccess k μ g β hβ₀ hβ₁ responses ≤
        NativeExperiment.success k μ g β hβ₀ hβ₁ strategy := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.NativeExperiment.maskSet, OAI.UniqueGamesTheorem.Clean.StochasticBound.Responses, OAI.UniqueGamesTheorem.Clean.NativeExperiment.MaskStrategy, OAI.UniqueGamesTheorem.Clean.StochasticBound.nativeStochasticSuccess, OAI.UniqueGamesTheorem.Clean.NativeExperiment.success

theorem OAI.UniqueGamesTheorem.Clean.StochasticBound.native_stochastic_le_mask_moment line 153

Source documentation

Stochastic kernels satisfy the same exact clean-mask moment as deterministic ones. The only supplied rate is for the actual ordinary repeated incidence game.

theorem native_stochastic_le_mask_moment
    (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (responses : (mask : Fin k → Bool) →
      RawCoefficients (NativeExperiment.maskSet mask) (ZeroInformation.Bits R) →
      Responses (Fin k) R O N)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j) (ρ : ℝ)
    (rate : ∀ n, ((incidenceGame g (μ.pushforward (incidence g.name))).repetition n).value ≤ ρ ^ n) :
    nativeStochasticSuccess k μ g β hβ₀ hβ₁ responses ≤
      (1 - cleanProbability β (ZeroInformation.Bits R) * (1 - ρ)) ^ k := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.NativeExperiment.maskSet, OAI.UniqueGamesTheorem.Clean.StochasticBound.Responses, OAI.UniqueGamesTheorem.Clean.StochasticBound.nativeStochasticSuccess, OAI.UniqueGamesTheorem.Clean.cleanProbability