PreprocessingRegularWords.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Complete serialization of the actual regularized table

Each global vertex emits its internal ports in increasing order, then its inherited port. Original darts are the first global vertices. Dummy vertices follow in increasing owner and local-dummy order. These are identities for the actual stored rows and existing codec, with arbitrary actual cloud tables.

def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow line 24
Source documentation
Read one row of the actual output, in the chosen global coordinates.
```
def actualRow (x : Vertex t padding) (p : Fin q ⊕ Unit) :
    GraphTables.DartRow (vertexCount t padding) (vertexCount t padding * (q + 1)) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.DartRow
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.vertexRows line 30
Source documentation
A vertex emits every internal port, followed by its inherited port.
```
def vertexRows (x : Vertex t padding) :
    List (GraphTables.DartRow (vertexCount t padding) (vertexCount t padding * (q + 1))) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.DartRow
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.originalVertexRows line 35
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.dummyVertexRows line 36
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.vertexBits line 39
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.originalVertexBits line 42
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits line 43
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow_internal line 47
Source documentation
The internal row is exactly the checked lookup/select row.
```
theorem actualRow_internal (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
    actualRow t padding tables x.val (.inl p) =
      PreprocessingInternalRows.row t padding tables v x p := rfl
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow_eq line 51
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow_tail line 61
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.inherited_original_reverse line 65
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_reverse line 77
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.relation_ext line 90
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.inherited_original_relation line 98
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_relation line 105
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.inherited_original_words line 116
Source documentation
The inherited original row keeps the complete input predicate.
```
theorem inherited_original_words (e : Fin t.darts) :
    GraphTables.rowWords (actualRow t padding tables (.inl e) (.inr ())) =
      [e.val, (q + 1) * t.rows[e].reverseIndex.val + q] ++
        GraphTables.relationWords t.rows[e].relation := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationWords
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_words line 124
Source documentation
The inherited dummy row is an always-accepting self-loop.
```
theorem inherited_dummy_words (v : Fin t.vertices) (j : Fin (padding v)) :
    GraphTables.rowWords (actualRow t padding tables (.inr ⟨v, j⟩) (.inr ())) =
      [t.darts + PreprocessingPaddingOffsets.offset padding v.val + j.val,
        (q + 1) * (t.darts + PreprocessingPaddingOffsets.offset padding v.val + j.val) + q] ++
        GraphTables.relationWords MachineDummyRows.trueRelation := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.offset, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationWords
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.encodeWords_flatMap line 133
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow_bits line 140
Source documentation
Per-row serialization agrees with the generic table codec.
```
theorem actualRow_bits (x : Vertex t padding) (p : Fin q ⊕ Unit) :
    encodeWords (GraphTables.rowWords (actualRow t padding tables x p)) =
      PreprocessingPaddingWords.rowBits (ofCloudTables t padding tables)
        (vertexOrder t padding x) (portOrder q p) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.vertexBits_eq line 149
Source documentation
Each block uses exactly the port order of the actual stored table.
```
theorem vertexBits_eq (x : Vertex t padding) :
    vertexBits t padding tables x =
      PreprocessingPaddingWords.vertexBits (ofCloudTables t padding tables)
        (vertexOrder t padding x) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.vertexBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.vertexBits
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.paddingOrder_ofFn line 167
Source documentation
The explicit padding list is the inverse enumeration of its numeric order.
```
theorem paddingOrder_ofFn :
    List.ofFn (paddingOrder padding).symm = paddingList padding := by
…
```

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.vertexOrder_ofFn line 179

Source documentation

Any global-vertex payload follows old darts, then the explicit dummy list.

theorem vertexOrder_ofFn {α : Type*} (f : Vertex t padding → α) :
    List.ofFn (fun i : Fin (vertexCount t padding) => f ((vertexOrder t padding).symm i)) =
      List.ofFn (fun e : Fin t.darts => f (.inl e)) ++
        (paddingList padding).map (fun z => f (.inr z)) := by
…

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.paddingList_flatMap line 209

Source documentation

The stored dummy list uses exactly the nested owner/local-index loop order.

theorem paddingList_flatMap {α : Type*} (f : (Σ v : Fin t.vertices, Fin (padding v)) → List α) :
    (paddingList padding).flatMap f =
      (List.ofFn (fun v : Fin t.vertices =>
        (List.ofFn (fun j : Fin (padding v) => f ⟨v, j⟩)).flatten)).flatten := by
…

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.rowsBits_ofCloudTables line 217
Source documentation
The whole actual row stream, split into the two executable outer loops.
```
theorem rowsBits_ofCloudTables :
    PreprocessingPaddingWords.rowsBits (ofCloudTables t padding tables) =
      (List.ofFn (originalVertexBits t padding tables)).flatten ++
        (List.ofFn (fun v : Fin t.vertices =>
          (List.ofFn (dummyVertexBits t padding tables v)).flatten)).flatten := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowsBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.originalVertexBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.tableBits_ofCloudTables line 237
Source documentation
Exact complete codec identity: new headers, original blocks, then dummy blocks.
```
theorem tableBits_ofCloudTables :
    PortTables.tableBits (ofCloudTables t padding tables) =
      encodeWords [vertexCount t padding, vertexCount t padding * (q + 1)] ++
        (List.ofFn (originalVertexBits t padding tables)).flatten ++
        (List.ofFn (fun v : Fin t.vertices =>
          (List.ofFn (dummyVertexBits t padding tables v)).flatten)).flatten := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.originalVertexBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits