OAI/Computability/UniqueGames/PCP/RawInitialMachineLoop.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact execution of the clause loop, in the original occurrence order.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoop.finalSigns line 15
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoop.trace_trans line 20
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoop.empty_loopTapes line 24
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoop.loopTrace line 31

    Source documentation

    The complete actual loop: every clause is read once, emits six rows, and leaves clean field tapes before the next guard. The final zero guard is included.

    theorem loopTrace {n : Nat} (i : Nat) (cs : List (Clause n))
    (rev : List Bool) (state : State) :
    (MachineComposition.advance (TM2.step program))^[loopTime i cs]
      (some ⟨some .guard, state, loopTapes n i cs.length (clauseInput cs) rev⟩) =
      some ⟨some (.scan .dummyVariables), (finalSigns state.1 cs, none),
        finishTapes n (i + cs.length) ((encodeWords (clauseOutput n i cs)).reverse ++ rev)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoop.finalSigns

  5. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoop.loopInTime line 55