OAI/Computability/UniqueGames/Machines/MachineClone100Headers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.parsedTapes line 16
  2. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes line 25

    Source documentation

    Exact header-stage endpoint. The occurrence counter is retained for the body loop; generated output is accumulated in reverse.

    def resultTapes (triples : List (Nat × Nat × Nat)) (base : Tape → List Bool)
    (n m : Nat) (suffix : List Bool) : Tape → List Bool
  | .input => suffix
  | .header => []
  | .counter => encodeWord m
  | .reversed => (encodeWords [100 * n, triples.length * m]).reverse
  | tape => base tape
  3. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes_input line 33
  4. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes_header line 35
  5. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes_counter line 37
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes_reversed line 39
  7. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes_scratch line 42
  8. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes_field line 44
  9. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes_output line 46
  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.twoFieldsTapes line 49
  11. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.firstContextTapes line 58
  12. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.secondContextTapes line 66
  13. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.clearHeaderTapes line 76
  14. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.headersTrace line 85
  15. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.headersInTime line 161

    Source documentation

    The exact header trace packaged in the machine execution-time interface.

    def headersInTime (triples : List (Nat × Nat × Nat)) (hne : triples ≠ [])
    (base : Tape → List Bool) (n m : Nat) (suffix : List Bool)
    (hinput : base .input = encodeWords [n, m] ++ suffix)
    (hheader : base .header = []) (hcounter : base .counter = [])
    (hscratch : base .scratch = []) (hreversed : base .reversed = []) :
    StateTransition.EvalsToInTime (TM2.step (program triples hne))
      ⟨some (.headerStart 0), initialState triples.length, base⟩
      (some ⟨some .guard, initialState triples.length,
        resultTapes triples base n m suffix⟩) (5 * n + 4 * m + 18) where
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.resultTapes

  16. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Headers.headersTime_linear line 174