OAI/Computability/UniqueGames/Machines/MachineRegularOriginalClean.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Reusable inherited-row execution with actual cleanup

Five concrete drain loops remove the query delimiter, unread scan suffix, raw reverse field, computed reverse field, and copied relation. With initially empty work tapes, the only final tape change is the appended output row. The index on tape zero and input table on tape one are both preserved.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.Tape line 19
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.Alphabet line 20
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.State line 21
  4. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.Label line 23
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.instruction line 28
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.cleanupTapes line 38
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps line 42
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.join_trace line 46
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.cleanupTraceAt line 50
  10. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.Input line 84
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.cleanup_frame line 89
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.suffix_length_le line 103
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_eq line 113
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_le line 157
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.steps line 171
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.timeBound line 175
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.steps_le line 178
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.traceAt line 186
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.machine line 205
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.machineInTime line 217

    Source documentation

    Exact inherited-row emission with all working tapes restored to empty.

    def machineInTime (H : BaseTable) (t : Table) (e : Fin t.darts)
    (base : Tape → List Bool) (input : Input t e base) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine internalDegree).step
      ⟨some (.row (.lookup .seed)), (((), MachineRegularOriginalRow.zeroBuffer), register), base⟩
      (some ⟨none, (((), MachineRegularOriginalRow.zeroBuffer), none),
        Function.update base (9 : Tape)
          (base (9 : Tape) ++ encodeWords (rowWords (MachineRegularOriginalRow.inheritedRow H t e)))⟩)
      (timeBound internalDegree (tableBits t).length (base (9 : Tape)).length) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.Input, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.timeBound