OAI/Computability/UniqueGames/PCP/Initialization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Actual setup-to-guard execution of the alphabet-table driver. The preserved input is parsed by Setup; the finite header template runs through an explicit state equivalence. The resulting loop invariant is a complete tape equation.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.inputTapes line 19
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.rowsBits line 23
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.headerBits line 26
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.setupTapes line 30
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.loopTapes line 39

    Source documentation

    Complete initial loop state. Every auxiliary tape not listed here is empty.

    def loopTapes (input : GenericGraphTables.Table q) : Tape → List Bool
  | .original => GenericGraphTables.tableBits input
  | .cursor => rowsBits input
  | .vertices => encodeWord input.vertices
  | .darts | .counter => encodeWord input.darts
  | .edge => encodeWord 0
  | .reversed => (headerBits input).reverse
  | _ => []

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.rowsBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.headerBits

  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.loopStart line 48
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.setupResult_eq line 52
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.headerResult_eq line 58
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.machineInitial_eq line 63
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.setupInTime line 74

    Source documentation

    The driver executes its actual setup statements from its actual input configuration.

    def setupInTime (input : GenericGraphTables.Table q) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      (initList (Driver.machine q) (GenericGraphTables.tableBits input))
      (some ⟨some (Driver.headerEntry q), initial q, setupTapes input⟩)
      (6 * (GenericGraphTables.tableBits input).length + 11) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.headerEntry, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.setupTapes

  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.headerView_at line 93
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.headerInTime line 105

    Source documentation

    No header execution is assumed: the checked template is instantiated at the concrete driver labels and transported through the finite state layout.

    def headerInTime (input : GenericGraphTables.Table q) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      ⟨some (Driver.headerEntry q), initial q, setupTapes input⟩
      (some (loopStart input))
      (7 * (3 * ((GenericGraphTables.tableBits input).length + 1) + 3) + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.headerEntry, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.setupTapes, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.loopStart, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits

  13. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.time line 143
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.time_eq line 145
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.initializeInTime line 151

    Source documentation

    Actual initialization of the complete finite driver, ending at its first guard with the exact input, counter, cursor, index, and reversed headers.

    def initializeInTime (input : GenericGraphTables.Table q) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      (initList (Driver.machine q) (GenericGraphTables.tableBits input))
      (some (loopStart input)) (time (GenericGraphTables.tableBits input).length) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.loopStart, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.time