OAI/Computability/UniqueGames/Machines/MachineCloudPrefix.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.Tape line 14
2. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.Label line 19
3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.Alphabet line 25
4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.State line 26
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.memory line 28
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame line 35
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame_query line 38
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame_count line 40
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame_power line 42
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame_level line 44
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame_bound line 46
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame_remaining line 48
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame_total line 50
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.update_frame_query line 53
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.update_frame_count line 61
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.update_frame_power line 69
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.update_frame_level line 77
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.update_frame_remaining line 85
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.update_frame_total line 89
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.paddingView line 94
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.paddingView_left line 98
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.paddingView_right line 100
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.placedTapes line 104
24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.program line 111
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.appendTrace line 127
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.paddingTrace line 133

    Source documentation

    The inner program is embedded with its actual table scan and geometric search; all three additional tapes are preserved by every inner transition.

    theorem paddingTrace (t : GraphTables.Table) (v : Fin t.vertices)
        (bound remaining total : List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[MachineCloudPadding.totalTime t v]
          (some ⟨some (.padding .init), ((ambient, false), register),
            frame (GraphTables.tableBits t) (encodeWord v.val) [] [] [] bound remaining total⟩) =
          some ⟨some .add, ((ambient, false), none),
            frame (GraphTables.tableBits t) (encodeWord v.val)
              (encodeWord (PreprocessingCloudIndex.cloudSize t v))
              (encodeWord (MachineCloudPadding.padding (PreprocessingCloudIndex.cloudSize t v)))
              (encodeWord (PreprocessingLevels.boundedLevel (PreprocessingCloudIndex.cloudSize t v)))
              bound remaining total⟩ := by
    …

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

27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.incrementStep line 151
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.bodyTime line 160
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.bodyTrace line 168

    Source documentation

    Padding tallies are consumed by unary addition; count and level fields are scanned away, and the remaining zero padding delimiter is removed while the physical vertex counter increases.

    theorem bodyTrace (t : GraphTables.Table) (v : Fin t.vertices)
        (bound remaining : List Bool) (acc : Nat) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[bodyTime t v]
          (some ⟨some (.padding .init), ((ambient, false), register),
            frame (GraphTables.tableBits t) (encodeWord v.val) [] [] []
              bound remaining (encodeWord acc)⟩) =
          some ⟨some .guard, ((ambient, false), none),
            frame (GraphTables.tableBits t) (encodeWord (v.val + 1)) [] [] []
              bound remaining (encodeWord (MachineCloudPadding.padding (PreprocessingCloudIndex.cloudSize t v) + acc))⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.bodyTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.frame, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.padding

30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.guardStep_succ line 210
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.guardStep_zero line 220
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.zeroTrace line 228
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.amount line 242
34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.cycleTime line 245
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.sumFrom line 248
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.loopTime line 252
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.loopTrace line 256
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.sumFrom_list line 287
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.sumFrom_eq_offset line 306
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.initStep line 315
41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.totalTime line 322
42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.prefixTrace line 325
43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.cycleBudget line 355

    Source documentation

    Uniform budget for one vertex iteration, including unary addition and cleanup. Its input argument bounds the complete table length.

    def cycleBudget (L : Nat) : Nat :=
    …

44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.bodyTime_le line 359
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.loopTime_le line 387
46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.inputLength line 400
47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.timePolynomial line 403
48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.totalTime_le line 412

    Source documentation

    The full execution has a cubic polynomial bound in the two actual preserved input words. The accumulator is never scanned to perform addition.

    theorem totalTime_le (t : GraphTables.Table) (b : Nat) (hb : b ≤ t.vertices)
        (suffix : List Bool) :
        totalTime t b suffix ≤ timePolynomial.eval (inputLength t b suffix) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.inputLength

49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.prefixInTime line 432
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.all_padding_sum line 449

    Source documentation

    At the complete vertex bound the output is the sum of all padding counts used by the actual regularized-table header.

    theorem all_padding_sum (t : GraphTables.Table) :
        sumFrom t 0 t.vertices = ∑ v, PreprocessingRegularTables.padding t v := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.sumFrom

51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.paddingOrder_eq_prefix line 455

    Source documentation

    At a vertex bound, adding its local dummy index to this machine's result gives precisely the existing executable padding-order index.

    theorem paddingOrder_eq_prefix (t : GraphTables.Table) (v : Fin t.vertices)
        (j : Fin (PreprocessingRegularTables.padding t v)) :
        (PreprocessingRegularTables.paddingOrder (PreprocessingRegularTables.padding t) ⟨v, j⟩).val =
          sumFrom t 0 v.val + j.val := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.sumFrom