OAI/Computability/UniqueGames/Machines/MachineExpanderTableLoop.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual outer vertex iteration for expander tables

The invariant is the reversed unary encoding of all completed vertices. Each positive unary guard invokes the proved complete fixed-position row loop; the zero guard enters the actual output-reversal phase. No execution premise is supplied by the caller.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.oldTableWord line 20
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.accumulatedVertices line 23
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_zero line 27
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_succ line 31
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_full line 37
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexBodyBudget line 42
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexLoopBudget line 45
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexLoopTapes line 48
  9. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.VertexLoopRun line 52
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundarySingleStep line 63
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexLoopInTime line 70

    Source documentation

    Execute every remaining vertex in the common finite table program.

    def vertexLoopInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (current remaining : Nat) (state : State ρ d) (suffix : List Bool)
    (count : current + remaining = v) (position : state.2 = zeroPosition positive) :
    VertexLoopRun positive G H current remaining state suffix := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.zeroPosition, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.VertexLoopRun