OAI/Computability/UniqueGames/PCP/RawInitialMachineCleanup.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual cleanup of all six clause-field tapes followed by the global unary index increment. The output accumulator, unread input, and other caller tapes are preserved, and no additional finish instruction is assumed.

  1. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineCleanup.trace_trans line 16
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineCleanup.incrementIndexTrace line 21

    Source documentation

    The index increment is exactly the one push in the actual global program.

    theorem incrementIndexTrace (base : Tape → List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[1]
      (some ⟨some .incrementIndex, state, base⟩) =
      some ⟨some .guard, state, Function.update base .index (true :: base .index)⟩ := by
…
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineCleanup.cleanupTrace line 28

    Source documentation

    Clear six actual field tapes, increment the index, and return to the guard.

    theorem cleanupTrace {n : ℕ} (base : Tape → List Bool) (c : Target.Clause n)
    (suffix : List Bool) (i : ℕ)
    (hempty : ∀ j, base (.field j) = []) (hindex : base .index = encodeWord i)
    (incoming : State) :
    (MachineComposition.advance (TM2.step program))^[
        (encodeWords (Complexity.clauseWords c)).length + 7]
      (some ⟨some (.cleanupField 0), incoming, recordTapes base c suffix⟩) =
      some ⟨some .guard, (incoming.1, none),
        Function.update (Function.update base .input suffix) .index (encodeWord (i + 1))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Clause, OAI.UniqueGamesTheorem.Foundations.Complexity.clauseWords

  4. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineCleanup.cleanupInTime line 111