PortTableLookup.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exact word offsets in executable port tables

These are optional list-lookup equalities for the unary-word stream consumed by the lookup machine. They expose the stored tail, reverse index, and predicate bit at their actual positions in the existing graph-table serialization.

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.flatMap_word line 17
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.vertices_word line 50
Source documentation
The first header word is the number of vertices.
```
theorem vertices_word (table : PortTables.Table n d) :
    (PortTables.tableWords table)[0]? = some n := rfl
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.darts_word line 54
Source documentation
The second header word is the number of directed port occurrences.
```
theorem darts_word (table : PortTables.Table n d) :
    (PortTables.tableWords table)[1]? = some (n * d) := rfl
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.row_word line 57
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.tail_word line 74
Source documentation
The first word of row i records the tail vertex.
```
theorem tail_word (table : PortTables.Table n d) (i : Fin (n * d)) :
    (PortTables.tableWords table)[2 + 4098 * i.val]? =
      some (((PortTables.rowIndex n d).symm i).1.val) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rowIndex
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.reverse_word line 83
Source documentation
The second word of row i is the actual stored reverse index.
```
theorem reverse_word (table : PortTables.Table n d) (i : Fin (n * d)) :
    (PortTables.tableWords table)[3 + 4098 * i.val]? =
      some (table.reverseIndex[i].val) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.relation_word line 93
Source documentation
Relation position j is a stored Boolean, encoded as its zero-or-one word.
```
theorem relation_word (table : PortTables.Table n d) (i : Fin (n * d))
    (j : Fin 4096) :
    (PortTables.tableWords table)[4 + 4098 * i.val + j.val]? =
      some (GraphTables.bitWord table.relations[i][j]) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.bitWord
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.accepts_word line 106
Source documentation
A lookup indexed by the two labels returns exactly the semantic predicate.
```
theorem accepts_word (table : PortTables.Table n d) (e : Fin n × Fin d)
    (a b : PortTables.Label) :
    (PortTables.tableWords table)[4 + 4098 * (PortTables.rowIndex n d e).val +
        (GraphTables.relationIndex (a, b)).val]? =
      some (GraphTables.bitWord (PortTables.accepts table e a b)) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rowIndex, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationIndex, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.bitWord, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.rotation_head_word line 114
Source documentation
After the reverse-index lookup, the target row's tail is the rotor endpoint.
```
theorem rotation_head_word (table : PortTables.Table n d) (e : Fin n × Fin d) :
    (PortTables.tableWords table)[2 + 4098 * (table.reverseIndex[PortTables.rowIndex n d e]).val]? =
      some ((PortTables.rotation table e).1.val) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rowIndex, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rotation
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTableLookup.rotor_lookups line 120
Source documentation
Both selections required by a concrete two-lookup rotor implementation.
```
theorem rotor_lookups (table : PortTables.Table n d) (e : Fin n × Fin d) :
    (PortTables.tableWords table)[3 + 4098 * (PortTables.rowIndex n d e).val]? =
      some (table.reverseIndex[PortTables.rowIndex n d e].val) ∧
    (PortTables.tableWords table)[2 + 4098 * (table.reverseIndex[PortTables.rowIndex n d e]).val]? =
      some ((PortTables.rotation table e).1.val) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rowIndex, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rotation