OAI/Computability/UniqueGames/PCP/SourceQueryOrderLemmas.lean

GitHub source file

141 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.occurrenceBits line 18
  2. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.slotBits line 21
  3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.tupleBits line 25
  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.equationBits_eq line 28
  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.prefixBits_eq_slotBits line 35
  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.sourceLoopInTime line 48
  7. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.BodyWork line 95
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.BodyExtra line 103
  9. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.Arena line 104
  10. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.QueryState line 105
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.ArithmeticState line 106
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.State line 107
  13. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.QueryMetadata line 108
  14. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.ArithmeticMetadata line 110
  15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.workTape line 115
  16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.variableHeader line 116
  17. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.clauseHeader line 117
  18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.canonicalSignature line 119
  19. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.canonicalState line 122
  20. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.queryStateEquiv line 126
  21. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.arithmeticStateEquiv line 132
  22. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.rankControls line 138
  23. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.clauseRankSlots line 148
  24. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.variableRankSlots line 151
  25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.baseSlots line 156

    Source documentation

    Both address-base phases use the same clean arithmetic work tapes. The right side adds the retained left block; the left side adds a seeded zero.

    def baseSlots (right : Bool) : MachineHorner.Layout 2 ↪ Arena u Extra where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.Arena

  26. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.querySources line 178
  27. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.queryLayout line 183
  28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.perSlotCleanup line 196

    Source documentation

    Retained global headers are excluded from cleanup.

    def perSlotCleanup : List (Arena u Extra) := [workTape .rank, workTape .leftBase]

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.Arena, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.workTape

  29. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.finalBaseCleanup line 197
  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.initializer_arena line 199
  31. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.Extra line 211
  32. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.Tape line 212
  33. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.State line 213
  34. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.outputTape line 215
  35. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.accumulatorTape line 216
  36. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.headerControl line 218
  37. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.headerSlots line 236
  38. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.ControlAmbient line 252
  39. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.controlStateEquiv line 256

    Source documentation

    Expose the existing arithmetic head register to the odometer and final cleanup. This is a static finite-state equivalence, with no machine steps.

    def controlStateEquiv (u D : Nat) :
    ControlAmbient u D × Option Bool ≃ State u D where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.ControlAmbient, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.State

  40. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.initialQuery line 265
  41. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.initialState line 268
  42. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.initialAmbient line 271
  43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.control_initial line 274
  44. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.coefficientKeys line 277
  45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.mem_coefficientKeys line 285
  46. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.workKeys line 291
  47. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.mem_workKeys line 297
  48. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.allTapes line 309

    Source documentation

    An explicit tape enumeration, fixed before the input is supplied. It uses constructor lists and increasing finite coefficient indices.

    noncomputable def allTapes (u D : Nat) : List (Tape u D) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.Tape

  49. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.mem_allTapes line 317
  50. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.clearKeys line 337
  51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.mem_clearKeys line 342
  52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGeneratorModel.accumulator_ne_output line 347
  53. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.Tape line 364
  54. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.State line 365
  55. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ArithmeticLabel line 366
  56. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.Label line 367
  57. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.headerLayout line 371
  58. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.arithmeticEntry line 379
  59. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.arithmeticProgram line 382
  60. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.program line 387
  61. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialTapes line 393
  62. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initializedTapes line 396
  63. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.countedTapes line 399
  64. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.outputTapes line 403
  65. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.readyTapes line 408
  66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_formula line 415
  67. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_current line 419
  68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_remaining line 423
  69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_variableHeader line 427
  70. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_clauseHeader line 433
  71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_work line 439
  72. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_work_raw line 446
  73. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_field line 450
  74. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialized_clean line 457
  75. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initialArithmeticMetadata line 471
  76. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initial_arithmetic line 474
  77. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initial_loader line 478
  78. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.initializeInTime line 482
  79. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.arithmeticInTime line 498
  80. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.arithmeticConfiguration line 520
  81. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.arithmetic_step line 526
  82. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.arithmeticPlacedInTime line 544
  83. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.phaseBound line 559
  84. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.phasesInTime line 565
  85. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.output_eq_ready line 574
  86. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_formula line 591
  87. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_current line 594
  88. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_remaining line 597
  89. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_variableHeader line 600
  90. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_clauseHeader line 603
  91. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_leftBlock line 606
  92. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_dummy line 610
  93. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_accumulator line 614
  94. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_field line 618
  95. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_work_blank line 621
  96. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_sharedWork line 627
  97. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.ready_sharedFrame line 631
  98. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.startupInTime line 641
  99. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.timePolynomial line 649
  100. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.phaseBound_le_polynomial line 654
  101. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.startupInPolynomialTime line 675
  102. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceStartup.machine line 684
  103. structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.Snapshot line 706
  104. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes line 716
  105. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_rank line 724
  106. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_rightBase line 726
  107. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_leftBase line 728
  108. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_zero line 730
  109. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_accumulator line 732
  110. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_coefficient line 734
  111. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_dummy line 736
  112. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_leftBlock line 738
  113. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_queryTemporary line 740
  114. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_queryScratch line 742
  115. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_field line 744
  116. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_current line 746
  117. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_formula line 748
  118. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_index line 750
  119. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_work line 752
  120. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_variableHeader line 754
  121. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_clauseHeader line 756
  122. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.update_rank line 761
  123. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.update_rightBase line 770
  124. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.update_leftBase line 779
  125. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.update_zero line 788
  126. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.update_emitted line 797
  127. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.query_result line 807
  128. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.horner_clause_result line 816
  129. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.horner_variable_result line 823
  130. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.horner_right_result line 831
  131. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.horner_left_result line 838
  132. structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.WorkClean line 845
  133. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.clean_clause line 852
  134. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.clean_variable line 860
  135. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.clean_base line 868
  136. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_coordinateOutput line 876
  137. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes_stageTapes line 889
  138. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.final_tapes line 901
  139. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.empty_tapes line 914
  140. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.clear_loaded line 921
  141. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.clearLoadedSnapshotInTime line 929

    Source documentation

    Apply the checked actual field cleanup directly to an overlaid loaded context.

    def clearLoadedSnapshotInTime (F : Target.Formula) (c : ClauseContext F u)
    (base : Arena u Extra → List Bool) (s : Snapshot)
    (hfields : ∀ j k, base (.field j k) = []) (hindex : base .index = []) (hwork : base .work = [])
    (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step SourceContextClear.program)
      ⟨some SourceContextClear.main, ((), register), tapes (SourceContextLoad.stageTapes F c base u) s⟩
      (some ⟨none, ((), none), tapes base s⟩)
      (6 * u * ((formulaBits F).length + 1) + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.Snapshot, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.main, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleTape.tapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes