OAI/Computability/UniqueGames/Machines/MachineCloudPadding.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Actual cloud counting, geometric padding, and unary subtraction

One finite program places the checked cloud counter and geometric search on shared tapes. Its final phase physically subtracts the preserved cloud size from the computed power. A head test handles the empty cloud separately.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.tapes line 26
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.label line 32
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.configuration line 36
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.statement line 41
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.tapes_apply line 56
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.tapes_update line 62
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.stepAux_simulation line 81
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.step_simulation line 108
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.trace line 128
  10. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Tape line 145
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Tape.enumList line 149
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Tape.enumList_getElem?_ctorIdx_eq line 152
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Tape.enumList_nodup line 156
  14. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.(instance at line 158) line 158
  15. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Label line 162
  16. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Alphabet line 168
  17. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.State line 169
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.memory line 171
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.update_count line 184
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.update_scratch line 187
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.update_power line 190
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.update_level line 194
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.countTape line 198
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.countView line 206
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.countView_left line 215
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.countView_right line 217
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.powerTape line 221
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.powerView line 231
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.powerView_left line 242
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.powerView_right line 244
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.countMemory line 248
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.powerMemory line 253
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.countTapes line 258
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.powerTapes line 263
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.subtractLoop line 270
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.program line 278
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.appendTrace line 293
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.countTrace line 297
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.powerTrace line 313
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.subtractStep_zero line 328
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.subtractStep_succ line 338
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.subtractScanTrace line 348
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.subtractTrace line 373

    Source documentation

    Physical unary subtraction preserves the complete count word by moving its consumed tallies to scratch and then transferring them back.

    theorem subtractTrace (table query level : List Bool) (k p : Nat) (hkp : k ≤ p)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[2 * k + 2]
      (some ⟨some .subtract, ((ambient, false), register),
        memory table query (encodeWord k) [] [] [] (encodeWord p) level [] []⟩) =
      some ⟨none, ((ambient, false), none),
        memory table query (encodeWord k) [] [] [] (encodeWord (p - k)) level [] []⟩ := by
…

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

  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.branchStep_zero line 393
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.branchStep_succ line 401
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.padding line 410
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.postTime line 412
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.postTrace line 417

    Source documentation

    Count zero is handled by a head test. Positive counts execute the exact power search and subtraction traces on the shared count tape.

    theorem postTrace (table query : List Bool) (k : Nat) (ambient : σ)
    (register : Option Bool) :
    (advance (TM2.step program))^[postTime k]
      (some ⟨some .branch, ((ambient, false), register),
        memory table query (encodeWord k) [] [] [] [] [] [] []⟩) =
      some ⟨none, ((ambient, false), none),
        memory table query (encodeWord k) [] [] [] (encodeWord (padding k))
          (encodeWord (PreprocessingLevels.boundedLevel k)) [] []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.postTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.padding

  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.initStep line 445
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.totalTime line 452
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.cloudPaddingTrace line 458

    Source documentation

    One complete concrete program returns the cloud size, geometric level, and required number of padding vertices, preserving input and query.

    theorem cloudPaddingTrace (t : GraphTables.Table) (v : Fin t.vertices)
    (suffix : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[totalTime t v]
      (some ⟨some .init, ((ambient, false), register),
        memory (GraphTables.tableBits t) (encodeWord v.val ++ suffix) [] [] [] [] [] [] [] []⟩) =
      some ⟨none, ((ambient, false), none),
        memory (GraphTables.tableBits t) (encodeWord v.val ++ suffix)
          (encodeWord (PreprocessingCloudIndex.cloudSize t v)) [] [] []
          (encodeWord (padding (PreprocessingCloudIndex.cloudSize t v)))
          (encodeWord (PreprocessingLevels.boundedLevel (PreprocessingCloudIndex.cloudSize t v)))
          [] []⟩ := by
…

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

  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.inputLength line 479
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.count_length_le line 482
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.table_length_le line 489
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.postTime_le line 494
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.timePolynomial line 500
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.totalTime_le line 503
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.cloudPaddingInTime line 520

    Source documentation

    The bound is quadratic in the combined actual graph/query tape length. All transitions are supplied by the concrete program and its phase traces.

    def cloudPaddingInTime (t : GraphTables.Table) (v : Fin t.vertices)
    (suffix : List Bool) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some .init, ((ambient, false), register),
        memory (GraphTables.tableBits t) (encodeWord v.val ++ suffix) [] [] [] [] [] [] [] []⟩
      (some ⟨none, ((ambient, false), none),
        memory (GraphTables.tableBits t) (encodeWord v.val ++ suffix)
          (encodeWord (PreprocessingCloudIndex.cloudSize t v)) [] [] []
          (encodeWord (padding (PreprocessingCloudIndex.cloudSize t v)))
          (encodeWord (PreprocessingLevels.boundedLevel (PreprocessingCloudIndex.cloudSize t v)))
          [] []⟩)
      (timePolynomial.eval (inputLength t v suffix)) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.padding, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.inputLength

  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.count_add_padding line 536