OAI/Computability/UniqueGames/Machines/MachineTableSplit.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

A fixed five-tape machine physically copies a graph table, preserves the original input, and splits its two unary header fields from the copied rows. The exact trace is ambient-state polymorphic for static machine placement.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Tape line 17
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.State line 18
  3. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Label line 20
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Label.enumList line 24
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Label.enumList_getElem?_ctorIdx_eq line 27
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Label.enumList_nodup line 31
  7. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.(instance at line 33) line 33
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.tapes line 39

    Source documentation

    Tape 0 is protected input, 1 is the working row stream, 2 is scratch, and 3 and 4 hold the extracted vertex and dart counts.

    def tapes (original work vertices darts : List Bool) : Tape → List Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Tape

  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.initialTapes line 43
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.resultTapes line 45
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.resultTapes_original line 48
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.resultTapes_work line 52
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.resultTapes_scratch line 55
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.resultTapes_vertices line 58
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.resultTapes_darts line 61
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.program line 65

    Source documentation

    Six finite control labels, independent of all input sizes and contents.

    def program {σ : Type} : Label → TM2.Stmt (fun _ : Tape => Bool) Label (State σ)
  | .copyFirst => Reduction.MachineTransfer.loopAt 0 2 id false .copyFirst (some .copySecond)
  | .copySecond => MachineCopy.forkLoop 2 0 1 false .copySecond (some .startVertices)
  | .startVertices => Hastad.SourceMachine.fieldStart 3 .readVertices
  | .readVertices => Hastad.SourceMachine.fieldLoop 1 3 .readVertices (some .startDarts)
  | .startDarts => Hastad.SourceMachine.fieldStart 4 .readDarts
  | .readDarts => Hastad.SourceMachine.fieldLoop 1 4 .readDarts none

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.State, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldStart, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceMachine.fieldLoop

  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.exactSteps line 73
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.splitTrace line 76
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.timePolynomial line 146
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.timePolynomial_eval line 148
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.exactSteps_le line 151
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.splitInTime line 158
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.machine line 168
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.initial_configuration line 179
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.rowsBits line 186
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.tableBits_header_rows line 189
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.tableTrace line 193
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.initializedTableInTime line 203

    Source documentation

    The concrete machine starts at its genuine initial configuration on a full graph table and leaves every output field on the stated physical tape.

    def initializedTableInTime (table : PCP.GraphTables.Table) :
    StateTransition.EvalsToInTime machine.step (initList machine (PCP.GraphTables.tableBits table))
      (some ⟨none, ((), none), resultTapes table.vertices table.darts (rowsBits table)⟩)
      (timePolynomial.eval (PCP.GraphTables.tableBits table).length) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.machine, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.resultTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.rowsBits