OAI/Computability/UniqueGames/Machines/MachineRegularLift.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The outer construction uses independent finite registers for its existing subprograms. This transport combines tape placement, an untouched register frame, and a static register equivalence, without adding any machine steps.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Lift.statement line 22
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Lift.configuration line 28
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Lift.stepAux line 36
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Lift.step line 49
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Lift.trace line 71