OAI/Computability/UniqueGames/PCP/SourceContextLoad.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

A shared-arena context loader. Its finite program copies each selected clause index, executes the checked lookup, and clears consumed scratch tapes. Tuple digits and arbitrary extra tapes are protected throughout.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.Tape line 17
  2. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.Label line 24
  3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.place line 33
  4. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.fill line 37
  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.fill_place line 44
  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.fill_self line 49
  7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.fill_update line 59
  8. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.placedLabel line 68
  9. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.placedConfiguration line 72
  10. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.placedStatement line 78
  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.placed_stepAux line 90
  12. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.nextLabel line 115
  13. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.program line 118
  14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.placed_step line 129
  15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.lookupOutput line 146
  16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.placedLookupInTime line 151
  17. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.copiedTapes line 167
  18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.coordinateOutput line 170
  19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.cleanup_lookupOutput line 178
  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.coordinateOutput_current line 207
  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.coordinateOutput_remaining line 212
  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.coordinateOutput_field line 217
  23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.coordinateOutput_other_field line 224
  24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.suffix_length_le_input line 229
  25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.coordinateInTime line 241
  26. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.labelAt line 286
  27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.nextLabel_eq line 289
  28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes line 291
  29. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes_frame line 299
  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes_clean line 312
  31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes_field line 324
  32. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.prefixInTime line 349
  33. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.loadInTime line 392
  34. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.clauses_length_le_input line 415
  35. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.loadUnaryInTime line 422

    Source documentation

    Actual odometer digits have empty suffixes. The resulting complete loader runs in a polynomial whose coefficients depend only on the fixed repetition u.

    noncomputable def loadUnaryInTime (F : Target.Formula) (tuple : Fin u → Fin F.clauses.length)
    (base : Tape u Extra → List Bool)
    (hformula : base .formula = formulaBits F)
    (hcurrent : ∀ j, base (.current j) = encodeWord (tuple j).val)
    (hindex : base .index = []) (hwork : base .work = [])
    (hscratch : base .scratch = []) (hcopy : base .copyScratch = []) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labelAt 0), ((), none), base⟩
      (some ⟨none, ((), none), stageTapes F tuple base u⟩)
      (u * (10 * (formulaBits F).length + 20) + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.labelAt, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes

  36. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.timePolynomial line 445
  37. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.timePolynomial_eval line 448
  38. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.variableSlot line 454
  39. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.polaritySlot line 455
  40. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.variableField line 456
  41. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.polarityField line 457
  42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.clauseWords_variable line 459
  43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.clauseWords_polarity line 465
  44. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.output_variable line 473
  45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.output_polarity line 480
  46. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.machine line 489