OAI/Computability/UniqueGames/Machines/MachineSubdivisionTableRead.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual execution of the subdivision controller's full-table reader. The reader consumes exactly the fixed number of zero-delimited table entries, retains the unread input suffix, and reverses the saved table into forward order. No table entry is stored in finite control; only the number of delimiters is.

  1. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tapes line 22
  2. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tapes_input line 25
  3. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tapes_reverse line 28
  4. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.update_input line 31
  5. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.update_reverse line 37
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.step_true line 43
  7. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.step_false line 53
  8. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.readWordTrace line 65

    Source documentation

    One encoded entry consumes its final delimiter in the same transition that increments the finite completed-entry counter.

    theorem readWordTrace (q : Nat) (completed : Fin (q + 1)) (valid : completed.val < q)
    (base : Tape → List Bool) (value : Nat) (input reversed : List Bool)
    (ambient : Unit × Unit) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program q)))^[value + 1]
      (some ⟨some (.readTable completed), (ambient, register),
        tapes base (encodeWord value ++ input) reversed⟩) =
      some ⟨some (.readTable ⟨completed.val + 1, by omega⟩), (ambient, none),
        tapes base input ((encodeWord value).reverse ++ reversed)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tapes

  9. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.readWordsTrace line 87

    Source documentation

    Read a suffix of the q-entry table, stopping before any following data.

    theorem readWordsTrace (q : Nat) (words : List Nat) (completed : Fin (q + 1))
    (complete : completed.val + words.length = q) (base : Tape → List Bool)
    (suffix reversed : List Bool) (ambient : Unit × Unit) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program q)))^[(encodeWords words).length + 1]
      (some ⟨some (.readTable completed), (ambient, register),
        tapes base (encodeWords words ++ suffix) reversed⟩) =
      some ⟨some .reverseTable, (ambient, none),
        tapes base suffix ((encodeWords words).reverse ++ reversed)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tapes

  10. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.finalTapes line 117
  11. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.finalTapes_other line 120
  12. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.finalTapes_input line 125
  13. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.finalTapes_reverse line 128
  14. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.finalTapes_permutation line 131
  15. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tableTrace line 136

    Source documentation

    Full exact table phase: read q delimited entries and reverse the physical saved stack, arriving at the actual row-emission label.

    theorem tableTrace (q : Nat) (words : List Nat) (length : words.length = q)
    (base : Tape → List Bool) (suffix : List Bool)
    (ambient : Unit × Unit) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program q)))^[2 * (encodeWords words).length + 2]
      (some ⟨some (.readTable 0), (ambient, register),
        tapes base (encodeWords words ++ suffix) []⟩) =
      some ⟨some (rowEntry q), (ambient, none), finalTapes base suffix (encodeWords words)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tapes, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.finalTapes

  16. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tableInTime line 165

    Source documentation

    Timed witness for the actual controller, with a fixed alphabet-dependent bound on its full forward table. Other row fields and unread input are preserved.

    def tableInTime {q : Nat} (table : Target.PermutationTable q)
    (base : Tape → List Bool) (suffix : List Bool)
    (ambient : Unit × Unit) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program q))
      ⟨some (.readTable 0), (ambient, register),
        tapes base (encodeWords (tableWords table) ++ suffix) []⟩
      (some ⟨some (rowEntry q), (ambient, none),
        finalTapes base suffix (encodeWords (tableWords table))⟩)
      (2 * (q * (q + 1)) + 2) where
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.tapes, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionTableRead.finalTapes