GameEncodingSize.lean`

4 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.MaxCutGames.Reduction.GameEncodingSize.tableBits_length_le line 18
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.MaxCutGames.Reduction.GameEncodingSize.constraintBits_length_le line 29
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.MaxCutGames.Reduction.GameEncodingSize.constraintsBits_length_le line 40
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.MaxCutGames.Reduction.GameEncodingSize.gameBits_length_le line 53
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
…
```