IncidenceGap.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

The weighted equation-versus-variable game for a three-variable parity system. An occurrence is sampled with its given weight and one of its three positions is sampled uniformly. Alice sees the occurrence and Bob sees only the variable name. Distinct positions make the predicate a partial projection. The loss of a factor of three in the gap is proved directly by counting the three positions. No PCP hardness statement or parallel-repetition bound is a premise here.

def OAI.MaxCutGames.Clean.IncidenceGap.slotLaw line 31
Source documentation
Independent occurrence and uniform retained-position sampling.
```
def slotLaw (ω : FiniteDistribution O) : FiniteDistribution (O × Fin 3) :=
…
```
theorem OAI.MaxCutGames.Clean.IncidenceGap.slotLaw_weight line 34
def OAI.MaxCutGames.Clean.IncidenceGap.incidenceLaw line 39
Source documentation
The retained position is internal; the actual right question is its name.
```
def incidenceLaw (g : Incidence O N) (ω : FiniteDistribution O) :
    FiniteDistribution (O × N) :=
…
```
def OAI.MaxCutGames.Clean.IncidenceGap.game line 43
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_accepts_iff line 48
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_isProjection line 54
def OAI.MaxCutGames.Clean.IncidenceGap.paritySuccess line 65
Source documentation
The actual weighted satisfaction probability of the parity equations.
```
def paritySuccess (g : Incidence O N) (ω : FiniteDistribution O) (b : N → Bool) : ℝ :=
…
```
def OAI.MaxCutGames.Clean.IncidenceGap.parityValue line 69
Source documentation
The attained optimum over all assignments to the names.
```
def parityValue (g : Incidence O N) (ω : FiniteDistribution O) : ℝ := by
…
```
theorem OAI.MaxCutGames.Clean.IncidenceGap.paritySuccess_le_parityValue line 73
theorem OAI.MaxCutGames.Clean.IncidenceGap.local_count_bound line 80
Source documentation
If Bob violates the equation, at most two of Alice's three coordinates can agree with him while satisfying the required parity.
```
theorem local_count_bound (a b : Triple) (rhs : Bool) :
    (∑ i : Fin 3, if xorTriple a = rhs ∧ a i = b i then (1 : ℝ) else 0) ≤
      2 + if xorTriple b = rhs then (1 : ℝ) else 0 := by
…
```
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_success_eq_slot_average line 93
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_success_honest_eq_paritySuccess line 115
Source documentation
The assignment itself supplies both local answer functions. Its incidence success equals its parity satisfaction probability exactly.
```
theorem game_success_honest_eq_paritySuccess
    (g : Incidence O N) (ω : FiniteDistribution O)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (b : N → Bool) :
    (game g ω).success ((fun o i => b (g.name o i)), b) = paritySuccess g ω b := by
…
```
Mentions: OAI.MaxCutGames.Clean.IncidenceGap.game, OAI.MaxCutGames.Clean.IncidenceGap.paritySuccess
theorem OAI.MaxCutGames.Clean.IncidenceGap.parityValue_le_game_value line 128
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_success_le_two_add_parity_third line 139
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_value_le_one_sub_third line 160
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_value_le_one_sub_gap_third line 170
theorem OAI.MaxCutGames.Clean.IncidenceGap.game_value_le_fourteen_fifteenths line 180
def OAI.MaxCutGames.Clean.IncidenceGap.satisfyingTriple line 189
Source documentation
Two bits encode the four satisfying answers for an occurrence.
```
def satisfyingTriple (rhs : Bool) (a : Bool × Bool) : Triple :=
…
```
theorem OAI.MaxCutGames.Clean.IncidenceGap.satisfyingTriple_valid line 192
theorem OAI.MaxCutGames.Clean.IncidenceGap.satisfyingTriple_of_valid line 197
def OAI.MaxCutGames.Clean.IncidenceGap.fourAnswerGame line 208
theorem OAI.MaxCutGames.Clean.IncidenceGap.four_answer_card line 213
theorem OAI.MaxCutGames.Clean.IncidenceGap.fourAnswerGame_isProjection line 215
theorem OAI.MaxCutGames.Clean.IncidenceGap.fourAnswerGame_accepts_encode line 222
theorem OAI.MaxCutGames.Clean.IncidenceGap.fourAnswerGame_value_eq line 236
Source documentation
Rejecting invalid ambient triples does not change the optimum. Both directions transport local answer functions; no extra question is revealed.
```
theorem fourAnswerGame_value_eq (g : Incidence O N) (ω : FiniteDistribution O) :
    (fourAnswerGame g ω).value = (game g ω).value := by
…
```
Mentions: OAI.MaxCutGames.Clean.IncidenceGap.fourAnswerGame, OAI.MaxCutGames.Clean.IncidenceGap.game
theorem OAI.MaxCutGames.Clean.IncidenceGap.fourAnswerGame_value_le_one_sub_third line 254
theorem OAI.MaxCutGames.Clean.IncidenceGap.fourAnswerGame_value_le_fourteen_fifteenths line 261

