OAI/Computability/UniqueGames/PCP/RawInitialMachineFinish.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Exact execution of the dummy-row and final cleanup/reversal phases.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.tapes line 14
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.finishTapes line 22
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.trace_trans line 25
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.trueRelationWords line 29
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.dummyBits_length line 36
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.update_reversed line 44
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.cleanupTrace line 50
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.resetReverseTrace line 99
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.update_finish line 130
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.copyFinishTrace line 134
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.closeDummyTailTrace line 150
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.closeDummyReverseTrace line 159
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.dummyRelationTrace line 168
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.dummyTrace line 180

    Source documentation

    The three actual prefix scans and three emitting transitions append the complete dummy row.

    theorem dummyTrace (n m : Nat) (rev : List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[2 * n + 4 * m + 9]
      (some ⟨some (.scan .dummyVariables), state, finishTapes n m rev⟩) =
      some ⟨some (.cleanupFinal 0), (state.1, none),
        finishTapes n m ((encodeWords (RawInitialRows.dummyWords n m)).reverse ++ rev)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.finishTapes, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.dummyWords

  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.finishTrace line 218

    Source documentation

    Exact final execution, including all tape cleanup and the canonical halt state.

    theorem finishTrace (n m : Nat) (rev : List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[
        3 * n + 5 * m + 17 + (encodeWords (RawInitialRows.dummyWords n m)).length + rev.length]
      (some ⟨some (.scan .dummyVariables), state, finishTapes n m rev⟩) =
      some (haltList machine (rev.reverse ++ encodeWords (RawInitialRows.dummyWords n m))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialRows.dummyWords, OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.finishTapes

  16. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineFinish.finishInTime line 236