OAI/Computability/UniqueGames/Machines/PoweringInitializeFrame.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialExtra line 12

   Source documentation

   The extra tapes initially contain only the live serialized table.

   def initialExtra (graph : PortTables.Table vertices d) (n : Nat) :
       PoweringMachineInitialize.ExtraTape (PoweringMachineRowBody.capacity n) → List Bool :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.ExtraTape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.capacity

2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialExtra_table line 17
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialExtra_other line 21
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialExtra_scratch line 26
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.preparedTapes line 32

   Source documentation

   Exact frame left by initialization, including the preserved input table.

   def preparedTapes (graph : PortTables.Table vertices d) (n : Nat) :
       PoweringMachineGlobal.Tape n → List Bool :=
   …

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

6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_commonRole line 38
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_ready line 46
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_start line 56
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_counter line 64

   Source documentation

   Installing the outer-loop counter changes nothing: it is already present.

   theorem prepared_counter (graph : PortTables.Table vertices d) (n : Nat) :
       PoweringMachineOuterLoop.counter (PoweringMachineGlobal.placement n)
         (preparedTapes graph n) vertices = preparedTapes graph n := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.counter, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.placement, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.preparedTapes

10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_output line 71
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_vertices line 76
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_darts line 79
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.prepared_source line 83
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.preparedCfg line 86
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialGlobalTapes_eq line 92

    Source documentation

    A homogeneous Boolean description of the machine's literal initial stacks.

    theorem initialGlobalTapes_eq (graph : PortTables.Table vertices d) (n : Nat) :
        PoweringMachineInitialize.initialGlobalTapes (initialExtra graph n) =
          fun tape => if tape = PoweringMachineGlobal.inputTape n
            then PortTables.tableBits graph else [] := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialExtra, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.inputTape

16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.machine_initialStacks line 107
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initList_eq line 114

    Source documentation

    The trace starts at Turing.initList, with no assumed prepared work tapes.

    theorem initList_eq (graph : PortTables.Table vertices d) (n : Nat) :
        initList (PoweringMachineGlobal.machine d n) (PortTables.tableBits graph) =
          ⟨some (PoweringMachineGlobal.main d n),
            PoweringMasterState.clean (PoweringMachineRowBody.bufferSize d n),
            PoweringMachineInitialize.initialGlobalTapes (initialExtra graph n)⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.main, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initialExtra

18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.tableBits_head line 124

    Source documentation

    The first serialized input field is the actual number of vertices.

    theorem tableBits_head (graph : PortTables.Table vertices d) :
        PortTables.tableBits graph = encodeWord vertices ++
          encodeWords (PortTables.tableWords graph).tail := rfl

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

19. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.initializeInTime line 130

    Source documentation

    Initialization of the actual global program from its literal input list. Every work-tape readiness property follows from the explicit final frame.

    def initializeInTime (graph : PortTables.Table vertices d) (n : Nat) :
        StateTransition.EvalsToInTime (PoweringMachineGlobal.machine d n).step
          (initList (PoweringMachineGlobal.machine d n) (PortTables.tableBits graph))
          (some (preparedCfg graph n)) (3 * vertices + 5) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringInitializeFrame.preparedCfg