GameEncodingSizeLemmas.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Bit-length bounds for the concrete unique-game serialization. Every stored constraint occurrence and every entry of its forward permutation table is encoded. These are output-size bounds, not machine running-time bounds.

theorem OAI.UniqueGamesTheorem.Reduction.GameEncodingSize.tableBits_length_le line 20
Source documentation
The full table has q labels, each with unary encoding length at most q+1. The conservative bound remains valid when the alphabet is empty.
```
theorem tableBits_length_le {q : Nat} (table : PermutationTable q) :
    (encodeWords (tableWords table)).length ≤ q * (q + 1) := by
…
```
theorem OAI.UniqueGamesTheorem.Reduction.GameEncodingSize.constraintBits_length_le line 31
Source documentation
Both endpoint words use at most n bits, and the entire forward table is retained. A constraint itself supplies the endpoint bounds, even for small n.
```
theorem constraintBits_length_le {n q : Nat} (constraint : Constraint n q) :
    (encodeWords (constraintWords constraint)).length ≤ 2 * n + q * (q + 1) := by
…
```
theorem OAI.UniqueGamesTheorem.Reduction.GameEncodingSize.constraintsBits_length_le line 42
Source documentation
Each occurrence contributes its own complete encoding; no deduplication or implicit edge weights enter the bound. The empty list is also covered.
```
theorem constraintsBits_length_le {n q : Nat} (constraints : List (Constraint n q)) :
    (encodeWords (constraints.flatMap constraintWords)).length ≤
      constraints.length * (2 * n + q * (q + 1)) := by
…
```
theorem OAI.UniqueGamesTheorem.Reduction.GameEncodingSize.gameBits_length_le line 55
Source documentation
Exact header accounting plus a bound on every serialized occurrence. No lower bound on the alphabet or vertex count is assumed.
```
theorem gameBits_length_le {q : Nat} (g : Instance q) :
    (gameBits g).length ≤
      g.vertices + q + g.constraints.length + 3 +
        g.constraints.length * (2 * g.vertices + q * (q + 1)) := by
…
```
structure OAI.UniqueGamesTheorem.Reduction.Incidence.Triple line 72
def OAI.UniqueGamesTheorem.Reduction.Incidence.parity line 78
def OAI.UniqueGamesTheorem.Reduction.Incidence.matchingSlots line 80
def OAI.UniqueGamesTheorem.Reduction.Incidence.acceptedSlots line 86
Source documentation
Invalid Alice answers lose in every slot.
```
def acceptedSlots (a b : Triple) (rhs : Bool) : Nat :=
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Triple
def OAI.UniqueGamesTheorem.Reduction.Incidence.failedEquation line 89
def OAI.UniqueGamesTheorem.Reduction.Incidence.bestResponse line 93
Source documentation
Copy a satisfying Bob triple; otherwise flip its first bit.
```
def bestResponse (b : Triple) (rhs : Bool) : Triple :=
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Triple
theorem OAI.UniqueGamesTheorem.Reduction.Incidence.local_count_bound line 96
theorem OAI.UniqueGamesTheorem.Reduction.Incidence.best_response_exact line 103
structure OAI.UniqueGamesTheorem.Reduction.Incidence.Equation line 110
inductive OAI.UniqueGamesTheorem.Reduction.Incidence.Slot line 118
def OAI.UniqueGamesTheorem.Reduction.Incidence.nameAt line 124
def OAI.UniqueGamesTheorem.Reduction.Incidence.bitAt line 129
def OAI.UniqueGamesTheorem.Reduction.Incidence.questionPredicate line 135
Source documentation
A predicate of the actual questions and answers, with no hidden slot input.
```
def questionPredicate (e : Equation Variable) (name : Variable)
    (alice : Triple) (bob : Bool) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Equation, OAI.UniqueGamesTheorem.Reduction.Incidence.Triple
theorem OAI.UniqueGamesTheorem.Reduction.Incidence.question_predicate_at_slot line 143
Source documentation
Cloning supplies exactly the distinctness needed to recover a slot from its name.
```
theorem question_predicate_at_slot (e : Equation Variable)
    (distinct₁₂ : e.first ≠ e.second) (distinct₁₃ : e.first ≠ e.third)
    (distinct₂₃ : e.second ≠ e.third) (alice : Triple) (bob : Bool) (slot : Slot) :
    questionPredicate e (nameAt e slot) alice bob ↔
      parity alice = e.rhs ∧ bitAt alice slot = bob := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Equation, OAI.UniqueGamesTheorem.Reduction.Incidence.Triple, OAI.UniqueGamesTheorem.Reduction.Incidence.Slot, OAI.UniqueGamesTheorem.Reduction.Incidence.questionPredicate, OAI.UniqueGamesTheorem.Reduction.Incidence.nameAt, OAI.UniqueGamesTheorem.Reduction.Incidence.parity, OAI.UniqueGamesTheorem.Reduction.Incidence.bitAt
