IncidenceGap.lean`

27 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.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw line 39
Source documentation
Independent occurrence and uniform retained-position sampling.
```
def slotLaw (ω : FiniteDistribution O) : FiniteDistribution (O × Fin 3) :=
…
```
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw_weight line 42
def OAI.UniqueGamesTheorem.Clean.IncidenceGap.incidenceLaw line 47
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.UniqueGamesTheorem.Clean.IncidenceGap.game line 51
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.game_accepts_iff line 56
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.game_isProjection line 62
def OAI.UniqueGamesTheorem.Clean.IncidenceGap.paritySuccess line 73
Source documentation
The actual weighted satisfaction probability of the parity equations.
```
def paritySuccess (g : Incidence O N) (ω : FiniteDistribution O) (b : N → Bool) : ℝ :=
…
```
def OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue line 77
Source documentation
The attained optimum over all assignments to the names.
```
def parityValue (g : Incidence O N) (ω : FiniteDistribution O) : ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.paritySuccess_le_parityValue line 81
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.local_count_bound line 88
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.UniqueGamesTheorem.Clean.IncidenceGap.game_success_eq_slot_average line 101
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.game_success_honest_eq_paritySuccess line 123
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.UniqueGamesTheorem.Clean.IncidenceGap.game, OAI.UniqueGamesTheorem.Clean.IncidenceGap.paritySuccess
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue_le_game_value line 136
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.game_success_le_two_add_parity_third line 147
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.game_value_le_one_sub_third line 168
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.game_value_le_one_sub_gap_third line 178
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.game_value_le_fourteen_fifteenths line 188
def OAI.UniqueGamesTheorem.Clean.IncidenceGap.satisfyingTriple line 197
Source documentation
Two bits encode the four satisfying answers for an occurrence.
```
def satisfyingTriple (rhs : Bool) (a : Bool × Bool) : Triple :=
…
```
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.satisfyingTriple_valid line 200
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.satisfyingTriple_of_valid line 205
def OAI.UniqueGamesTheorem.Clean.IncidenceGap.fourAnswerGame line 216
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.four_answer_card line 221
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.fourAnswerGame_isProjection line 223
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.fourAnswerGame_accepts_encode line 230
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.fourAnswerGame_value_eq line 244
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.UniqueGamesTheorem.Clean.IncidenceGap.fourAnswerGame, OAI.UniqueGamesTheorem.Clean.IncidenceGap.game
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.fourAnswerGame_value_le_one_sub_third line 262
theorem OAI.UniqueGamesTheorem.Clean.IncidenceGap.fourAnswerGame_value_le_fourteen_fifteenths line 269