OAI/Computability/MaxCut/Machines/MachineProductProgram.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Concrete header and initialized work-tape frames for the product machine.

  1. abbrev OAI.MaxCutGames.Explicit.MachineProductProgram.Extra line 15
  2. abbrev OAI.MaxCutGames.Explicit.MachineProductProgram.Tape line 16
  3. abbrev OAI.MaxCutGames.Explicit.MachineProductProgram.State line 17
  4. def OAI.MaxCutGames.Explicit.MachineProductProgram.auxiliary line 19
  5. def OAI.MaxCutGames.Explicit.MachineProductProgram.constantDigit line 20
  6. def OAI.MaxCutGames.Explicit.MachineProductProgram.accumulator line 21
  7. def OAI.MaxCutGames.Explicit.MachineProductProgram.output line 22
  8. def OAI.MaxCutGames.Explicit.MachineProductProgram.rowRole line 24
  9. def OAI.MaxCutGames.Explicit.MachineProductProgram.decodeRow_inline_MachineProductProgram line 34
  10. theorem OAI.MaxCutGames.Explicit.MachineProductProgram.decodeRow_role_inline_MachineProductProgram line 45
  11. def OAI.MaxCutGames.Explicit.MachineProductProgram.rowSlots line 54
  12. def OAI.MaxCutGames.Explicit.MachineProductProgram.powerRole line 61
  13. theorem OAI.MaxCutGames.Explicit.MachineProductProgram.powerRole_injective line 70
  14. def OAI.MaxCutGames.Explicit.MachineProductProgram.powerSlots line 82
  15. def OAI.MaxCutGames.Explicit.MachineProductProgram.initRole line 85
  16. theorem OAI.MaxCutGames.Explicit.MachineProductProgram.initRole_injective line 91
  17. def OAI.MaxCutGames.Explicit.MachineProductProgram.seedCommands line 95
  18. def OAI.MaxCutGames.Explicit.MachineProductProgram.clearKeys line 98
  19. theorem OAI.MaxCutGames.Explicit.MachineProductProgram.mem_clearKeys line 101
  20. inductive OAI.MaxCutGames.Explicit.MachineProductProgram.Label line 107
  21. def OAI.MaxCutGames.Explicit.MachineProductProgram.headerDestination line 122
  22. def OAI.MaxCutGames.Explicit.MachineProductProgram.rowMain line 127
  23. def OAI.MaxCutGames.Explicit.MachineProductProgram.nextCheck line 130
  24. def OAI.MaxCutGames.Explicit.MachineProductProgram.resetAt line 132
  25. def OAI.MaxCutGames.Explicit.MachineProductProgram.headerNext line 134
  26. def OAI.MaxCutGames.Explicit.MachineProductProgram.program line 137
  27. def OAI.MaxCutGames.Explicit.MachineProductProgram.machine line 163
  28. def OAI.MaxCutGames.Explicit.MachineProductHeaders.frame line 188

    Source documentation

    All permanent input fields and fixed Horner digits are explicit tape words. The argument is the forward-order emitted already emitted.

    def frame {q : Nat} (H : Instance q) (t : Nat) (emitted : List Bool) : Tape t → List Bool
  | .formula => encodeWords (ProductMachineSemantics.inputTable H)
  | .extra (.inl i) =>
      if i = 0 then encodeWord H.vertices
      else if i = 7 then encodeWord q
      else if i = 8 then encodeWord H.constraints.length
      else if i = 6 then emitted.reverse else []
  | .extra (.inr i) => encodeWord (MachineProductPower.digits i.val)
  | _ => []

    Mentions: OAI.MaxCutGames.Explicit.ProductMachineSemantics.inputTable, OAI.MaxCutGames.Explicit.MachineProductPower.digits

  29. def OAI.MaxCutGames.Explicit.MachineProductHeaders.headerBits line 198
  30. def OAI.MaxCutGames.Explicit.MachineProductHeaders.baseTapes line 202

    Source documentation

    Canonical frame before the odometer digits are filled.

    def baseTapes {q : Nat} (H : Instance q) (t : Nat) : Tape t → List Bool :=
…
  31. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.frame_accumulator line 205
  32. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.frame_output line 208
  33. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.frame_radix line 211
  34. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.frame_digit line 217
  35. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.power_outside line 222
  36. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.frame_power_clean line 228
  37. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.frame_power_output line 232
  38. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.frame_append line 236
  39. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.initialized_eq line 249

    Source documentation

    The generic odometer initializer has exactly the scheduler's concrete digit frame; all permanent headers and output-emitted bits retain their identity.

    theorem initialized_eq {q : Nat} (H : Instance q) (t : Nat) :
    MachineOdometerInit.stageTapes (initRole t) H.constraints.length (baseTapes H t) t =
      SourceOdometerSchedule.setDigits H.constraints.length (fun _ : Fin t => 0) (baseTapes H t) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductHeaders.baseTapes

  40. def OAI.MaxCutGames.Explicit.MachineProductHeadersRead.inputTapes line 281
  41. def OAI.MaxCutGames.Explicit.MachineProductHeadersRead.afterVertices line 285
  42. def OAI.MaxCutGames.Explicit.MachineProductHeadersRead.afterAlphabet line 290
  43. def OAI.MaxCutGames.Explicit.MachineProductHeadersRead.rawResultTapes line 295
  44. def OAI.MaxCutGames.Explicit.MachineProductHeadersRead.resultTapes line 301
  45. theorem OAI.MaxCutGames.Explicit.MachineProductHeadersRead.initList_eq line 307
  46. theorem OAI.MaxCutGames.Explicit.MachineProductHeadersRead.first_result line 315
  47. theorem OAI.MaxCutGames.Explicit.MachineProductHeadersRead.second_result line 328
  48. theorem OAI.MaxCutGames.Explicit.MachineProductHeadersRead.third_result line 341
  49. def OAI.MaxCutGames.Explicit.MachineProductHeadersRead.rawHeadersInTime line 354
  50. def OAI.MaxCutGames.Explicit.MachineProductHeadersRead.headersInTime line 393

    Source documentation

    The exact runtime machine starts on the complete ordinary target game codec and reaches the seed phase with its untouched row table and three unary headers.

    def headersInTime {q : Nat} (H : Target.Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some ⟨some .seedStart, (((), ()), none), resultTapes H t⟩)
      (H.vertices + q + H.constraints.length + 6) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineProductHeadersRead.resultTapes

  51. theorem OAI.MaxCutGames.Explicit.MachineProductHeadersRead.headers_budget line 407
  52. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.seedCommands_nodup line 425
  53. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.seed_result line 431
  54. def OAI.MaxCutGames.Explicit.MachineProductHeaders.seedBridge line 459
  55. def OAI.MaxCutGames.Explicit.MachineProductHeaders.seedInTime line 476
  56. def OAI.MaxCutGames.Explicit.MachineProductHeaders.powerExit line 512
  57. def OAI.MaxCutGames.Explicit.MachineProductHeaders.powerInTime line 515
  58. def OAI.MaxCutGames.Explicit.MachineProductHeaders.alphabetInTime line 531
  59. def OAI.MaxCutGames.Explicit.MachineProductHeaders.powersInTime line 542
  60. def OAI.MaxCutGames.Explicit.MachineProductHeaders.initializeInTime line 576
  61. def OAI.MaxCutGames.Explicit.MachineProductHeaders.steps line 590
  62. def OAI.MaxCutGames.Explicit.MachineProductHeaders.prepareInTime line 597

    Source documentation

    Header reading, literal seed setup, actual Horner power computation, and all odometer digits are supplied by real execution traces of the same program.

    def prepareInTime {q : Nat} (H : Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some (SourceOdometerSchedule.initialConfiguration (m := H.constraints.length)
…
  63. def OAI.MaxCutGames.Explicit.MachineProductHeaders.timePolynomial line 613
  64. theorem OAI.MaxCutGames.Explicit.MachineProductHeaders.steps_le line 618
  65. def OAI.MaxCutGames.Explicit.MachineProductHeaders.inPolynomialTime line 634

    Source documentation

    Polynomial initialization in the literal incoming instance-code length.

    def inPolynomialTime {q : Nat} (H : Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some (SourceOdometerSchedule.initialConfiguration (m := H.constraints.length)
…
  66. def OAI.MaxCutGames.Explicit.MachineProductBounds.fieldPolynomial line 655
  67. theorem OAI.MaxCutGames.Explicit.MachineProductBounds.fieldPolynomial_eval line 660
  68. theorem OAI.MaxCutGames.Explicit.MachineProductBounds.field_steps_le line 666
  69. def OAI.MaxCutGames.Explicit.MachineProductBounds.rowCost line 689
  70. theorem OAI.MaxCutGames.Explicit.MachineProductBounds.row_steps_le line 697