OAI/Computability/MaxCut/Machines/MachineLazyTableRuntime.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

Canonical polynomial-time computation of the executable lazy preprocessing map. The raw machine's retained original input is physically drained by the checked canonical-output wrapper before it reaches the standard haltList endpoint.

  1. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.rawProgram line 17
  2. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.sourceMachine_eq line 25
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.cleanupTapes line 30

    Source documentation

    A fixed explicit list of every non-output tape, independent of input data.

    def cleanupTapes : List Tape :=
…
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.cleanup_complete line 34
  5. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.terminalRun line 40

    Source documentation

    The terminal witness is the checked full lazy-table execution. The wrapper then drains the retained original input rather than assuming it disappeared.

    def terminalRun (d : Nat) (positive : 0 < d) (a : PortTables.Input d) :
    MachineCanonicalOutput.TerminalRun (rawProgram d positive) (PortTables.inputBits a)
      (PortTables.inputBits (PreprocessingStageMaps.lazy d a))
      ((MachineLazyTable.timePolynomial d).eval (PortTables.inputBits a).length) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.rawProgram, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.timePolynomial

  6. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.computableInPolyTime line 52

    Source documentation

    The actual canonical-output finite machine computes precisely the shared degree-d to degree-2d stage map in polynomial time.

    noncomputable def computableInPolyTime (d : Nat) (positive : 0 < d) :
    TM2ComputableInPolyTime (PortTables.inputBits (ports := d))
…
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTableRuntime.finite_alphabet line 60

    Source documentation

    Every tape alphabet of this exact completed computation certificate is finite.

    theorem finite_alphabet (d : Nat) (positive : 0 < d) :
    ∀ k, Finite ((computableInPolyTime d positive).tm.Γ k) :=
