OAI/Computability/MaxCut/Machines/MachineCloudCount.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Tape line 11
2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Tape.enumList line 15
3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Tape.enumList_getElem?_ctorIdx_eq line 18
4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Tape.enumList_nodup line 22
5. instance OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.(instance at line 24) line 24
6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Alphabet line 28
7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.State line 29
8. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory line 31
9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory_original line 39
10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory_work line 41
11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory_target line 43
12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory_scratch line 45
13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory_count line 47
14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory_spare line 49
15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.update_memory_work line 52
16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.update_memory_target line 56
17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.update_memory_scratch line 60
18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.update_memory_count line 64
19. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.finishField line 71
20. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldLoop line 74
21. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.hit line 89

    Source documentation

    Specification only: equality of the original natural values, unless an earlier step has already detected overflow.

    def hit (flag : Bool) (x v : Nat) : Nat := if flag = false ∧ x = v then 1 else 0

22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldStep_zero line 91
23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_zero line 108
24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_succ line 124
25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldTrace line 142

    Source documentation

    The actual field-reading trace. The scratch holds exactly the consumed target bits, and the output increment records equality of the complete field.

    theorem fieldTrace (again restore : Λ)
        (program : Λ → TM2.Stmt Alphabet Λ (State σ))
        (atField : program again = fieldLoop again restore)
        (original suffix targetSuffix spare : List Bool) (x v : Nat)
        (scratch count : List Bool) (ambient : σ) (flag : Bool) (register : Option Bool) :
        (advance (TM2.step program))^[x + 1]
          (some ⟨some again, ((ambient, flag), register),
            memory original (encodeWord x ++ suffix) (encodeWord v ++ targetSuffix)
              scratch count spare⟩) =
          some ⟨some restore, ((ambient, false), none),
            memory original suffix (encodeWord (v - x) ++ targetSuffix)
              (List.replicate (min x v) true ++ scratch)
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.State, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldLoop, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.replicate_encodeWord line 176
27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.preservingFieldTrace line 181

    Source documentation

    The actual restoring transfer returns every consumed target bit.

    theorem preservingFieldTrace (again restore next : Λ)
        (program : Λ → TM2.Stmt Alphabet Λ (State σ))
        (atField : program again = fieldLoop again restore)
        (atRestore : program restore = Reduction.MachineTransfer.loopAt
          .scratch .target id false restore (some next))
        (original suffix targetSuffix count spare : List Bool) (x v : Nat)
        (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[x + min x v + 2]
          (some ⟨some again, ((ambient, false), register),
            memory original (encodeWord x ++ suffix) (encodeWord v ++ targetSuffix)
              [] count spare⟩) =
          some ⟨some next, ((ambient, false), none),
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.State, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldLoop, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

28. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.preservingFieldInTime line 213
29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.discardFieldsTrace line 235

    Source documentation

    Consecutive concrete field-discard instructions consume a fixed list of fields. The hypotheses specify code, not an abstract body execution.

    theorem discardFieldsTrace (labels : Nat → Λ)
        (program : Λ → TM2.Stmt Alphabet Λ (State σ))
        (fields : List Nat) (offset : Nat)
        (atField : ∀ i, i < fields.length → program (labels (offset + i)) =
          MachineLookup.discard .work (labels (offset + i)) (labels (offset + i + 1)))
        (original suffix target scratch count spare : List Bool)
        (ambient : σ) (flag : Bool) (register : Option Bool) :
        (advance (TM2.step program))^[(encodeWords fields).length]
          (some ⟨some (labels offset), ((ambient, flag), register),
            memory original (encodeWords fields ++ suffix) target scratch count spare⟩) =
          some ⟨some (labels (offset + fields.length)),
            ((ambient, flag), if fields = [] then register else none),
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.State, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discard, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.memory

30. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Label line 270
31. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.skipLabel line 275
32. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowEntry line 278
33. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program line 286

    Source documentation

    A single fixed program copies the input once, skips two headers, then compares the first field of each 4098-field row.

    def program : Label → TM2.Stmt Alphabet Label (State σ)
      | .copyFirst => Reduction.MachineTransfer.loopAt
          .original .spare id false .copyFirst (some .copySecond)
      | .copySecond => MachineCopy.forkLoop
          .spare .original .work false .copySecond (some .headerFirst)
      | .headerFirst => MachineLookup.discard .work .headerFirst .headerSecond
      | .headerSecond => MachineLookup.discard .work .headerSecond .row
      | .row => rowEntry
      | .field => fieldLoop .field .restore
      | .restore => Reduction.MachineTransfer.loopAt
          .scratch .target id false .restore (some (skipLabel 0))
      | .skip i => MachineLookup.discard .work (.skip i) (skipLabel (i.val + 1))

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Label, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.State, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop, OAI.MaxCutGames.Foundations.Complexity.MachineLookup.discard, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowEntry, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.fieldLoop, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.skipLabel

34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program_skip line 299
35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowStep_nonempty line 304
36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowStep_empty line 314
37. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Row line 320
38. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowWords line 322
39. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowTime line 324
40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowTrace line 328

    Source documentation

    One complete stored row is consumed; the target and original are restored.

    theorem rowTrace (r : Row) (hwidth : r.2.length = 4097) (v : Nat)
        (original suffix targetSuffix count spare : List Bool) (ambient : σ)
        (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[rowTime v r]
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Row, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowTime

41. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowsHits line 363
42. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowsTime line 367
43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowsTrace line 372

    Source documentation

    The complete actual row scan halts with the number of matching tails.

    theorem rowsTrace (rs : List Row) (hwidth : ∀ r ∈ rs, r.2.length = 4097) (v : Nat)
        (original targetSuffix count spare : List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[rowsTime v rs]
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Row, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowsTime

44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowTime_le line 396
45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowsTime_le line 405
46. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.inputWord line 415
47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.inputWord_eq line 418
48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.inputWord_length line 422
49. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.totalSteps line 429
50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.countTrace line 434

    Source documentation

    One preserving copy, the two concrete header discards, and the proved row scan form the complete execution. The input and target tapes are unchanged.

    theorem countTrace (n m v : Nat) (rs : List Row)
        (hwidth : ∀ r ∈ rs, r.2.length = 4097)
        (targetSuffix count : List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[totalSteps n m v rs]
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.Row, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.totalSteps

51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.totalSteps_le line 469
52. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.tableRows line 478
53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.tableRows_width line 482
54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.tableRows_words line 488
55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.tableRows_input line 495
56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowsHits_eq_filter line 500
57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowList_eq_finRange_map line 507
58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.rowList_cloud_count line 514
59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.tableRows_hits line 520
60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.cloudCountTrace line 528

    Source documentation

    Cloud size is produced by reading the actual encoded tail fields, with the complete graph input and unary vertex query preserved on their tapes.

    theorem cloudCountTrace (t : GraphTables.Table) (v : Fin t.vertices)
        (targetSuffix countSuffix : List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step (program (σ := σ))))^[totalSteps t.vertices t.darts v.val (tableRows t)]
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.totalSteps, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.tableRows

61. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.cloudCountInTime line 543

    Source documentation

    A linear transition budget for this concrete cloud-count subroutine.

    def cloudCountInTime (t : GraphTables.Table) (v : Fin t.vertices)
        (targetSuffix countSuffix : List Bool) (ambient : σ) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step (program (σ := σ)))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.program

62. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Tape line 566
63. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList line 570
64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList_getElem?_ctorIdx_eq line 573
65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList_nodup line 577
66. instance OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.(instance at line 579) line 579
67. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Label line 583
68. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Label.enumList line 588
69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Label.enumList_getElem?_ctorIdx_eq line 591
70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Label.enumList_nodup line 595
71. instance OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.(instance at line 597) line 597
72. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Alphabet line 601
73. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.State line 602
74. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.memory line 604
75. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.update_work line 614
76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.update_power line 617
77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.update_saved line 620
78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.update_level line 623
79. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.update_fuel line 626
80. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.update_product line 629
81. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.compareLoop line 635
82. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.scaleLoop line 647

    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.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Label, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.State

83. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.program line 656
84. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.overflow line 679
85. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.compareStep_zero line 681
86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_zero line 691
87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_succ line 701
88. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.compareTrace line 712

    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.MaxCutGames.Foundations.Complexity.MachineCeilingPower.program, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.overflow

89. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.replicate_encodeWord line 737
90. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.compareRestoredTrace line 741
91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.appendTrace_inline_MachineCeilingPower line 762
92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.scaleStep_succ line 766
93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.scaleStep_zero line 777
94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.scaleScanTrace line 787
95. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.scaleTrace line 807

    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.MaxCutGames.Foundations.Complexity.MachineCeilingPower.program, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.cleanupTrace line 829
97. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.guardStep_succ line 840
98. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.guardStep_zero line 851
99. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.decideStep line 862
100. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.prefixTime line 874
101. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.prefixTrace line 878

     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.MaxCutGames.Foundations.Complexity.MachineCeilingPower.program, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.prefixTime, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

102. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.coreTime line 905
103. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.coreTrace line 912

     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.MaxCutGames.Foundations.Complexity.MachineCeilingPower.program, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.coreTime, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

104. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.roundBudget line 940
105. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le line 942
106. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le_roundBudget line 947
107. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.continuingTime_le line 953
108. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.coreTime_le line 961
109. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.initStep line 986
110. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.totalTime line 994
111. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.searchTrace line 998

     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.MaxCutGames.Foundations.Complexity.MachineCeilingPower.program, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

112. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.timeBound line 1018
113. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.totalTime_le line 1020
114. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.timePolynomial line 1029

     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 :=
     …

115. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.timePolynomial_encoding line 1032
116. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.paddingTrace line 1038

     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.MaxCutGames.Foundations.Complexity.MachineCeilingPower.program, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

117. def OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.paddingInTime line 1046
118. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.paddingOutput_bounds line 1057