OAI/Computability/MaxCut/Games/PoweringInitializeFrame.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Concrete global configurations and tape separation

These lemmas specialize the checked initializer placement to the fixed global machine. The final configuration is the actual Turing.haltList, with the machine's clean initial register and only the output tape populated.

  1. def OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra line 13

    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.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.ExtraTape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.capacity

  2. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_table line 18
  3. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_other line 22
  4. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_scratch line 27
  5. def OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.preparedTapes line 33

    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.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.Tape

  6. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_commonRole line 39
  7. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_ready line 47
  8. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_start line 57
  9. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_counter line 65

    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.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.counter, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.placement, OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.preparedTapes

  10. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_output line 72
  11. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_vertices line 77
  12. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_darts line 80
  13. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_source line 84
  14. def OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.preparedCfg line 87
  15. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialGlobalTapes_eq line 93

    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.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes, OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.inputTape

  16. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.machine_initialStacks_inline_PoweringInitializeFrame line 108
  17. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initList_eq line 120

    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.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.main, OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clean, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes, OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra

  18. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.tableBits_head line 130

    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.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  19. def OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.initializeInTime line 136

    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.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.MaxCutGames.Foundations.Complexity.PoweringInitializeFrame.preparedCfg

  20. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_injective line 164
  21. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_output line 167
  22. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.output_ne_placement line 173
  23. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_placement line 177
  24. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_placement line 183
  25. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerVertices line 189
  26. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerDarts line 193
  27. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_headerDarts line 197
  28. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_output line 200
  29. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_output line 203
  30. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_scratch line 206
  31. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_scratch line 211
  32. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.scratch_ne_output line 216
  33. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.boolList_mpr_eq line 223

    Source documentation

    A Boolean tape alphabet is constant, so the type-equality transport in the bundled machine's dependent stack specification leaves its word intact.

    @[simp] theorem boolList_mpr_eq (h : List Bool = List Bool) (bits : List Bool) :
    h.mpr bits = bits := rfl
  34. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_tapes line 228

    Source documentation

    The dependent stack definition in haltList is exactly the Boolean output tape shape produced by the checked finite cleanup program.

    theorem haltList_tapes (d n : Nat) (output : List Bool) :
    (Turing.haltList (machine d n) output).stk =
      MachineDrainMany.haltTapes (outputTape n) output := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.haltTapes

  35. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_eq line 239

    Source documentation

    Exact identity with the global machine's actual output specification.

    theorem haltList_eq (d n : Nat) (output : List Bool) :
    Turing.haltList (machine d n) output =
      (⟨none, PoweringMasterState.clean (PoweringMachineRowBody.bufferSize d n),
        MachineDrainMany.haltTapes (outputTape n) output⟩ : (machine d n).Cfg) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMasterState.clean, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.haltTapes