def OAI.UniqueGamesTheorem.Reduction.Incidence.bobTriple line 153
Source documentation
Bob receives only a variable name: the strategy has no occurrence input.
```
def bobTriple (g : Variable → Bool) (e : Equation Variable) : Triple :=
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Equation, OAI.UniqueGamesTheorem.Reduction.Incidence.Triple
def OAI.UniqueGamesTheorem.Reduction.Incidence.acceptedCount line 157
Source documentation
An occurrence index supplies Alice's full question and its equation.
```
def acceptedCount (equations : Index → Equation Variable)
    (g : Variable → Bool) (alice : Index → Triple) : List Index → Nat
  | [] => 0
  | i :: rest =>
    acceptedSlots (alice i) (bobTriple g (equations i)) (equations i).rhs +
      acceptedCount equations g alice rest
```
Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Equation, OAI.UniqueGamesTheorem.Reduction.Incidence.Triple, OAI.UniqueGamesTheorem.Reduction.Incidence.acceptedSlots, OAI.UniqueGamesTheorem.Reduction.Incidence.bobTriple
def OAI.UniqueGamesTheorem.Reduction.Incidence.failureCount line 164
theorem OAI.UniqueGamesTheorem.Reduction.Incidence.total_count_bound line 171
def OAI.UniqueGamesTheorem.Reduction.Incidence.optimalAlice line 182
theorem OAI.UniqueGamesTheorem.Reduction.Incidence.optimal_alice_exact line 186

theorem OAI.UniqueGamesTheorem.Reduction.Incidence.fixed_bob_optimum line 198

Source documentation

Exact finite-count form of max_Alice Pr[accept | Bob = g] = 1 - u(g)/3.

theorem fixed_bob_optimum (equations : Index → Equation Variable)
    (g : Variable → Bool) (occurrences : List Index) :
    ∃ alice : Index → Triple,
      acceptedCount equations g alice occurrences + failureCount equations g occurrences =
        3 * occurrences.length ∧
      ∀ other : Index → Triple,
        acceptedCount equations g other occurrences ≤
          acceptedCount equations g alice occurrences := by
…

Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Equation, OAI.UniqueGamesTheorem.Reduction.Incidence.Triple, OAI.UniqueGamesTheorem.Reduction.Incidence.acceptedCount, OAI.UniqueGamesTheorem.Reduction.Incidence.failureCount

theorem OAI.UniqueGamesTheorem.Reduction.Incidence.soundness_191_over_192 line 212
theorem OAI.UniqueGamesTheorem.Reduction.Incidence.game_soundness_191_over_192 line 220
Source documentation
The same bound holds for every deterministic pair when every Bob assignment has the gap.
```
theorem game_soundness_191_over_192 (equations : Index → Equation Variable)
    (occurrences : List Index)
    (source_gap : ∀ g : Variable → Bool,
      occurrences.length ≤ 64 * failureCount equations g occurrences) :
    ∀ (g : Variable → Bool) (alice : Index → Triple),
      64 * acceptedCount equations g alice occurrences ≤ 191 * occurrences.length := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.Incidence.Equation, OAI.UniqueGamesTheorem.Reduction.Incidence.failureCount, OAI.UniqueGamesTheorem.Reduction.Incidence.Triple, OAI.UniqueGamesTheorem.Reduction.Incidence.acceptedCount