OAI/Computability/UniqueGames/Machines/PoweringMachineOuterLoopLemmas.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Actual variable-size vertex enumeration. The finite guard decrements the live unary counter, a one-step bridge enters the fixed vertex producer, and the producer returns to the guard. Work tapes may change after every vertex.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.Placement line 18
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.State line 19
  3. structure OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.Ready line 21
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.counter line 29
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.counter_other line 32
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.ready_vertex line 39
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.ready_of_vertex line 58
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.vertexStart line 64
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.vertexEntry line 67
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.bridge line 85
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes line 90

    Source documentation

    The exact tapes produced by repeatedly executing the actual vertex body.

    def finalTapes (graph : PortTables.Table vertices d) (n : Nat) (placement : Placement K n)
    (output : K) : (remaining : Nat) → remaining ≤ vertices → (K → List Bool) → K → List Bool
  | 0, _, base => counter placement base 0
  | r + 1, bounded, base =>
      finalTapes graph n placement output r (by omega)
        (PoweringMachineVertex.finalTapes graph n placement output ⟨r, by omega⟩
          (counter placement base r))

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.Placement, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.counter, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.finalTapes

  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.steps line 98
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.steps_le line 104
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_ready line 116
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows line 141
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_ofFn line 146
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_all line 163
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_output line 170
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_other line 196
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.loopTrace line 208
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.loopInTime line 274
  22. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.Tape line 315
  23. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.State line 318
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.placement line 321
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.inputTape line 325
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.outputTape line 328
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.headerVertices line 331
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.headerDarts line 332
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.enumeration line 334
  30. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.FinishLabel line 338
  31. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.Label line 340
  32. instance OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.labelFintype line 343
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.initLabels line 347
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.guardLabel line 348
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel line 349
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.vertexLabels line 351
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.finishLabels line 354
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.finishEntry line 358

    Source documentation

    Finish first copies the dart-count field, then the vertex-count field.

    def finishEntry (d n : Nat) : Label d n := finishLabels d n (.inl .seed)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.finishLabels

  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.main line 361

    Source documentation

    Initialization first clones the input's live vertex-count field.

    def main (d n : Nat) : Label d n := initLabels d n (.inr .seed)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.initLabels

  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.program line 364

    Source documentation

    The complete program, fixed solely by the reduction parameters.

    def program (d n : Nat) :
    Label d n → TM2.Stmt (fun _ : Tape n => Bool) (Label d n) (State d n)
  | .inl label => PoweringMachineInitialize.instruction
      (PoweringMachineRowBody.capacity n) (PoweringMachineRowBody.bufferSize d n)
      (PCP.PoweringTableLayout.blockSize d n) (initLabels d n) (some (guardLabel d n)) label
  | .inr (.inl false) => MachineUnaryCounter.guard
      (placement n (PoweringMachineTapes.start (PoweringMachineRowBody.capacity n)))
      (bridgeLabel d n) (finishEntry d n)
  | .inr (.inl true) => PoweringMachineOuterLoop.bridge d n (vertexLabels d n) (guardLabel d n)
  | .inr (.inr (.inl label)) => PoweringMachineVertex.instruction n (placement n) (outputTape n)
      (vertexLabels d n) (some (guardLabel d n)) label
  | .inr (.inr (.inr label)) => PoweringMachineFinish.instruction (enumeration n)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.State, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.capacity, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableLayout.blockSize, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.initLabels, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.guardLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.placement, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.start, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.finishEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineOuterLoop.bridge, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.vertexLabels, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.outputTape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.enumeration

  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.atInit line 380
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.atGuard line 385
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.atBridge line 390
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.atVertex line 394
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.atFinish line 398
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine line 406

    Source documentation

    All state and control spaces are explicit finite types; only the tapes hold variable-size data.

    def machine (d n : Nat) : FinTM2 where
…
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine_code line 417
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine_main line 420
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine_initialState line 422
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.input_ne_output line 425
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.placement_injective line 443
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_output line 446
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.output_ne_placement line 452
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_placement line 456
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_placement line 462
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerVertices line 468
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerDarts line 472
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_headerDarts line 476
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_output line 479
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_output line 482
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_scratch line 485
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_scratch line 490
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.scratch_ne_output line 495
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.boolList_mpr_eq line 502

    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
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.haltList_tapes line 507

    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.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.haltTapes

  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalConfiguration.haltList_eq line 515

    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.UniqueGamesTheorem.Foundations.Complexity.PoweringMasterState.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowBody.bufferSize, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.haltTapes