OAI/Computability/MaxCut/Machines/MachineSingleOrbitProgram.lean

GitHub source file

84 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.MaxCutGames.Explicit.MachineSingleOrbitProgram.Tape line 20
  2. abbrev OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.Tape.enumList line 24
  3. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.Tape.enumList_getElem?_ctorIdx_eq line 27
  4. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.Tape.enumList_nodup line 31
  5. instance OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.(instance at line 33) line 33
  6. abbrev OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.State line 37
  7. def OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.initialState line 39
  8. def OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.clearKeys line 41
  9. inductive OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.Label line 43
  10. def OAI.MaxCutGames.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.MaxCutGames.Explicit.MachineSingleOrbitProgram.Label, OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.Tape, OAI.MaxCutGames.Explicit.MachineSingleOrbitProgram.State

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

  29. theorem OAI.MaxCutGames.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.MaxCutGames.Explicit.MachineSingleOrbitStreams.cfg

  30. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitHeader.halfStep_first line 233
  31. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitHeader.halfStep_second line 239
  32. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitHeader.halfStep_false line 245
  33. theorem OAI.MaxCutGames.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.MaxCutGames.Explicit.MachineSingleOrbitHeader.countStep_true line 273
  35. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitHeader.countStep_false line 279
  36. theorem OAI.MaxCutGames.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.MaxCutGames.Explicit.MachineSingleOrbitHeader.initial_configuration line 303
  38. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitHeader.initialStep line 310
  39. theorem OAI.MaxCutGames.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.MaxCutGames.Explicit.MachineSingleOrbitSubtract.subtractStep_zero line 365
  41. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitSubtract.subtractStep_succ line 373
  42. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitSubtract.subtractTrace line 384

    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.MaxCutGames.Explicit.MachineSingleOrbitSubtract.restore_tapes line 399
  44. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitSubtract.restoreTrace line 407

    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.MaxCutGames.Explicit.MachineSingleOrbitSubtract.removeOffsetTrace line 426

    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. def OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubleConstraint line 451
  47. def OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubleInstance line 456
  48. def OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.rowBits line 461
  49. def OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubledRowBits line 464
  50. def OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.rowsBits line 467
  51. def OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubledRowsBits line 470
  52. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.rowBits_eq line 473
  53. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubledRowBits_eq line 478
  54. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.rowsBits_nil line 483
  55. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubledRowsBits_nil line 484
  56. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.rowsBits_cons line 487
  57. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubledRowsBits_cons line 491
  58. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.gameBits_eq line 496
  59. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.doubled_gameBits_eq line 501
  60. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.input_length_eq line 507
  61. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.vertices_le_input_length line 515
  62. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitCodec.rows_le_input_length line 520
  63. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.joinTrace line 535
  64. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.rowCost line 539
  65. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.rowTrace line 542
  66. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.guardStep_succ line 578
  67. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.guardStep_zero line 586
  68. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.rowsCost line 594
  69. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.rowsCost_cons line 597
  70. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRows.rowsTrace line 605

    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.MaxCutGames.Explicit.MachineSingleOrbitRows.rowsCost

  71. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitFinish.haltList_eq line 647
  72. def OAI.MaxCutGames.Explicit.MachineSingleOrbitFinish.finishStartInTime line 654
  73. def OAI.MaxCutGames.Explicit.MachineSingleOrbitFinish.timePolynomial line 662
  74. def OAI.MaxCutGames.Explicit.MachineSingleOrbitFinish.completePrefix line 667

    Source documentation

    This helper consumes a proved prefix trace. The final runtime theorem supplies that trace from the concrete header and complete row traversal.

    def completePrefix (q : Nat) (input : List Bool) (prefixTime : Polynomial Nat)
    (base : Tape → List Bool)
    (execution : StateTransition.EvalsToInTime (machine q).step
      (initList (machine q) input)
      (some ⟨some .finishStart, initialState, base⟩) (prefixTime.eval input.length))
    (outputEmpty : base .output = []) :
    TM2OutputsInTime (machine q) input (some (base .accumulator).reverse)
      ((timePolynomial q prefixTime).eval input.length) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSingleOrbitFinish.timePolynomial

  75. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.finalTapes line 715
  76. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.prefixCost line 718
  77. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.prefixTrace line 722

    Source documentation

    The complete prefix is obtained from the actual header and row traces.

    theorem prefixTrace {q : Nat} (I : Instance q) :
    (advance (TM2.step (program q)))^[prefixCost I]
      (some (initList (machine q) (gameBits (doubleInstance I)))) =
      some ⟨some .finishStart, initialState, finalTapes I⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.prefixCost, OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.finalTapes

  78. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.prefixPolynomial line 750
  79. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.prefixCost_le line 753
  80. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.prefixInTime line 762
  81. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.timePolynomial line 771
  82. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.fullRunInTime line 775

    Source documentation

    Literal init-to-halt execution, with every non-output tape empty at halt.

    def fullRunInTime {q : Nat} (I : Instance q) :
    TM2OutputsInTime (machine q) (gameBits (doubleInstance I))
      (some (gameBits I)) ((timePolynomial q).eval (gameBits (doubleInstance I)).length) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.timePolynomial

  83. def OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.computableInPolyTime line 784

    Source documentation

    A proved polynomial-time codec conversion, without an assumed time bound, an output-size certificate, or an unbounded integer in finite machine state.

    def computableInPolyTime (q : Nat) :
    TM2ComputableInPolyTime (fun I : Instance q => gameBits (doubleInstance I)) gameBits id where
…
  84. theorem OAI.MaxCutGames.Explicit.MachineSingleOrbitRuntime.workAlphabetFinite line 799