OAI/Computability/UniqueGames/Machines/GraphCounterModel.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

A fixed Boolean-stack program prepending the logarithmic round count to a graph table. It copies the original word, adds its two unary header values, runs the actual logarithm machine, then emits the counter and original word.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraTape line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList line 19
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_getElem?_ctorIdx_eq line 21
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_nodup line 25
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.(instance at line 27) line 27
  6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraLabel line 31
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList line 36
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_getElem?_ctorIdx_eq line 39
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_nodup line 43
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.(instance at line 45) line 45
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.Tape line 49
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.Label line 50
  13. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.Alphabet line 51
  14. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.State line 52
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.initialState line 54
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockLabel line 56
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockStatement line 61

    Source documentation

    Homogeneous Boolean embedding of the fixed logarithm program.

    def clockStatement : TM2.Stmt MachineLogCounter.Alphabet (Fin 5) MachineLogCounter.State →
    TM2.Stmt Alphabet Label State
  | .push k f next => .push (.inl k) (fun state => f state.1) (clockStatement next)
  | .peek k f next => .peek (.inl k) (fun state x => (f state.1 x, state.2)) (clockStatement next)
  | .pop k f next => .pop (.inl k) (fun state x => (f state.1 x, state.2)) (clockStatement next)
  | .load f next => .load (fun state => (f state.1, state.2)) (clockStatement next)
  | .branch f yes no => .branch (fun state => f state.1) (clockStatement yes) (clockStatement no)
  | .goto f => .goto (fun state => .inl (f state.1))
  | .halt => .goto (fun _ => .inr .clearInput)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.State, OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.State

  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.readHeader line 71
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.program line 77
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.machine line 95
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockTapes line 106
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockConfiguration line 110
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockTapes_update line 114
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockStatement_simulation line 121
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockStep line 146
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockInTime line 161