OAI/Computability/MaxCut/PCP/ContextLoad.lean

GitHub source file

63 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.MaxCutGames.Foundations.Hastad.SourceContextLoad.Tape line 15
  2. inductive OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.Label line 22
  3. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.place line 31
  4. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.fill line 35
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.fill_place line 42
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.fill_self line 47
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.fill_update line 57
  8. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.placedLabel line 66
  9. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.placedConfiguration line 70
  10. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.placedStatement line 76
  11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.placed_stepAux line 88
  12. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.nextLabel line 113
  13. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.program line 116
  14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.placed_step line 127
  15. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.lookupOutput line 144
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.placedLookupInTime line 149
  17. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.copiedTapes line 165
  18. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput line 168
  19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.cleanup_lookupOutput line 176
  20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_current line 205
  21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_remaining line 210
  22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_field line 215
  23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_other_field line 222
  24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.suffix_length_le_input line 227
  25. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.coordinateInTime line 239
  26. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.labelAt line 284
  27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.nextLabel_eq line 287
  28. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes line 289
  29. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes_frame line 297
  30. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes_clean line 310
  31. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes_field line 322
  32. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.prefixInTime line 347
  33. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.loadInTime line 390
  34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.clauses_length_le_input line 413
  35. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.loadUnaryInTime line 420

    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.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.program, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.labelAt, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes

  36. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.timePolynomial line 443
  37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.timePolynomial_eval line 446
  38. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.variableSlot line 452
  39. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.polaritySlot line 453
  40. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.variableField line 454
  41. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.polarityField line 455
  42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.clauseWords_variable line 457
  43. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.clauseWords_polarity line 463
  44. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.output_variable line 471
  45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.output_polarity line 478
  46. def OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.machine line 487
  47. abbrev OAI.MaxCutGames.Foundations.Hastad.Cube line 510
  48. def OAI.MaxCutGames.Foundations.Hastad.bitSign line 512
  49. theorem OAI.MaxCutGames.Foundations.Hastad.bitSign_sq line 514
  50. theorem OAI.MaxCutGames.Foundations.Hastad.bitSign_xor line 517
  51. def OAI.MaxCutGames.Foundations.Hastad.cubeXor line 521
  52. def OAI.MaxCutGames.Foundations.Hastad.walsh line 523
  53. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_symm line 526
  54. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_sq line 530
  55. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_xor line 534
  56. theorem OAI.MaxCutGames.Foundations.Hastad.coordinate_orthogonality line 542
  57. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_sum_orthogonality line 547
  58. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_orthogonality line 564
  59. def OAI.MaxCutGames.Foundations.Hastad.coefficient line 571
  60. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_inversion line 574
  61. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_inner line 591
  62. theorem OAI.MaxCutGames.Foundations.Hastad.walsh_parseval line 608
  63. theorem OAI.MaxCutGames.Foundations.Hastad.sign_parseval line 612