PreprocessingPaddingWords.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Exact serialization of whole-vertex padding

The original dart rows remain in their original order, with every old tail, reverse index, and relation bit unchanged. The suffix is exactly the bit stream emitted by the checked dummy-vertex machine, starting at vertex n and dart n*d. This is an equality for the actual table codec, with no runtime premise.

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.encodeWords_flatMap line 24
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.ofFn_split line 31
Source documentation
Split any indexed list at the actual old/new vertex boundary.
```
theorem ofFn_split {α : Type*} (h : n ≤ m) (f : Fin m → α) :
    List.ofFn f =
      List.ofFn (fun v : Fin n => f (v.castLE h)) ++
        List.ofFn (fun v : Fin (m - n) => f (PreprocessingPaddingTables.vertexEquiv h (.inr v))) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.flatten_ofFn_rowIndex line 42

Source documentation

Mixed-radix row order is vertex-major, then increasing port order.

theorem flatten_ofFn_rowIndex {α : Type*} (f : Fin (n * d) → List α) :
    (List.ofFn f).flatten =
      (List.ofFn (fun v : Fin n =>
        (List.ofFn (fun p : Fin d => f (rowIndex n d (v, p)))).flatten)).flatten := by
…

def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits line 58
Source documentation
The bits of one actual table row, in the existing graph codec.
```
def rowBits (table : Table n d) (v : Fin n) (p : Fin d) : List Bool :=
…
```
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.vertexBits line 62
def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowsBits line 66
Source documentation
The old encoded rows, without their two header words.
```
def rowsBits (table : Table n d) : List Bool :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits_flat line 70
Source documentation
Recover the original flat row from its exact mixed-radix coordinates.
```
theorem rowBits_flat (table : Table n d) (i : Fin (n * d)) :
    encodeWords (GraphTables.rowWords ((flatRows table)[i])) =
      rowBits table ((rowIndex n d).symm i).1 ((rowIndex n d).symm i).2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowsBits_eq_vertices line 77
Source documentation
Serializing all rows agrees with grouping their bits by vertex and port.
```
theorem rowsBits_eq_vertices (table : Table n d) :
    rowsBits table = (List.ofFn (fun v : Fin n => vertexBits table v)).flatten := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowsBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.vertexBits
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_old line 92
Source documentation
Every bit in an original row survives padding unchanged.
```
theorem rowBits_pad_old (table : Table n d) (h : n ≤ m) (v : Fin n) (p : Fin d) :
    rowBits (PreprocessingPaddingTables.pad table h) (v.castLE h) p = rowBits table v p := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_new line 105
Source documentation
A new row is the machine's self-loop row with its actual global index.
```
theorem rowBits_pad_new (table : Table n d) (h : n ≤ m)
    (v : Fin (m - n)) (p : Fin d) :
    rowBits (PreprocessingPaddingTables.pad table h)
        (PreprocessingPaddingTables.vertexEquiv h (.inr v)) p =
      MachineDummyRows.rowBits (n + v.val) (p.val + d * (n + v.val)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.dummy_rowsBits_eq_ofFn line 116
Source documentation
The row emitter's recursive stream enumerates successive reverse indices.
```
theorem dummy_rowsBits_eq_ofFn (v e count : Nat) :
    MachineDummyRows.rowsBits v e count =
      (List.ofFn (fun p : Fin count => MachineDummyRows.rowBits v (e + p.val))).flatten := by
…
```

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.paddingBits_eq_ofFn line 131

Source documentation

The vertex emitter's recursive stream enumerates consecutive vertex blocks.

theorem paddingBits_eq_ofFn (d v e count : Nat) :
    MachinePaddingRows.paddingBits d v e count =
      (List.ofFn (fun k : Fin count =>
        MachineDummyRows.rowsBits (v + k.val) (e + k.val * d) d)).flatten := by
…

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_old line 145
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_new line 150
Source documentation
The new vertex's complete port block equals the actual machine block.
```
theorem vertexBits_pad_new (table : Table n d) (h : n ≤ m) (v : Fin (m - n)) :
    vertexBits (PreprocessingPaddingTables.pad table h)
        (PreprocessingPaddingTables.vertexEquiv h (.inr v)) =
      MachineDummyRows.rowsBits (n + v.val) (n * d + v.val * d) d := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.vertexBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowsBits_pad line 163
Source documentation
The actual padded row codec is the old row codec followed by the emitted suffix.
```
theorem rowsBits_pad (table : Table n d) (h : n ≤ m) :
    rowsBits (PreprocessingPaddingTables.pad table h) =
      rowsBits table ++ MachinePaddingRows.paddingBits d n (n * d) (m - n) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowsBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.tableBits_pad line 171
Source documentation
Exact final codec identity used by the machine-output correspondence.
```
theorem tableBits_pad (table : Table n d) (h : n ≤ m) :
    tableBits (PreprocessingPaddingTables.pad table h) =
      encodeWords [m, m * d] ++ rowsBits table ++
        MachinePaddingRows.paddingBits d n (n * d) (m - n) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingWords.rowsBits