OAI/Computability/UniqueGames/Machines/PoweringMachineInitialize.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Actual powering initialization on the common finite tape set. The first unary input field is copied by the affine machine and consumed by the checked header program. The original input and every unrelated tape are preserved. No runtime graph or vertex count is captured by the finite program.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.ExtraTape line 19
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.GlobalTape line 20
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.Label line 21
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.finalOutput line 23
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement line 26

    Source documentation

    The unary start vertex and outer counter occupy the same physical tape.

    def commonPlacement (max : Nat) (tape : PoweringMachineTapes.Tape max) : GlobalTape max :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.GlobalTape

  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_injective line 29
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_start line 35
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_table line 39
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_scratch line 44
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_rowOutput line 49
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_finalOutput line 54
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_header line 59
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerPlacement line 67

    Source documentation

    Header writers use the common work tapes but emit on the final output. The relation producer continues to use commonPlacement rowOutput.

    def headerPlacement (max : Nat) (tape : PoweringMachineTapes.Tape max) : GlobalTape max :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.GlobalTape

  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_injective line 71
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_rowOutput line 86
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_eq_common line 90
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_data line 94
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_header line 102
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.castTapes line 114
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.castStatement line 117
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.castConfiguration line 120
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.castTapes_apply line 123
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_mk line 129
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.stepAux_cast line 135
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.boolAlphabet_eq line 143
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.mergeTapes line 149
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.castTapes_embedding line 154
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.dropUnit line 162
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerStatement line 170

    Source documentation

    The native checked header statement is embedded and its inert extra register removed. All four native header tapes keep their identities.

    def headerStatement (max N B : Nat) (label : HeaderLabel) :
    TM2.Stmt (fun _ : GlobalTape max => Bool) Label (Master N) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.GlobalTape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.Label

  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration line 177
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration_eq line 182
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.stepAux_headerStatement line 196
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.program line 209
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerStep line 222
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.headerTrace line 238
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes line 249
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.copyFirstTrace line 252
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.initializeTrace line 285

    Source documentation

    A concrete successful trace: copy the live input count, then execute the existing header machine on that copy. Runtime is exactly 3*vertices+5.

    theorem initializeTrace (max N B vertices : Nat) (extra : ExtraTape max → List Bool)
    (suffix : List Bool)
    (input : extra (.inl (PoweringMachineTapes.table max)) = encodeWord vertices ++ suffix)
    (scratch : extra (.inl (PoweringMachineTapes.scratch max)) = [])
    (state : Master N) :
    (MachineComposition.advance (TM2.step (program max N B)))^[3 * vertices + 5]
      (some ⟨some (.inr .seed), state, initialGlobalTapes extra⟩) =
      some ⟨none, (state.1, none), mergeTapes (finalTapes B vertices []) extra⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.ExtraTape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.table, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.scratch, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineComposition.advance, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.program, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.mergeTapes

  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.initializeInTime line 297
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.instruction line 312

    Source documentation

    The five finite initialization labels can be placed in a caller's program. The native halt becomes its chosen continuation in the very same transition.

    def instruction {Λ : Type} (max N B : Nat) (labels : Label → Λ) (exit : Option Λ)
    (label : Label) : TM2.Stmt (fun _ : GlobalTape max => Bool) Λ (Master N) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.GlobalTape

  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.initializeAtInTime line 316
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.final_counter line 331
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.final_vertices line 336
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.final_darts line 339
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineInitialize.final_extra line 342