OAI/Computability/UniqueGames/Machines/MachineRegularTableTrace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.joinTrace line 10

   Also declared: OAI/Computability/UniqueGames/Machines/MachineRegularTable.lean:1235 (same declaration text).

2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.normalizeEmptyAppend line 14
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerStartTrace line 18
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerOldTrace line 30
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.beforeCleanupTrace line 46
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleanupFinalTrace line 62
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.fullTrace line 70
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.update_frame_output line 78
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.input_stacks_eq line 91
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.initial_cfg_eq line 111
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.trace line 122

    Source documentation

    Complete execution from the actual serialized input. All header reads, metadata, geometric rotors, rows, counters and cleanup are run by this one finite machine. No body trace or target-table computation is supplied as a premise.

    theorem trace (H : BaseTable) (t : GraphTables.Table) :
        (advance (TM2.step (program H)))^[totalTime H t]
          (some (Turing.initList (machine H) (GraphTables.tableBits t))) =
          some ⟨none, readyState H,
            Function.update (Turing.initList (machine H) (GraphTables.tableBits t)).stk
              (coreTape 8) (PortTables.tableBits (PreprocessingRegularTables.regularize H t))⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.readyState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.coreTape