OAI/Computability/UniqueGames/Machines/MachineSingleOrbitProgramLemmas.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Physical postprocessing of the two-side address codec. The program reads 2*C,q,m, writes C,q,m, and replaces each row u,C+v,table by u,v,table. Only the fixed alphabet size q occurs in finite control. All input-dependent integers reside on unary tapes. Six Bool tapes suffice.

  1. inductive OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.Tape line 20
  2. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.Tape.enumList line 24
  3. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.Tape.enumList_getElem?_ctorIdx_eq line 27
  4. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.Tape.enumList_nodup line 31
  5. instance OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.(instance at line 33) line 33
  6. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.State line 37
  7. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.initialState line 39
  8. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.clearKeys line 41
  9. inductive OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.Label line 43
  10. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.copyField line 53

    Source documentation

    Consume one complete unary field, including its delimiter, appending its reverse to the output accumulator. All other tapes are unchanged.

    def copyField {q : Nat} (loopLabel exitLabel : Label q) :
    TM2.Stmt (fun _ : Tape => Bool) (Label q) State :=
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.Label, OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.Tape, OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.State

  11. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.program line 61
  12. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.machine line 97
  13. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.finite_workAlphabet line 108
  14. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.accumulator_not_mem_clearKeys line 113
  15. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.output_not_mem_clearKeys line 114
  16. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitProgram.clearKeys_covers line 116
  17. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tapes line 129
  18. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tapes_input line 137
  19. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tapes_capacity line 138
  20. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tapes_saved line 139
  21. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tapes_remaining line 140
  22. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tapes_accumulator line 141
  23. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tapes_output line 142
  24. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.update_tapes line 144
  25. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.cfg line 151
  26. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.copyStep_true line 155
  27. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.copyStep_false line 164
  28. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.copyFieldTrace line 174

    Source documentation

    The physical field copy takes one transition for each input bit.

    theorem copyFieldTrace {q : Nat} (loopLabel exitLabel : Label q)
    (atLoop : program q loopLabel = copyField loopLabel exitLabel)
    (n : Nat) (suffix c s r a o : List Bool) (register : Option Bool) :
    (advance (TM2.step (program q)))^[n + 1]
      (some (cfg loopLabel register (encodeWord n ++ suffix) c s r a o)) =
      some (cfg exitLabel none suffix c s r ((encodeWord n).reverse ++ a) o) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.cfg

  29. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.tableTrace line 192

    Source documentation

    All permutation fields are copied with a finite delimiter counter.

    theorem tableTrace {q : Nat} (completed : Fin (q + 1)) (words : List Nat)
    (hcount : completed.val + words.length = q)
    (suffix c s r a o : List Bool) (register : Option Bool) :
    (advance (TM2.step (program q)))^[(encodeWords words).length + 1]
      (some (cfg (.table completed) register (encodeWords words ++ suffix) c s r a o)) =
      some (cfg .guard none suffix c s r ((encodeWords words).reverse ++ a) o) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitStreams.cfg

  30. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.halfStep_first line 233
  31. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.halfStep_second line 239
  32. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.halfStep_false line 245
  33. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.halfTrace line 252

    Source documentation

    Consume two unary input marks per output mark, storing the new capacity.

    theorem halfTrace {q : Nat} (n : Nat) (suffix c s r a o : List Bool)
    (register : Option Bool) :
    (advance (TM2.step (program q)))^[2 * n + 1]
      (some (cfg .halfFirst register (encodeWord (2 * n) ++ suffix) c s r a o)) =
      some (cfg .alphabet none suffix (List.replicate n true ++ c) s r
        ((encodeWord n).reverse ++ a) o) := by
