OAI/Computability/UniqueGames/Machines/MachinePaddingRowsLemmas.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the actual outer padding-loop recurrence. No execution or cost premise is introduced: the recurrence is the one matched to the concrete machine by MachinePaddingRows.loopTrace.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.Control line 10
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.Control.enumList line 14
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.Control.enumList_getElem?_ctorIdx_eq line 16
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.Control.enumList_nodup line 20
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.(instance at line 22) line 22
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.Tape line 26
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.Label line 27
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.Alphabet line 28
  9. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.State line 30
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.bodyEntry line 32
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.extra line 35
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.program line 46
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.tapes line 49
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.cfg line 53
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.bodyTrace line 57
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.guard_succ line 75
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.guard_zero line 86
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.bump_step line 97
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.paddingBits line 109
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.steps line 113
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.loopTrace line 120

    Source documentation

    The entire varying-length padding loop is proved from its actual guards, actual row bodies and actual vertex increments.

    theorem loopTrace (d : Nat) (hd : 0 < d) (count v e : Nat) (output : List Bool) :
    (advance (TM2.step (program d hd)))^[steps d v e output count]
      (some (cfg d (some (.inr .guard)) v e count output)) =
      some (cfg d none (v + count) (e + count * d) 0
        (output ++ paddingBits d v e count)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.paddingBits

  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.initialTapes line 142
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.initialize_step line 145
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.paddingTrace line 160
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.machine line 167
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.execution line 180

    Source documentation

    The exact time count is the sum of the physically executed row loops. Its polynomial bound is derived separately from this recurrence.

    def execution (d : Nat) (hd : 0 < d) (count v e : Nat) (output : List Bool) :
    StateTransition.EvalsToInTime (machine d hd).step
      ⟨some (.inr .initialize), (((), none), ()), initialTapes v e count output⟩
      (some (cfg d none (v + count) (e + count * d) 0
        (output ++ paddingBits d v e count)))
      (steps d v e output count + 1) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.paddingBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.steps

  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowsBits_length_le line 201

    Source documentation

    All rows in a fixed block are bounded by its last possible index.

    theorem rowsBits_length_le (v e count : Nat) :
    (MachineDummyRows.rowsBits v e count).length ≤ count * (v + e + count + 8194) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits

  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowBound line 217

    Source documentation

    A common row-size bound for all remaining vertices and ports.

    def rowBound (d v e count : Nat) : Nat := v + count + e + (count + 1) * d + 8194
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowBound_next line 221

    Source documentation

    This bound is invariant when one vertex and its d reverse indices have been consumed from the remaining outer-loop count.

    theorem rowBound_next (d v e count : Nat) :
    rowBound d (v + 1) (e + d) count = rowBound d v e (count + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowBound

  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.blockRow_le_rowBound line 226
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.steps_le_bound line 233

    Source documentation

    The actual outer-loop cost is bounded by the number of vertices times a uniform bound on its actual row bodies and two control transitions.

    theorem steps_le_bound (d v e : Nat) (output : List Bool) (count : Nat) :
    MachinePaddingRows.steps d v e output count ≤
      count * (d * (4 * rowBound d v e count +
        2 * (output.length + count * d * rowBound d v e count) + 10) + 2) + 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingRows.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowBound

  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.inputSize line 284

    Source documentation

    Exact variable-size input: two unary fields, unary fuel, and old output.

    def inputSize (v e count : Nat) (output : List Bool) : Nat :=
…
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowCap line 287
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowBound_le_cap line 289
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.rowPolynomial line 302
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.timePolynomial line 307

    Source documentation

    A cubic polynomial for fixed degree, including the final zero-fuel guard. The one-time relation initializer can be accounted for separately.

    noncomputable def timePolynomial (d : Nat) : Polynomial Nat :=
…
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingBounds.timePolynomial_bounds line 313
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingCertificate.timePolynomial line 344
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingCertificate.execution line 347