OAI/Computability/MaxCut/Machines/MachineRegularTableRuntime.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

A fixed five-tape machine physically copies a graph table, preserves the original input, and splits its two unary header fields from the copied rows. The exact trace is ambient-state polymorphic for static machine placement.

  1. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.rawProgram line 14
  2. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.sourceMachine_eq line 22
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.cleanupTapes line 26
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.cleanup_complete line 29
  5. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.terminalRun line 33
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime line 53

    Source documentation

    The literal canonical output configuration computes the shared regular preprocessing map, with the actual complete raw execution as its witness.

    noncomputable def computableInPolyTime (H : PreprocessingRegularTables.BaseTable) :
    TM2ComputableInPolyTime GraphTables.tableBits
      (PortTables.inputBits (ports := PreprocessingRegularTables.internalDegree + 1))
…
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.finite_alphabet line 62

    Source documentation

    Finiteness refers to the exact machine in the preceding certificate.

    theorem finite_alphabet (H : PreprocessingRegularTables.BaseTable) :
    ∀ k, Finite ((computableInPolyTime H).tm.Γ k) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime

  8. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Tape line 80
  9. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.State line 81
  10. inductive OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Label line 83
  11. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Label.enumList line 87
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Label.enumList_getElem?_ctorIdx_eq line 90
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Label.enumList_nodup line 94
  14. instance OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.(instance at line 96) line 96
  15. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.tapes line 102

    Source documentation

    Tape 0 is protected input, 1 is the working row stream, 2 is scratch, and 3 and 4 hold the extracted vertex and dart counts.

    def tapes (original work vertices darts : List Bool) : Tape → List Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Tape

  16. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.initialTapes line 106
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.resultTapes line 108
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.resultTapes_original line 111
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.resultTapes_work line 115
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.resultTapes_scratch line 118
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.resultTapes_vertices line 121
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.resultTapes_darts line 124
  23. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.program line 128

    Source documentation

    Six finite control labels, independent of all input sizes and contents.

    def program {σ : Type} : Label → TM2.Stmt (fun _ : Tape => Bool) Label (State σ)
  | .copyFirst => Reduction.MachineTransfer.loopAt 0 2 id false .copyFirst (some .copySecond)
  | .copySecond => MachineCopy.forkLoop 2 0 1 false .copySecond (some .startVertices)
  | .startVertices => Hastad.SourceMachine.fieldStart 3 .readVertices
  | .readVertices => Hastad.SourceMachine.fieldLoop 1 3 .readVertices (some .startDarts)
  | .startDarts => Hastad.SourceMachine.fieldStart 4 .readDarts
  | .readDarts => Hastad.SourceMachine.fieldLoop 1 4 .readDarts none

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Label, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.State, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop, OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldStart, OAI.MaxCutGames.Foundations.Hastad.SourceMachine.fieldLoop

  24. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.exactSteps line 136
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.splitTrace line 139
  26. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.timePolynomial line 209
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.timePolynomial_eval line 211
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.exactSteps_le line 214
  29. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.splitInTime line 221
  30. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.machine line 231
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.initial_configuration line 242
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.rowsBits line 251
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.tableBits_header_rows line 254
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.tableTrace line 258
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.initializedTableInTime line 268

    Source documentation

    The concrete machine starts at its genuine initial configuration on a full graph table and leaves every output field on the stated physical tape.

    def initializedTableInTime (table : PCP.GraphTables.Table) :
    StateTransition.EvalsToInTime machine.step (initList machine (PCP.GraphTables.tableBits table))
      (some ⟨none, ((), none), resultTapes table.vertices table.darts (rowsBits table)⟩)
      (timePolynomial.eval (PCP.GraphTables.tableBits table).length) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.machine, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.resultTapes, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.rowsBits

  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowsBits_length_le line 284

    Source documentation

    All rows in a fixed block are bounded by its last possible index.

    theorem rowsBits_length_le (v e count : Nat) :
    (MachineDummyRows.rowsBits v e count).length ≤ count * (v + e + count + 8194) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits

  37. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowBound line 300

    Source documentation

    A common row-size bound for all remaining vertices and ports.

    def rowBound (d v e count : Nat) : Nat := v + count + e + (count + 1) * d + 8194
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowBound_next line 304

    Source documentation

    This bound is invariant when one vertex and its d reverse indices have been consumed from the remaining outer-loop count.

    theorem rowBound_next (d v e count : Nat) :
    rowBound d (v + 1) (e + d) count = rowBound d v e (count + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowBound

  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.blockRow_le_rowBound line 309
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.steps_le_bound line 316

    Source documentation

    The actual outer-loop cost is bounded by the number of vertices times a uniform bound on its actual row bodies and two control transitions.

    theorem steps_le_bound (d v e : Nat) (output : List Bool) (count : Nat) :
    MachinePaddingRows.steps d v e output count ≤
      count * (d * (4 * rowBound d v e count +
        2 * (output.length + count * d * rowBound d v e count) + 10) + 2) + 1 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.steps, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowBound

  41. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.inputSize line 367

    Source documentation

    Exact variable-size input: two unary fields, unary fuel, and old output.

    def inputSize (v e count : Nat) (output : List Bool) : Nat :=
…
  42. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowCap line 370
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowBound_le_cap line 372
  44. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.rowPolynomial line 385
  45. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial line 390

    Source documentation

    A cubic polynomial for fixed degree, including the final zero-fuel guard. The one-time relation initializer can be accounted for separately.

    noncomputable def timePolynomial (d : Nat) : Polynomial Nat :=
…
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial_bounds line 396
  47. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingCertificate.timePolynomial line 427
  48. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingCertificate.execution line 430
  49. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingTable.initialOutput line 455
  50. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingTable.execution line 458
  51. inductive OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.Tape line 497
  52. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList line 502
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList_getElem?_ctorIdx_eq line 505
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList_nodup line 509
  55. instance OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.(instance at line 511) line 511
  56. inductive OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.Label line 515
  57. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.Alphabet line 524
  58. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.State line 525
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.memory line 528

    Source documentation

    All unnamed work stacks are empty at the phase boundaries below.

    def memory (input output vertex edge power level fuel relation : List Bool) : Tape → List Bool
  | .original => input
  | .output => output
  | .vertex => vertex
  | .edge => edge
  | .power => power
  | .level => level
  | .fuel => fuel
  | .relation => relation
  | _ => []

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.Tape

  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.update_output line 539
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.update_vertex line 542
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.update_edge line 545
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.update_power line 548
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.update_fuel line 551
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.update_relation line 554
  66. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.splitTape line 558
  67. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.splitView line 559
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.splitView_left line 567
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.splitView_right line 569
  70. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.powerTape line 573
  71. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.powerView line 582
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.powerView_left line 593
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.powerView_right line 595
  74. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.subtractTape line 599
  75. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.subtractView line 610
  76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.subtractView_left line 623
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.subtractView_right line 625
  78. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowTape line 629
  79. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowView line 632
  80. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowView_left line 642
  81. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowView_right line 646
  82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowAlphabet_eq line 652
  83. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowStateEquiv line 655
  84. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowProgram line 661
  85. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.program line 668
  86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.appendTrace_inline_MachineVertexPadding line 694
  87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.tableBits_split line 698
  88. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.splitInitialTapes line 704
  89. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.splitResultTapes line 710
  90. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.splitTrace line 716
  91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.powerTapes line 733
  92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.powerTrace line 738
  93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.affineTapes line 752
  94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.affineOutputTrace line 759
  95. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.headersTrace line 801
  96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.copyPowerTrace line 817
  97. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.subtractTapes line 831
  98. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.subtractTrace line 838
  99. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowBoolTapes line 853
  100. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.transport_tapes_apply_inline_MachineVertexPadding line 858
  101. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowCastTapes line 865
  102. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowInitialTapes line 871
  103. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowFinalTapes line 878
  104. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowTime line 886
  105. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.frameTrace_inline_MachineVertexPadding line 889
  106. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowsTrace line 900

    Source documentation

    The checked padding-row machine is transported through alphabet/state equalities and a static tape placement. No row execution is assumed.

    theorem rowsTrace {σ : Type} {n d m : Nat} (hd : 0 < d) (t : PortTables.Table n d)
    (hnm : n ≤ m) (input power level : List Bool) (ambient : σ) :
    (advance (TM2.step (program d hd)))^[rowTime (m := m) t]
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.program, OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rowTime

  107. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.cleanupTime line 934
  108. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.cleanupTrace line 936
  109. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.otherTime line 971
  110. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.totalTime line 978
  111. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingTrace line 983

    Source documentation

    The whole table transformation begins with only its original encoding. Every row-emitter counter and the updated prefix are produced by this run.

    theorem vertexPaddingTrace {σ : Type} {n d : Nat} (hd : 0 < d) (t : PortTables.Table n d)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program d hd)))^[totalTime t]
      (some ⟨some (.splitCode .copyFirst), ((ambient, false), register),
        memory (PortTables.tableBits t) [] [] [] [] [] [] []⟩) =
      some ⟨none, ((ambient, false), none),
        memory (PortTables.tableBits t)
          (PortTables.tableBits (PreprocessingPaddingTables.pad t (PreprocessingLevels.le_paddedSize n)))
          [] [] [] (encodeWord (PreprocessingLevels.boundedLevel n)) [] []⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.program, OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  112. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.rows_length_le line 1019
  113. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.darts_length_le line 1024
  114. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.power_length_bound line 1028
  115. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.initialOutput_length line 1033
  116. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.intermediateCoefficient line 1040
  117. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.intermediatePolynomial line 1042
  118. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.intermediate_bound line 1045
  119. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.otherPolynomial line 1060
  120. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.otherTime_le line 1064
  121. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.timePolynomial line 1080
  122. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.totalTime_le line 1083
  123. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingInTime line 1096

    Source documentation

    Complete runtime certificate from the original input alone, with an explicit clean final frame and an actual polynomial in its encoded length.

    def vertexPaddingInTime {σ : Type} {n d : Nat} (hd : 0 < d) (t : PortTables.Table n d)
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program d hd))
      ⟨some (.splitCode .copyFirst), ((ambient, false), register),
        memory (PortTables.tableBits t) [] [] [] [] [] [] []⟩
      (some ⟨none, ((ambient, false), none),
        memory (PortTables.tableBits t)
          (PortTables.tableBits (PreprocessingPaddingTables.pad t (PreprocessingLevels.le_paddedSize n)))
          [] [] [] (encodeWord (PreprocessingLevels.boundedLevel n)) [] []⟩)
      ((timePolynomial d).eval (PortTables.tableBits t).length) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.program, OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.timePolynomial

  124. def OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.machine line 1110
  125. theorem OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.alphabet_finite line 1121