…
  34. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.countStep_true line 273
  35. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.countStep_false line 279
  36. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.countTrace line 286

    Source documentation

    Copy the occurrence count while also storing its physical unary counter.

    theorem countTrace {q : Nat} (n : Nat) (suffix c s r a o : List Bool)
    (register : Option Bool) :
    (advance (TM2.step (program q)))^[n + 1]
      (some (cfg .count register (encodeWord n ++ suffix) c s r a o)) =
      some (cfg .guard none suffix c s (List.replicate n true ++ r)
        ((encodeWord n).reverse ++ a) o) := by
…
  37. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.initial_configuration line 303
  38. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.initialStep line 310
  39. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitHeader.headerTrace line 319

    Source documentation

    Read 2*C,q,m, write C,q,m, and leave the physical unary capacity and occurrence counters ready for the row loop. The bound counts real transitions.

    theorem headerTrace (q C m : Nat) (suffix : List Bool) :
    (advance (TM2.step (program q)))^[2 * C + q + m + 4]
      (some (initList (machine q)
        (encodeWord (2 * C) ++ encodeWord q ++ encodeWord m ++ suffix))) =
      some (cfg .guard none suffix (encodeWord C) [] (encodeWord m)
        (encodeWords [C, q, m]).reverse []) := by
…
  40. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitSubtract.subtractStep_zero line 363
  41. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitSubtract.subtractStep_succ line 371
  42. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitSubtract.subtractTrace line 382

    Source documentation

    The scan consumes precisely the capacity prefix of the target field.

    theorem subtractTrace (q n : Nat)
    (suffix saved remaining accumulator output : List Bool) (register : Option Bool) :
    (advance (TM2.step (program q)))^[n + 1]
      (some (cfg .subtract register (List.replicate n true ++ suffix)
        (encodeWord n) saved remaining accumulator output)) =
      some (cfg .restore none suffix (encodeWord 0)
        (List.replicate n true ++ saved) remaining accumulator output) := by
…
  43. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitSubtract.restore_tapes line 397
  44. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitSubtract.restoreTrace line 405

    Source documentation

    The real saved-prefix transfer restores C, empties scratch, and takes C + 1 transitions.

    theorem restoreTrace (q n : Nat) (suffix remaining accumulator output : List Bool) :
    (advance (TM2.step (program q)))^[n + 1]
      (some (cfg .restore none suffix (encodeWord 0) (List.replicate n true)
        remaining accumulator output)) =
      some (cfg .target none suffix (encodeWord n) [] remaining accumulator output) := by
…
  45. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitSubtract.removeOffsetTrace line 424

    Source documentation

    The complete target-offset removal preserves every other tape. In particular the capacity is reusable and the v field delimiter is untouched.

    theorem removeOffsetTrace (q C v : Nat) (suffix remaining accumulator output : List Bool)
    (register : Option Bool) :
    (advance (TM2.step (program q)))^[2 * (C + 1)]
      (some (cfg .subtract register (encodeWord (C + v) ++ suffix)
        (encodeWord C) [] remaining accumulator output)) =
      some (cfg .target none (encodeWord v ++ suffix) (encodeWord C)
        [] remaining accumulator output) := by
…
  46. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.joinTrace line 449
  47. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.rowCost line 453
  48. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.rowTrace line 456
  49. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.guardStep_succ line 492
  50. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.guardStep_zero line 500
  51. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.rowsCost line 508
  52. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.rowsCost_cons line 511
  53. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.rowsTrace line 519

    Source documentation

    The actual counted loop visits every row once and preserves its order. No complete-loop execution is supplied as an input hypothesis.

    theorem rowsTrace {C q : Nat} (cs : List (Constraint C q))
    (suffix accumulator output : List Bool) (register : Option Bool) :
    (advance (TM2.step (program q)))^[rowsCost cs]
      (some (cfg .guard register (doubledRowsBits cs ++ suffix)
        (encodeWord C) [] (encodeWord cs.length) accumulator output)) =
      some (cfg .finishStart none suffix (encodeWord C) [] (encodeWord 0)
        ((rowsBits cs).reverse ++ accumulator) output) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRows.rowsCost