theorem OAI.MaxCutGames.Clean.Bound.repeated_incidence_value_le line 287

Source documentation

The precise rate is obtained from the proved ordinary projection-game bound, with no question-set or alphabet parameter in its base.

theorem repeated_incidence_value_le
    (g : IncidenceExtraction.Incidence O N) (ω : FiniteDistribution O)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (hopt : IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5) (n : ℕ) :
    ((incidenceGame g ((IncidenceGap.slotLaw ω).pushforward (incidence g.name))).repetition n).value ≤
      (1 - (1 : ℝ) / 3600) ^ n := by
…

Mentions: OAI.MaxCutGames.Clean.IncidenceGap.parityValue, OAI.MaxCutGames.Clean.IncidenceGap.slotLaw

theorem OAI.MaxCutGames.Clean.Bound.clean_success_le line 300

Source documentation

Section 5's clean agreement estimate, with every sampling/locality/rate step discharged for the explicit advice experiment.

theorem clean_success_le (k : ℕ) (g : IncidenceExtraction.Incidence O N)
    (ω : FiniteDistribution O) (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (hopt : IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5) :
    success k (IncidenceGap.slotLaw ω) g extraLaw β hβ₀ hβ₁ strategy ≤
      (1 - (β / (Fintype.card (Coefficient R) : ℝ)) / 3600) ^ k := by
…

Mentions: OAI.MaxCutGames.Clean.IncidenceGap.parityValue, OAI.MaxCutGames.Clean.IncidenceGap.slotLaw

theorem OAI.MaxCutGames.Clean.Bound.clean_success_le_dimension line 315

Source documentation

A uniform bound on visible advice dimension makes the estimate independent of the sampled map A. Apply with Coefficient R ≃ W × range A.

theorem clean_success_le_dimension (k : ℕ) (g : IncidenceExtraction.Incidence O N)
    (ω : FiniteDistribution O) (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N)
    (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 (Coefficient R) ≤ 2 ^ (dimW + rs)) :
    success k (IncidenceGap.slotLaw ω) g extraLaw β hβ₀ hβ₁ strategy ≤
      (1 - (β / (2 : ℝ) ^ (dimW + rs)) / 3600) ^ k := by
…

Mentions: OAI.MaxCutGames.Clean.IncidenceGap.parityValue, OAI.MaxCutGames.Clean.IncidenceGap.slotLaw

theorem OAI.MaxCutGames.Clean.Bound.native_clean_success_le_dimension line 332
theorem OAI.MaxCutGames.Clean.ActualAdviceBound.deterministic_success_le_dimension line 364

theorem OAI.MaxCutGames.Clean.ActualAdviceBound.stochastic_success_le_dimension line 382

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.MaxCutGames.Clean.ActualAdviceStochasticBridge.Policies, OAI.MaxCutGames.Clean.IncidenceGap.parityValue, OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.success, OAI.MaxCutGames.Clean.IncidenceGap.slotLaw

theorem OAI.MaxCutGames.Clean.ActualAdviceBound.stochastic_success_le_dimension_finite line 398