OAI/Computability/UniqueGames/Machines/MachineCeilingPower.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Tape line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Tape.enumList line 19
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Tape.enumList_getElem?_ctorIdx_eq line 22
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Tape.enumList_nodup line 26
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.(instance at line 28) line 28
  6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Label line 32
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Label.enumList line 37
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Label.enumList_getElem?_ctorIdx_eq line 40
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Label.enumList_nodup line 44
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.(instance at line 46) line 46
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Alphabet line 50
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.State line 51
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.memory line 53
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.update_work line 63
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.update_power line 66
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.update_saved line 69
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.update_level line 72
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.update_fuel line 75
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.update_product line 78
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.compareLoop line 84
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.scaleLoop line 96

    Source documentation

    Each input tally emits the fixed block of g tallies. The delimiter starts the new power and the level is incremented by an actual push.

    def scaleLoop (g : Nat) : TM2.Stmt Alphabet Label (State σ) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.State

  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.program line 105
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.overflow line 128
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.compareStep_zero line 130
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.compareStep_succ_zero line 140
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.compareStep_succ_succ line 150
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.compareTrace line 161

    Source documentation

    The comparison is performed by actual finite-head transitions.

    theorem compareTrace (g x p : Nat) (input saved level fuel spare product : List Bool)
    (ambient : σ) (flag : Bool) (register : Option Bool) :
    (advance (TM2.step (program g)))^[x + 1]
      (some ⟨some .compare, ((ambient, flag), register),
        memory input (encodeWord x) (encodeWord p) saved level fuel spare product⟩) =
      some ⟨some .restore, ((ambient, overflow flag x p), none),
        memory input [] (encodeWord (p - x))
          (List.replicate (min x p) true ++ saved) level fuel spare product⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.overflow

  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.replicate_encodeWord line 186
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.compareRestoredTrace line 190
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.appendTrace line 211
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.scaleStep_succ line 215
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.scaleStep_zero line 226
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.scaleScanTrace line 236
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.scaleTrace line 256

    Source documentation

    The fixed-coefficient unary multiplication is an actual scan and transfer; the level increment is one explicit push in the final scan transition.

    theorem scaleTrace (g k p e : Nat) (fuel : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program g)))^[p + g * p + 2]
      (some ⟨some .scale, ((ambient, false), register),
        memory (encodeWord k) [] (encodeWord p) [] (encodeWord e) fuel [] []⟩) =
      some ⟨some .guard, ((ambient, false), none),
        memory (encodeWord k) [] (encodeWord (p * g)) [] (encodeWord (e + 1)) fuel [] []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.cleanupTrace line 278
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.guardStep_succ line 289
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.guardStep_zero line 300
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.decideStep line 311
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.prefixTime line 323
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.prefixTrace line 327

    Source documentation

    The loop prefix is an actual guard, preserving copy, comparison, restoration and finite decision, all in the same fixed program.

    theorem prefixTrace (g k p e f : Nat) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program g)))^[prefixTime k p]
      (some ⟨some .guard, ((ambient, false), register),
        memory (encodeWord k) [] (encodeWord p) [] (encodeWord e) (encodeWord (f + 1)) [] []⟩) =
      some ⟨some (if k ≤ p then Label.cleanup else Label.scale), ((ambient, false), none),
        memory (encodeWord k) [] (encodeWord p) [] (encodeWord e) (encodeWord f) [] []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.prefixTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.coreTime line 354
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.coreTrace line 361

    Source documentation

    The fixed machine realizes the exact previously checked bounded loop. Every initial fuel tally is either used or cleared before halting.

    theorem coreTrace (g k f e p : Nat) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program g)))^[coreTime g k f p]
      (some ⟨some .guard, ((ambient, false), register),
        memory (encodeWord k) [] (encodeWord p) [] (encodeWord e) (encodeWord f) [] []⟩) =
      some ⟨none, ((ambient, false), none),
        memory (encodeWord k) []
          (encodeWord (PreprocessingLevels.levelLoop g k f e p).2) []
          (encodeWord (PreprocessingLevels.levelLoop g k f e p).1) [] [] []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.coreTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.roundBudget line 389
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.prefixTime_le line 391
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.prefixTime_le_roundBudget line 396
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.continuingTime_le line 402
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.coreTime_le line 410
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.initStep line 435
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.totalTime line 443
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.searchTrace line 447

    Source documentation

    Initialization writes one and zero, copies the actual input to the fuel tape, and executes the proved loop. All auxiliary tapes are empty on exit.

    theorem searchTrace (g k : Nat) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program g)))^[totalTime g k]
      (some ⟨some .init, ((ambient, false), register), memory (encodeWord k) [] [] [] [] [] [] []⟩) =
      some ⟨none, ((ambient, false), none),
        memory (encodeWord k) []
          (encodeWord (PreprocessingLevels.levelLoop g k k 0 1).2) []
          (encodeWord (PreprocessingLevels.levelLoop g k k 0 1).1) [] [] []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.timeBound line 467
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.totalTime_le line 469
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.timePolynomial line 478

    Source documentation

    The bound is one fixed quadratic polynomial in the actual unary input length. Its coefficient may depend on the fixed growth factor.

    noncomputable def timePolynomial (g : Nat) : Polynomial Nat :=
…
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.timePolynomial_encoding line 481
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.paddingTrace line 487

    Source documentation

    Instantiate the fixed program with the actual expander growth. This is the exact executable result already identified with the ceiling logarithm.

    theorem paddingTrace (k : Nat) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program ExpanderFamily.growth)))^[totalTime ExpanderFamily.growth k]
      (some ⟨some .init, ((ambient, false), register), memory (encodeWord k) [] [] [] [] [] [] []⟩) =
      some ⟨none, ((ambient, false), none),
        memory (encodeWord k) [] (encodeWord (PreprocessingLevels.paddedSize k)) []
          (encodeWord (PreprocessingLevels.boundedLevel k)) [] [] []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.paddingInTime line 495
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.paddingOutput_bounds line 506