OAI/Computability/UniqueGames/Machines/MachineClone100Triples.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowOutput line 16
  2. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowSteps line 22
  3. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.startAt line 26
  4. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.contextTapes_field line 29
  5. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowOutput_update line 34
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowSteps_update line 39
  7. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.chain line 43
  8. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.fourContexts_tapes line 47
  9. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowTrace line 59

    Source documentation

    Execute each of the four actual contexts in slot order.

    theorem rowTrace (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (i : Fin triples.length) (base : Tape → List Bool)
    (scratchEmpty : base .scratch = []) (state : State triples.length) :
    (MachineComposition.advance (TM2.step (program triples nonempty)))^[rowSteps base]
      (some ⟨some (.setup (.inr (i, 0))), state, base⟩) =
      some ⟨startAt triples.length (i.val + 1), initialState _,
        Function.update base .reversed ((rowOutput (triples.get i) base).reverse ++
          base .reversed)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowSteps, OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.startAt, OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowOutput

  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.tailTrace line 94
  11. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.tableTrace_raw line 134
  12. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.affineRecord line 145
  13. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.rowOutput_words line 148
  14. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.tableOutput_words line 156
  15. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.tableTrace line 169

    Source documentation

    The actual inner loop outputs the concrete cloned equation words.

    theorem tableTrace (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (base : Tape → List Bool) (scratchEmpty : base .scratch = [])
    (state : State triples.length) (a b c rhs : Nat)
    (h0 : base (.field 0) = encodeWord a) (h1 : base (.field 1) = encodeWord b)
    (h2 : base (.field 2) = encodeWord c) (h3 : base (.field 3) = encodeWord rhs) :
    (MachineComposition.advance (TM2.step (program triples nonempty)))^[
      triples.length * (3 * ((a + 1) + (b + 1) + (c + 1) + (rhs + 1)) + 12)]
      (some ⟨some (.setup (.inr (⟨0, List.length_pos_iff.mpr nonempty⟩, 0))), state, base⟩) =
      some ⟨some (.cleanup 0), initialState _, Function.update base .reversed
        ((encodeWords (triples.flatMap (affineRecord a b c rhs))).reverse ++ base .reversed)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.affineRecord

  16. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Triples.tableTapes_other line 183