OAI/Computability/UniqueGames/Machines/MachineVertexPadding.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Vertex padding from the original serialized port graph

Header counters, the geometric padding count, and the initial row buffer are generated by physical tape operations before the checked row emitter.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.Tape line 23
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.Tape.enumList line 28
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.Tape.enumList_getElem?_ctorIdx_eq line 31
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.Tape.enumList_nodup line 35
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.(instance at line 37) line 37
  6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.Label line 41
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.Alphabet line 50
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.State line 51
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.memory line 54

    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.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.Tape

  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.update_output line 65
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.update_vertex line 68
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.update_edge line 71
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.update_power line 74
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.update_fuel line 77
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.update_relation line 80
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.splitTape line 84
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.splitView line 85
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.splitView_left line 93
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.splitView_right line 95
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.powerTape line 99
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.powerView line 108
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.powerView_left line 119
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.powerView_right line 121
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.subtractTape line 125
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.subtractView line 136
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.subtractView_left line 149
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.subtractView_right line 151
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowTape line 155
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowView line 158
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowView_left line 168
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowView_right line 172
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowAlphabet_eq line 178
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowStateEquiv line 181
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowProgram line 187
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.program line 194
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.appendTrace line 220
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.tableBits_split line 224
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.splitInitialTapes line 230
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.splitResultTapes line 236
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.splitTrace line 242
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.powerTapes line 259
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.powerTrace line 264
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.affineTapes line 278
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.affineOutputTrace line 285
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.headersTrace line 327
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.copyPowerTrace line 343
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.subtractTapes line 357
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.subtractTrace line 364
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowBoolTapes line 379
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.transport_tapes_apply line 384
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowCastTapes line 391
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowInitialTapes line 397
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowFinalTapes line 404
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowTime line 412
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.frameTrace line 415
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowsTrace line 426

    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.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rowTime

  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.cleanupTime line 460
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.cleanupTrace line 462
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.otherTime line 497
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.totalTime line 504
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.vertexPaddingTrace line 509

    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.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.rows_length_le line 545
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.darts_length_le line 550
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.power_length_bound line 554
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.initialOutput_length line 559
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.intermediateCoefficient line 566
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.intermediatePolynomial line 568
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.intermediate_bound line 571
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.otherPolynomial line 586
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.otherTime_le line 590
  71. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.timePolynomial line 606
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.totalTime_le line 609
  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.vertexPaddingInTime line 622

    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.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.timePolynomial

  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.machine line 636
  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.alphabet_finite line 647