PoweringTableLayout.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Vertex-major serialization of the actual powering table

Each vertex contributes a fixed number of consecutive stored dart rows. The identities below group the actual vector, including every predicate entry, and then apply the shared word codec. They do not assume an output layout or assert a machine running time. Unary bit lengths can vary with the stored indices.

def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockSize line 21
Source documentation
One adjacent orientation pair for each recorded port word.
```
def blockSize (d n : Nat) : Nat := 2 * d ^ (n + 1)
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.dartCount_eq_vertex_blocks line 23
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockIndex line 30
Source documentation
The index of a stored row within the consecutive block of vertex v.
```
def blockIndex {vertices : Nat} (d n : Nat) (v : Fin vertices)
    (j : Fin (blockSize d n)) : Fin (dartCount vertices d n) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockSize
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockIndex_val line 35
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockIndex_eq_encodeDart line 42
Source documentation
The consecutive block is the actual vertex-major recorded-walk order.
```
theorem blockIndex_eq_encodeDart {vertices : Nat} (d n : Nat) (v : Fin vertices)
    (p : Fin (n + 1) → Fin d) (direction : Bool) :
    blockIndex d n v (dartBlockEquiv d n (p, direction)) =
      encodeDart vertices d n (direction, (v, p)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockIndex
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRows line 50
Source documentation
Exactly the stored rows at positions B*v, ..., B*v+B-1.
```
def vertexRows {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (v : Fin vertices) :
    List (GenericGraphTables.DartRow (labelCount d n) vertices (dartCount vertices d n)) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.DartRow
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowWords line 56
Source documentation
All fields of these stored rows, in their actual codec order.
```
def vertexRowWords {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (v : Fin vertices) : List Nat :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table
def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowBits line 61
Source documentation
Actual unary serialization of the complete vertex block.
```
def vertexRowBits {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (v : Fin vertices) : List Bool :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRows_length line 65
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vector_toList_ofFn line 71

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vector_blocks line 79

Source documentation

Regroup a stored vector without changing, omitting, or permuting a row.

private theorem vector_blocks {α : Type*} {m vertices width : Nat}
    (sameCount : m = vertices * width) (rows : Vector α m) :
    rows.toList = (List.finRange vertices).flatMap (fun v =>
      List.ofFn (fun j : Fin width =>
        rows[Fin.cast sameCount.symm (finProdFinEquiv (v, j))])) := by
…

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.rowList_eq_vertexRows line 96
Source documentation
Every actual stored row occurs once in its vertex's consecutive block.
```
theorem rowList_eq_vertexRows {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) :
    GenericGraphTables.rowList (table input n) =
      (List.finRange vertices).flatMap (vertexRows input n) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowList, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRows
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.outputWords_vertexRows line 103
Source documentation
The full word stream, including its two header fields, in vertex order.
```
theorem outputWords_vertexRows {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) :
    GenericGraphTables.tableWords (table input n) =
      [vertices, dartCount vertices d n] ++
        (List.finRange vertices).flatMap (vertexRowWords input n) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowWords
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.encodeWords_flatMap line 114
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.outputBits_vertexRows line 122
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowWords_length line 131
Source documentation
Each stored row has its tail, reversal, and every ordered predicate bit.
```
theorem vertexRowWords_length {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (v : Fin vertices) :
    (vertexRowWords input n v).length =
      (labelCount d n * labelCount d n + 2) * blockSize d n := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowWords, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockSize
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_ge line 139
Source documentation
Every natural field contributes at least its unary delimiter.
```
theorem vertexRowBits_length_ge {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (v : Fin vertices) :
    (labelCount d n * labelCount d n + 2) * blockSize d n ≤
      (vertexRowBits input n v).length := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockSize, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowBits
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_le line 148
Source documentation
Actual unary row blocks have a uniform bound from the two index bounds.
```
theorem vertexRowBits_length_le {vertices d : Nat} (input : PortTables.Table vertices d)
    (n : Nat) (v : Fin vertices) :
    (vertexRowBits input n v).length ≤
      blockSize d n *
        (vertices + dartCount vertices d n + 2 * (labelCount d n * labelCount d n)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.vertexRowBits, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockSize
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.outputHeader_length line 158
Source documentation
The actual unary header contains the two declared counts.
```
theorem outputHeader_length (vertices d n : Nat) :
    (encodeWords [vertices, dartCount vertices d n]).length =
      vertices + dartCount vertices d n + 2 := by
…
```