OAI/Computability/UniqueGames/PCP/SourceContextClear.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.Tape line 15
  2. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.fieldAt line 19
  3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.fields line 22
  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.fieldAt_injective line 24
  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.fields_length line 31
  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.fields_nodup line 34
  7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.field_mem line 37
  8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.mem_fields_iff line 42
  9. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.outputTapes line 50
  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.output_field line 54
  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.output_frame line 57
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.Label line 61
  13. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.entryLabel line 64
  14. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.main line 68
  15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.program line 72
  16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.entryLabel_eq line 77
  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.entry_eq line 84
  18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.finalTapes_eq line 88
  19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.lengthSum_update line 94
  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.steps_eq_of_nodup line 105

    Source documentation

    Distinct chosen tapes make the pre-cleanup length sum the exact drain cost.

    private theorem steps_eq_of_nodup {K : Type} [DecidableEq K] (chosen : List K)
    (h : chosen.Nodup) (base : K → List Bool) :
    MachineDrainMany.steps chosen base =
      MachineDrainMany.lengthSum chosen base + chosen.length := by
…
  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.trace_trans line 117
  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.clearTrace line 121
  23. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.clearInTime line 133
  24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.lengthSum_le_selected line 141
  25. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.clauseField_length_le line 153
  26. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.variables_add_two_le_input line 161
  27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.loaded_field_length_le line 168
  28. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.loaded_cost_le line 177
  29. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.clearLoadedInTime line 190
  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.output_loaded_eq_base line 202
  31. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.clearLoadedToBaseInTime line 215

    Source documentation

    With initially clean fields and lookup work tapes, loading followed by this cleanup restores the caller's original frame exactly.

    def clearLoadedToBaseInTime (F : Target.Formula) (tuple : Fin u → Fin F.clauses.length)
    (base : Tape u Extra → List Bool) (hfields : ∀ j s, base (.field j s) = [])
    (hindex : base .index = []) (hwork : base .work = []) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some main, ((), register), SourceContextLoad.stageTapes F tuple base u⟩
      (some ⟨none, ((), none), base⟩)
      (6 * u * ((formulaBits F).length + 1) + 1) := by
…

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

  32. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextClear.machine line 225