OAI/Computability/MaxCut/Machines/MachineExpanderRowFrames.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

Concrete data and tape frames for an actual expander-row computation

Only the five actual row inputs are stored. Every address, table return and finite control value below is computed from those inputs. The thirteen tape frames use the existing phase-output functions. These are data identities and size bounds, not assumed machine executions.

  1. structure OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData line 19
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.rowData line 26
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.control0 line 34
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstRow line 35
  5. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue line 36
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstPair line 37
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex line 38
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn line 39
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.control1 line 40
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondRow line 41
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue line 42
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondPair line 43
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex line 44
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn line 45
  15. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.control2 line 46
  16. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.query1 line 47
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.query2 line 48
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue line 49
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.tableLength line 50
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_eq_firstRow line 52
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_eq_secondRow line 55
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_div_degree line 58
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_mod_degree line 59
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_div_degree line 60
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_mod_degree line 61
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_eq_residue line 63
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_eq_residue line 67
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveFirst_residue_eq_control1 line 71
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveSecond_residue_eq_control2 line 77
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstSelected line 83
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondSelected line 87
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.evaluateRow_eq line 91
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue_eq_step_reverseIndex line 94
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.rows_le_tableLength line 101
  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_le_tableLength line 105
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_le_tableLength line 109
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_le_tableLength line 113
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_le_tableLength line 116
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.inputVertex_le_tableLength line 119
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex_le_tableLength line 124
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex_le_tableLength line 128
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_le_tableLength line 132
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_le_tableLength line 136
  44. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frameContents line 145

    Source documentation

    Complete explicit tape contents; all three scratch roles omitted here are empty.

    def frameContents (r : RowData v d) (output : List Bool)
    (qr qi lo q1 q2 r1 r2 : List Bool) : Tape → List Bool
  | .inputVertex => encodeWord r.inputVertex.val
  | .table => encodeWords (rotationWords r.oldTable)
  | .output => output
  | .queryReverse => qr
  | .queryIndex => qi
  | .lookupOutput => lo
  | .quotientFirst => q1
  | .quotientSecond => q2
  | .remainderFirst => r1
  | .remainderSecond => r2
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  45. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame0 line 159
  46. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame1 line 161
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame2 line 163
  48. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame3 line 165
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame4 line 168
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame5 line 170
  51. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame6 line 172
  52. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame7 line 174
  53. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame8 line 176
  54. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame9 line 179
  55. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame10 line 181
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame11 line 183
  57. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame12 line 185
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_id_eq_inline_MachineExpanderRowFrames line 188
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame1_eq line 196
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame2_eq line 202
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame3_eq line 208
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame4_eq line 214
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame5_eq line 220
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame6_eq line 228
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame7_eq line 234
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame8_eq line 241
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame9_eq line 248
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame10_eq line 255
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame11_eq line 263
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame12_eq line 271
  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.final_frame_eq line 277
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame0_inputVertex line 284
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame0_table line 287
  74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame0_output line 290
  75. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame1_inputVertex line 293
  76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame1_emitScratch line 296
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame2_queryReverse line 299
  78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame2_queryIndex line 302
  79. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame3_table line 305
  80. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupRestore line 308
  81. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupWork line 311
  82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupOutput line 314
  83. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame3_queryIndex line 317
  84. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame4_lookupOutput line 320
  85. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame4_quotientFirst line 323
  86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame4_remainderFirst line 326
  87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame6_quotientFirst line 329
  88. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame6_emitScratch line 332
  89. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame7_queryReverse line 335
  90. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame7_queryIndex line 338
  91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame8_table line 341
  92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupRestore line 344
  93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupWork line 347
  94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupOutput line 350
  95. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame8_queryIndex line 353
  96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame9_lookupOutput line 356
  97. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame9_quotientSecond line 359
  98. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame9_remainderSecond line 362
  99. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame10_quotientSecond line 365
  100. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame10_emitScratch line 368
  101. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame10_output line 371
  102. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.final_dirty_word_length_le line 374
  103. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_le_tableLength line 382
  104. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.concatenate_inline_MachineExpanderRow line 407
  105. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.rowSteps line 412

    Source documentation

    The actual number of transitions, retaining both concrete lookup costs.

    def rowSteps {v d : Nat} (r : RowData v d) (output : List Bool) : Nat :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData

  106. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.rowTraceAt line 432

    Source documentation

    The complete execution follows the concrete program. The only code premise places its instructions in a caller; every lookup is derived from oldTable.

    theorem rowTraceAt :
    (advance (TM2.step target))^[rowSteps r output]
      (some ⟨some (labels .initialize), divisionState positive ambient r.control0 none,
        frame0 r output⟩) =
      some ⟨exit, divisionState positive ambient r.control2 none,
        emittedWord .output (frame0 r output) r.finalValue⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.rowSteps, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame0, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emittedWord

  107. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.rowSteps_le line 556
  108. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.rowInTimeAt line 576

    Source documentation

    The actual row program has a linear transition bound, with all temporary tapes empty at return. The bound holds for every valid finite input table.

    def rowInTimeAt {v d : Nat} {ρ Λ : Type} [Fintype ρ]
    (positive : 0 < d) (r : RowData v d) (output : List Bool) (ambient : ρ)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : Tape => Bool) Λ (State ρ d))
    (code : ∀ l, target (labels l) = statement positive r.smallTable id labels exit l) :
    StateTransition.EvalsToInTime (TM2.step target)
      ⟨some (labels .initialize), divisionState positive ambient r.control0 none,
        frame0 r output⟩
      (some ⟨exit, divisionState positive ambient r.control2 none,
        emittedWord .output (frame0 r output) r.finalValue⟩)
      (80 * (r.tableLength + 1)) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.statement, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame0, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emittedWord

  109. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.rowInTime line 592

    Source documentation

    Specialization to the standalone finite row program.

    def rowInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (r : RowData v d) (output : List Bool) (ambient : ρ) :
    StateTransition.EvalsToInTime (TM2.step (program positive r.smallTable))
      ⟨some .initialize, divisionState positive ambient r.control0 none, frame0 r output⟩
      (some ⟨none, divisionState positive ambient r.control2 none,
        emittedWord .output (frame0 r output) r.finalValue⟩)
      (80 * (r.tableLength + 1)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.RowData, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.divisionState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.frame0, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.emittedWord

  110. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller_boundaryState line 618
  111. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.prepareState_boundaryState line 622
  112. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_boundaryState line 627
  113. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller_prepareState line 632
  114. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller_resetState line 635
  115. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller_clearRegister line 638
  116. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller_advancePositionState line 641
  117. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller_resetPositionState line 644
  118. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.nextPosition_val_of_lt line 647
  119. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_update_count line 652

    Source documentation

    Replacing the count word leaves the entire row frame and result unchanged.

    theorem boundaryTapes_update_count (vertex remaining next : Nat)
    (oldTable output countSuffix result : List Bool) :
    Function.update (boundaryTapes vertex remaining oldTable output countSuffix result)
      (.inr .vertexCount) (encodeWord next ++ countSuffix) =
      boundaryTapes vertex next oldTable output countSuffix result := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  120. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_increment_vertex line 663

    Source documentation

    The last row's one actual push increments the unary vertex word.

    theorem boundaryTapes_increment_vertex (vertex remaining : Nat)
    (oldTable output countSuffix result : List Bool) :
    Function.update (boundaryTapes vertex remaining oldTable output countSuffix result)
      (.inl .inputVertex) (true :: encodeWord vertex) =
      boundaryTapes (vertex + 1) remaining oldTable output countSuffix result := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  121. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.initialTapes_initialize line 676
  122. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.initializeStep line 690
  123. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.initialize_boundaryStep line 699
  124. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_succStep line 715

    Source documentation

    A positive vertex counter is physically decremented; its suffix remains.

    theorem vertexGuard_succStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (remaining : Nat) (suffix : List Bool)
    (counter : base (.inr .vertexCount) = encodeWord (remaining + 1) ++ suffix) :
    TM2.step (program positive H) ⟨some (.inr .vertexGuard), state, base⟩ =
      some ⟨some (.inr .prepareRow), clearRegister state,
        Function.update base (.inr .vertexCount) (encodeWord remaining ++ suffix)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister

  125. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_zeroStep line 728

    Source documentation

    The zero delimiter is retained when the loop enters output reversal.

    theorem vertexGuard_zeroStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (suffix : List Bool)
    (counter : base (.inr .vertexCount) = encodeWord 0 ++ suffix) :
    TM2.step (program positive H) ⟨some (.inr .vertexGuard), state, base⟩ =
      some ⟨some (.inr .reverseOutput), clearRegister state, base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister

  126. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_succStep line 739
  127. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_zeroStep line 752
  128. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.prepareRowStep line 763

    Source documentation

    Preparing a row modifies finite control only, preserving every tape.

    theorem prepareRowStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d) :
    TM2.step (program positive H) ⟨some (.inr .prepareRow), state, base⟩ =
      some ⟨some (.inl .initialize), prepareState positive H state, base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.prepareState

  129. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.afterRow_moreStep line 772

    Source documentation

    A nonfinal row advances the finite position without changing tapes.

    theorem afterRow_moreStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (more : state.2.val + 1 < rowFactor d) :
    TM2.step (program positive H) ⟨some (.inr .afterRow), state, base⟩ =
      some ⟨some (.inr .prepareRow), advancePositionState positive state, base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.advancePositionState

  130. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.afterRow_lastStep line 782

    Source documentation

    The final row increments the tape vertex and resets the finite position.

    theorem afterRow_lastStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (last : ¬ state.2.val + 1 < rowFactor d) :
    TM2.step (program positive H) ⟨some (.inr .afterRow), state, base⟩ =
      some ⟨some (.inr .vertexGuard), resetPositionState positive state,
        Function.update base (.inl .inputVertex) (true :: base (.inl .inputVertex))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.resetPositionState

  131. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.afterRow_last_boundaryStep line 792
  132. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_consStep line 812

    Source documentation

    One reversal step moves an actual symbol and preserves the finite position.

    theorem reverseOutput_consStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (symbol : Bool) (word : List Bool) (source : base (.inl .output) = symbol :: word) :
    TM2.step (program positive H) ⟨some (.inr .reverseOutput), state, base⟩ =
      some ⟨some (.inr .reverseOutput), ((state.1.1, some symbol), state.2),
        Function.update (Function.update base (.inl .output) word)
          (.inr .result) (symbol :: base (.inr .result))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program

  133. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_nilStep line 824
  134. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.doneStep line 836