OAI/Computability/UniqueGames/Machines/MachineExpanderRowFrames.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

Concrete data and tape frames for an actual expander-row computation

Only the five actual row inputs are stored. Every address, table return and finite control value below is computed from those inputs. The thirteen tape frames use the existing phase-output functions. These are data identities and size bounds, not assumed machine executions. Kernel-checked with Lean 4.33.1.

  1. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData line 22
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.rowData line 29
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.control0 line 37
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstRow line 38
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstValue line 39
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstPair line 40
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex line 41
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn line 42
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.control1 line 43
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondRow line 44
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondValue line 45
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondPair line 46
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex line 47
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn line 48
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.control2 line 49
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.query1 line 50
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.query2 line 51
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.finalValue line 52
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.tableLength line 53
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.query1_eq_firstRow line 55
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.query2_eq_secondRow line 58
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_div_degree line 61
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_mod_degree line 62
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_div_degree line 63
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_mod_degree line 64
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_eq_residue line 66
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_eq_residue line 70
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.receiveFirst_residue_eq_control1 line 74
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.receiveSecond_residue_eq_control2 line 80
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstSelected line 86
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondSelected line 90
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.evaluateRow_eq line 94
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.finalValue_eq_step_reverseIndex line 97
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.rows_le_tableLength line 104
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.query1_le_tableLength line 108
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.query2_le_tableLength line 112
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_le_tableLength line 116
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_le_tableLength line 119
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.inputVertex_le_tableLength line 122
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex_le_tableLength line 127
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex_le_tableLength line 131
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_le_tableLength line 135
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_le_tableLength line 139
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frameContents line 148

    Source documentation

    Complete explicit tape contents; all three scratch roles omitted here are empty.

    def frameContents (r : RowData v d) (output : List Bool)
    (qr qi lo q1 q2 r1 r2 : List Bool) : Tape → List Bool
  | .inputVertex => encodeWord r.inputVertex.val
  | .table => encodeWords (rotationWords r.oldTable)
  | .output => output
  | .queryReverse => qr
  | .queryIndex => qi
  | .lookupOutput => lo
  | .quotientFirst => q1
  | .quotientSecond => q2
  | .remainderFirst => r1
  | .remainderSecond => r2
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame0 line 162
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame1 line 164
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame2 line 166
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame3 line 168
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame4 line 171
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame5 line 173
  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame6 line 175
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame7 line 177
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame8 line 179
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame9 line 182
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame10 line 184
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame11 line 186
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame12 line 188
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_id_eq line 191
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame1_eq line 199
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame2_eq line 205
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame3_eq line 211
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame4_eq line 217
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame5_eq line 223
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame6_eq line 231
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame7_eq line 237
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame8_eq line 244
  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame9_eq line 251
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame10_eq line 258
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame11_eq line 266
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame12_eq line 274
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.final_frame_eq line 280
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame0_inputVertex line 287
  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame0_table line 290
  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame0_output line 293
  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame1_inputVertex line 296
  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame1_emitScratch line 299
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame2_queryReverse line 302
  78. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame2_queryIndex line 305
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame3_table line 308
  80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame3_lookupRestore line 311
  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame3_lookupWork line 314
  82. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame3_lookupOutput line 317
  83. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame3_queryIndex line 320
  84. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame4_lookupOutput line 323
  85. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame4_quotientFirst line 326
  86. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame4_remainderFirst line 329
  87. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame6_quotientFirst line 332
  88. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame6_emitScratch line 335
  89. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame7_queryReverse line 338
  90. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame7_queryIndex line 341
  91. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame8_table line 344
  92. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame8_lookupRestore line 347
  93. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame8_lookupWork line 350
  94. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame8_lookupOutput line 353
  95. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame8_queryIndex line 356
  96. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame9_lookupOutput line 359
  97. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame9_quotientSecond line 362
  98. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame9_remainderSecond line 365
  99. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame10_quotientSecond line 368
  100. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame10_emitScratch line 371
  101. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame10_output line 374
  102. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.final_dirty_word_length_le line 377
  103. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.cleanupSteps_le_tableLength line 385