PreprocessingPaddingWords.lean`

41 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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.encodeWords_flatMap_inline_PreprocessingPaddingWords line 22

theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.ofFn_split line 29

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.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv

theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.flatten_ofFn_rowIndex line 40

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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits line 56
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits line 60
def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits line 64
Source documentation
The old encoded rows, without their two header words.
```
def rowsBits (table : Table n d) : List Bool :=
…
```
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_flat line 68
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.MaxCutGames.Foundations.PCP.GraphTables.rowWords, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_eq_vertices line 75
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_old line 90
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_new line 103
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv

theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.dummy_rowsBits_eq_ofFn line 114

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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.paddingBits_eq_ofFn line 129

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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_old line 143
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_new line 148
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_pad line 161
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.tableBits_pad line 169
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow line 198
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.MaxCutGames.Foundations.PCP.GraphTables.DartRow
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.vertexRows line 204
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.MaxCutGames.Foundations.PCP.GraphTables.DartRow
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.originalVertexRows line 209
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexRows line 210
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.vertexBits line 213
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.originalVertexBits line 216
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits line 217
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_internal line 221
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.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.MaxCutGames.Foundations.PCP.PreprocessingInternalRows.row
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_eq line 225
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_tail line 235
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_reverse line 239
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_reverse line 251
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.relation_ext_inline_PreprocessingRegularWords line 264
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_relation line 272
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_relation line 279
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_words line 290
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.MaxCutGames.Foundations.PCP.GraphTables.rowWords, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.MaxCutGames.Foundations.PCP.GraphTables.relationWords
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_words line 298
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.MaxCutGames.Foundations.PCP.GraphTables.rowWords, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.offset, OAI.MaxCutGames.Foundations.PCP.GraphTables.relationWords
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.encodeWords_flatMap_inline_PreprocessingRegularWords line 307
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_bits line 314
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.MaxCutGames.Foundations.PCP.GraphTables.rowWords, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.actualRow, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.vertexBits_eq line 323
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.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.vertexBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.paddingOrder_ofFn line 341
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.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.vertexOrder_ofFn line 353

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.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.paddingList_flatMap line 384

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.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.rowsBits_ofCloudTables line 392
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.MaxCutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.originalVertexBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.tableBits_ofCloudTables line 412
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.MaxCutGames.Foundations.PCP.PortTables.tableBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.originalVertexBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits