OAI/Computability/MaxCut/Machines/PoweringMachineVertex.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Actual variable-size vertex enumeration. The finite guard decrements the live unary counter, a one-step bridge enters the fixed vertex producer, and the producer returns to the guard. Work tapes may change after every vertex.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.Command line 13
  2. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.ports line 15
  3. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.direction line 18
  4. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.commands line 21
  5. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.commands_length line 23
  6. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.LocalLabel line 27
  7. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.SequenceLabel line 28
  8. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.Label line 29
  9. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.State line 30
  10. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceEntry line 32
  11. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.entry line 37
  12. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceInstruction line 40
  13. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.instruction line 49
  14. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.result line 55
  15. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes line 61
  16. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes line 67
  17. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps line 72
  18. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.costSum line 78
  19. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps_eq line 84
  20. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.steps line 97
  21. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.budget line 100
  22. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.costSum_le line 103
  23. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.steps_le line 116
  24. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTrace line 120
  25. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.vertexTrace line 150
  26. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_ready line 168
  27. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_ready line 182
  28. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_other line 191
  29. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_other line 205
  30. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.rowBits line 212
  31. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.blockIndex_eq_encodeDart line 217

    Source documentation

    Decoding a command gives exactly its existing vertex-block row index.

    theorem blockIndex_eq_encodeDart (n : Nat) (vertex : Fin vertices) (j : Command d n) :
    PoweringTableLayout.blockIndex d n vertex j =
      PoweringEnumeration.encodeDart vertices d n (direction j, vertex, ports j) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.Command, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.direction, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.ports

  32. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.rowBits_eq line 225
  33. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.encodeWords_flatMap_inline_PoweringMachineVertex line 232
  34. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.rows_eq_vertexRowBits line 238
  35. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_output line 261
  36. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_output line 281
  37. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.vertexInTime line 292
  38. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.Placement line 322
  39. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.State line 323
  40. structure OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.Ready line 325
  41. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.counter line 333
  42. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.counter_other line 336
  43. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_vertex line 343
  44. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_of_vertex line 362
  45. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexStart line 368
  46. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexEntry line 371
  47. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.bridge line 389
  48. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes line 394

    Source documentation

    The exact tapes produced by repeatedly executing the actual vertex body.

    def finalTapes (graph : PortTables.Table vertices d) (n : Nat) (placement : Placement K n)
    (output : K) : (remaining : Nat) → remaining ≤ vertices → (K → List Bool) → K → List Bool
  | 0, _, base => counter placement base 0
  | r + 1, bounded, base =>
      finalTapes graph n placement output r (by omega)
        (PoweringMachineVertex.finalTapes graph n placement output ⟨r, by omega⟩
          (counter placement base r))

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.Placement, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.counter, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes

  49. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.steps line 402
  50. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.steps_le line 408
  51. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_ready line 420
  52. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows line 445
  53. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_ofFn line 450
  54. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_all line 467
  55. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_output line 474
  56. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_other line 500
  57. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.loopTrace line 512
  58. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineOuterLoop.loopInTime line 578
  59. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Alphabet line 620
  60. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Label line 622
  61. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.copyInstruction line 626
  62. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.instruction line 634

    Source documentation

    The labels contain two fixed affine copies and one fixed list of drains.

    def instruction (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (labels : Label enumeration output → Λ) :
    Label enumeration output → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Alphabet

  63. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.program line 647

    Source documentation

    Actual finite control, independent of both runtime header values.

    def program (enumeration : Fin N ≃ K) (headerV headerD output scratch : K) :
    Label enumeration output →
      TM2.Stmt (Alphabet (K := K)) (Label enumeration output) (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Alphabet

  64. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.afterD line 652
  65. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders line 655
  66. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_output line 658
  67. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_other line 662
  68. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.copySteps line 666
  69. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.copySteps_eq line 668
  70. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.steps line 673

    Source documentation

    Exact cleanup cost is computed on the actual post-copy tape contents.

    def steps (enumeration : Fin N ≃ K) (output : K) (base : K → List Bool) (n m : Nat) : Nat :=
…
  71. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.budget line 677
  72. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.trace_trans_inline_PoweringMachineFinish line 681
  73. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.traceAt line 687

    Source documentation

    Exact execution inside any ambient program containing these instructions. The only data premises describe physical header words and an empty scratch tape.

    theorem traceAt (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (hvs : headerV ≠ scratch) (hvo : headerV ≠ output)
    (hds : headerD ≠ scratch) (hdo : headerD ≠ output) (hso : scratch ≠ output)
    (labels : Label enumeration output → Λ)
    (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.Alphabet

  74. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.trace line 737

    Source documentation

    The standalone program satisfies the trace with no code or execution premise.

    theorem trace (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (hvs : headerV ≠ scratch) (hvo : headerV ≠ output)
    (hds : headerD ≠ scratch) (hdo : headerD ≠ output) (hso : scratch ≠ output)
    (base : K → List Bool) (n m : Nat) (suffixV suffixD : List Bool)
    (wordV : base headerV = encodeWord n ++ suffixV)
    (wordD : base headerD = encodeWord m ++ suffixD)
    (scratchEmpty : base scratch = []) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program enumeration headerV headerD output scratch)))^[
      steps enumeration output base n m]
      (some ⟨some (.inl .seed), (ambient, register), base⟩) =
      some ⟨none, (ambient, none),
        MachineDrainMany.haltTapes output (encodeWords [n, m] ++ base output)⟩ :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.program, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.steps, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.haltTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  75. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.steps_le_budget line 753
  76. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_length_le line 759
  77. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.steps_le_uniform line 773

    Source documentation

    A uniform pre-cleanup stack bound gives a linear finishing budget.

    theorem steps_le_uniform (enumeration : Fin N ≃ K) (output : K)
    (base : K → List Bool) (n m bound : Nat)
    (bounded : ∀ k, (base k).length ≤ bound) :
    steps enumeration output base n m ≤ 2 * (n + m) + 6 + N * (bound + n + m + 3) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.steps

  78. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.execution line 788

    Source documentation

    A bounded execution witness, obtained from the physical trace above.

    def execution (enumeration : Fin N ≃ K) (headerV headerD output scratch : K)
    (hvs : headerV ≠ scratch) (hvo : headerV ≠ output)
    (hds : headerD ≠ scratch) (hdo : headerD ≠ output) (hso : scratch ≠ output)
    (base : K → List Bool) (n m : Nat) (suffixV suffixD : List Bool)
    (wordV : base headerV = encodeWord n ++ suffixV)
    (wordD : base headerD = encodeWord m ++ suffixD)
    (scratchEmpty : base scratch = []) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program enumeration headerV headerD output scratch))
      ⟨some (.inl .seed), (ambient, register), base⟩
      (some ⟨none, (ambient, none),
        MachineDrainMany.haltTapes output (encodeWords [n, m] ++ base output)⟩)
      (budget enumeration output base n m) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.program, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.haltTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.budget