…

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

  8. def OAI.MaxCutGames.Foundations.PCP.PreprocessingFinishRuntime.finish line 76
  9. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFinishRuntime.output_eq_finish line 81
  10. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFinishRuntime.finish_degree_positive line 85
  11. def OAI.MaxCutGames.Foundations.PCP.PreprocessingFinishRuntime.computableInPolyTime line 90

    Source documentation

    Both stages supply complete executions, cleanup, and polynomial bounds; the sequential composition includes the physical interstage bit transfer.

    noncomputable def computableInPolyTime (H : PreprocessingTables.BaseTable)
    (d : Nat) (hd : 0 < d) :
    TM2ComputableInPolyTime (PortTables.inputBits (ports := d))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.PortTables.inputBits

  12. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFinishRuntime.finite_alphabet line 101
  13. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRuntime.tablePolynomialTime line 119
  14. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRuntime.finiteAlphabet line 132
  15. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.bitLength line 155
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.bitLength_zero line 157
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.bitLength_positive line 159
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.bitLength_half line 162
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.increments line 169
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.increments_true line 172
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.increments_half line 175
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.increments_false line 179
  23. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.coreTime line 184
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.coreTime_zero line 189
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.coreTime_positive line 191
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.coreTime_bound line 195
  27. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.Alphabet line 205
  28. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.State line 206
  29. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.initialState line 208
  30. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.rawTapes line 210
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.update_input_inline_MachineLogCounter line 215
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.update_scratch_inline_MachineLogCounter line 220
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.update_output_inline_MachineLogCounter line 225
  34. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.stripLoop line 230
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.guardLoop line 236
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.halfLoop line 245
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.program line 254
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.machine line 261
  39. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.configuration line 272
  40. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.next line 276
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.stripStep_true line 278
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.stripStep_false line 286
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.stripTrace line 294
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.halfStep_nil line 310
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.halfStep_false line 318
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.halfStep_true line 327
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.halfTrace line 337

    Source documentation

    A parity bit implements division by two using actual pop/push transitions.

    theorem halfTrace (n m : Nat) (output : List Bool) (parity started : Bool)
    (register : Option Bool) :
    next^[n + 1] (some (configuration (some 3) ((parity, started), register)
      (List.replicate n true) (List.replicate m true) output)) =
      some (configuration (some 4) ((false, started), none) []
        (List.replicate (m + (n + if parity then 1 else 0) / 2) true) output) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.next, OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.configuration

  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.restoreTrace line 369
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.guardStep_zero line 386
  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.guardStep_positive line 394
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.coreTrace line 407

    Source documentation

    The halving rounds are actual guard, scan, and restoration executions.

    theorem coreTrace (n : Nat) (output : List Bool) (started : Bool) :
    next^[coreTime n] (some (configuration (some 2) ((false, started), none)
      (List.replicate n true) [] output)) =
      some (configuration none initialState [] []
        (List.replicate (increments n started) true ++ output)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.next, OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.coreTime, OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.configuration, OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.initialState, OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.increments

  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.initList_eq line 439
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.haltList_eq line 448
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.initialStep line 456
  55. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.totalTime line 465
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.totalTime_bound line 467
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.machineTrace line 472
  58. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.outputsInTime line 487
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.computableInPolyTime line 495

    Source documentation

    A genuine finite-machine certificate for unary log2(n)+1; its linear polynomial is measured in the actual encoded input length.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime encodeWord encodeWord (fun n => n.log2 + 1) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord

  60. inductive OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraTape line 526
  61. abbrev OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList line 530
  62. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_getElem?_ctorIdx_eq line 532
  63. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_nodup line 536
  64. instance OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.(instance at line 538) line 538
  65. inductive OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel line 542
  66. abbrev OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList line 547
  67. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_getElem?_ctorIdx_eq line 550
  68. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_nodup line 554
  69. instance OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.(instance at line 556) line 556
  70. abbrev OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.Tape line 560
  71. abbrev OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.Label line 561
  72. abbrev OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.Alphabet line 562
  73. abbrev OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.State line 563
  74. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.initialState line 565
  75. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockLabel line 567
  76. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockStatement line 572

    Source documentation

    Homogeneous Boolean embedding of the fixed logarithm program.

    def clockStatement : TM2.Stmt MachineLogCounter.Alphabet (Fin 5) MachineLogCounter.State →
    TM2.Stmt Alphabet Label State
  | .push k f next => .push (.inl k) (fun state => f state.1) (clockStatement next)
  | .peek k f next => .peek (.inl k) (fun state x => (f state.1 x, state.2)) (clockStatement next)
  | .pop k f next => .pop (.inl k) (fun state x => (f state.1 x, state.2)) (clockStatement next)
  | .load f next => .load (fun state => (f state.1, state.2)) (clockStatement next)
  | .branch f yes no => .branch (fun state => f state.1) (clockStatement yes) (clockStatement no)
  | .goto f => .goto (fun state => .inl (f state.1))
  | .halt => .goto (fun _ => .inr .clearInput)

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.State, OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.Alphabet, OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.Label, OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.State

  77. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.readHeader line 582
  78. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.program line 588
  79. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.machine line 606
  80. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockTapes line 617
  81. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockConfiguration line 621
  82. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockTapes_update line 625
  83. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockStatement_simulation line 632
  84. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockStep line 657
  85. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockInTime line 672
  86. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.startExtra line 689
  87. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.startMemory line 694
  88. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.startMemory_input_update line 698
  89. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.startMemory_sum_update line 706
  90. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.headerStep_zero line 714
  91. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.headerStep_succ line 728
  92. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.headerTrace line 745
  93. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.headerInTime line 762
  94. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.initialMemory line 774
  95. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockInitialMemory line 786
  96. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.startInTime line 800

    Source documentation

    Exact handoff from the genuine machine input to the actual logarithm machine, with the original graph word protected in the archive.

    def startInTime (n m : Nat) (rest : List Bool) :
    StateTransition.EvalsToInTime machine.step
      (initList machine (encodeWords [n, m] ++ rest))
      (some (clockConfiguration (startExtra rest (encodeWords [n, m] ++ rest)) none
        (initList MachineLogCounter.machine (encodeWord (n + m)))))
      (2 * ((encodeWords [n, m] ++ rest).length + 1) + 1 + (n + 1) + (m + 1)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.machine, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.clockConfiguration, OAI.MaxCutGames.Foundations.Complexity.GraphCounterModel.startExtra, OAI.MaxCutGames.Foundations.Complexity.MachineLogCounter.machine, OAI.MaxCutGames.Foundations.Complexity.encodeWord