MachineExpanderTableRows.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Actual execution of all expander-table positions for one vertex

The inner loop calls the complete row machine once per fixed cloud/port position. The returned state and the successful machine execution are constructed together. Neither a row execution nor an inner-loop execution is a caller premise.

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.singleStep line 21
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.sequence line 27
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.widen line 34
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.tableRowData line 40
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.tableRowData_finalValue line 44
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.tableRowData_frame0 line 48
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.tableRowData_finalFrame line 55
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowAfterState line 68
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowAfterState_position line 74
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller_rowAfterState line 79

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.preparedRowInTime line 85

Source documentation

Preparation and one actual embedded row call, with the two extra tapes retained. The row value is computed from the actual old and small tables.

def preparedRowInTime (positive : 0 < d) (G : Table v (degree d))
    (H : Table (cloudSize d) d) (vertex : Fin v) (state : State ρ d)
    (remaining : Nat) (output countSuffix result : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program positive H))
      ⟨some (.inr .prepareRow), state,
        boundaryTapes vertex.val remaining (encodeWords (rotationWords G)) output countSuffix result⟩
      (some ⟨some (.inr .afterRow), rowAfterState positive G H vertex state,
        boundaryTapes vertex.val remaining (encodeWords (rotationWords G))
          ((encodeWord (rowValue G H vertex state.2)).reverse ++ output) countSuffix result⟩)
      (1 + 80 * ((encodeWords (rotationWords G)).length + 1)) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowAfterState, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.VertexSuffixRun line 116
Source documentation
A successful suffix of the finite position loop, returning actual finite state together with the execution certificate and its preserved caller.
```
structure VertexSuffixRun (positive : 0 < d) (G : Table v (degree d))
    (H : Table (cloudSize d) d) (vertex : Fin v) (state : State ρ d)
    (remaining : Nat) (output countSuffix result : List Bool) where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.suffixRun_aux line 130
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.suffixInTime line 184
structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.VertexRun line 192
Source documentation
The complete inner loop for one vertex, starting at position zero.
```
structure VertexRun (positive : 0 < d) (G : Table v (degree d))
    (H : Table (cloudSize d) d) (vertex : Fin v) (state : State ρ d)
    (remaining : Nat) (output countSuffix result : List Bool) where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexInTime line 206