OAI/Computability/UniqueGames/Machines/MachineExpanderTable.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Complete finite machine execution for the next expander table

The initialized old table and unary vertex count are consumed by one actual finite program. The machine writes precisely the complete square/zigzag rotation table, preserving its old table and all promised framing. The bound is quadratic in the unary old-table length for each fixed small graph.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.completeBudget line 21
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.timeCoefficient line 24
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.timePolynomial line 27
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertices_le_word_length line 30
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.completeBudget_le line 40

    Source documentation

    All actual loop, row, and final reversal costs are bounded quadratically.

    theorem completeBudget_le {v d : Nat} (positive : 0 < d)
    (G : Table v (degree d)) (H : Table (cloudSize d) d) :
    completeBudget G H ≤ (timePolynomial d).eval (oldTableWord G).length := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.completeBudget, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.timePolynomial, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.oldTableWord

  6. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.TableRun line 75
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.initializeInTime line 87
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.tableInTime line 106

    Source documentation

    Construct the entire table execution from its actual initialized inputs. No row trace, loop trace, or abstract computational witness is a hypothesis.

    def tableInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (state : State ρ d) (suffix : List Bool) : TableRun positive G H state suffix := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.TableRun