OAI/Computability/MaxCut/Machines/MachineCloudPrefix.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.Tape line 13
2. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.Label line 18
3. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.Alphabet line 24
4. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.State line 25
5. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.memory line 27
6. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame line 34
7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame_query line 37
8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame_count line 39
9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame_power line 41
10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame_level line 43
11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame_bound line 45
12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame_remaining line 47
13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame_total line 49
14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_query line 52
15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_count line 60
16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_power line 68
17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_level line 76
18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_remaining line 84
19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_total line 88
20. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.paddingView line 93
21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.paddingView_left line 97
22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.paddingView_right line 99
23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.placedTapes line 103
24. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.program line 110
25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.appendTrace_inline_MachineCloudPrefix line 126
26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.paddingTrace line 132

    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.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.padding

27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.incrementStep line 150
28. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.bodyTime line 159
29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.bodyTrace line 167

    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.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.bodyTime, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.frame, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.padding

30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.guardStep_succ line 209
31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.guardStep_zero line 219
32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.zeroTrace line 227
33. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.amount line 241
34. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.cycleTime line 244
35. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom line 247
36. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.loopTime line 251
37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.loopTrace line 255
38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_list line 286
39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_eq_offset line 308
40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.initStep line 317
41. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.totalTime line 324
42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.prefixTrace line 327
43. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.cycleBudget line 357

    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.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.bodyTime_le line 361
45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.loopTime_le line 389
46. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.inputLength line 402
47. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.timePolynomial line 405
48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.totalTime_le line 414

    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.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.inputLength

49. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.prefixInTime line 434
50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.all_padding_sum line 451

    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.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom

51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.paddingOrder_eq_prefix line 457

    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.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom

52. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet line 473
53. inductive OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Label line 475
54. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.statement line 482

    Source documentation

    Tape roles: 0 original table, 1 unary index, 2 working copy, 3 output, 4 copy/restore scratch. The embedded halt enters the explicit cleanup loop.

    def statement (tape : Fin 5 → K) (labels : Label → Λ) (exit : Option Λ) :
        Label → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet

55. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.program line 488
56. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.steps line 493

    Source documentation

    Exact copy, lookup, return, and residual-cleanup transition count.

    def steps (values : List Nat) (index : Nat) : Nat :=
    …

57. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.remaining_length_le line 497
58. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le line 504
59. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.timePolynomial line 512
60. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le_timePolynomial line 514
61. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt line 523

    Source documentation

    Actual ambient-program execution. code fixes the concrete instructions at each placed label; it does not assume any execution or semantic behavior. The frame records an empty working copy at both endpoints.

    theorem traceAt (tape : Fin 5 → K) (distinct : Function.Injective tape)
        (labels : Label → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet

62. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt line 581

    Source documentation

    A timed certificate for the same actual trace, bounded by a single linear polynomial in the original table encoding length.

    def inTimeAt (tape : Fin 5 → K) (distinct : Function.Injective tape)
        (labels : Label → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet

63. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.initialTapes_eq line 604

    Source documentation

    The framing representation is the caller's exact tape state whenever its index and work tape contain the specified index and an empty list.

    theorem initialTapes_eq (tape : Fin 5 → K) (base : K → List Bool)
        (index : Nat) (indexSuffix : List Bool)
        (counterWord : base (tape 1) = encodeWord index ++ indexSuffix)
        (workEmpty : base (tape 2) = []) :
        MachinePreservingLookup.initialTapes tape base index indexSuffix [] (base (tape 3)) =
          base := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.initialTapes

64. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt_fromTapes line 614

    Source documentation

    A convenience interface starting from the caller's exact configuration.

    theorem traceAt_fromTapes (tape : Fin 5 → K) (distinct : Function.Injective tape)
        (labels : Label → Λ) (exit : Option Λ)
        (target : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet

65. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.machine line 637

    Source documentation

    The complete construction has five Boolean tapes, nine control labels, and one optional-bit register. No table data appears in its finite state.

    def machine : FinTM2 where
    …

66. def OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookupClean.machineInTime line 650

    Source documentation

    The generic trace instantiates the concrete finite machine, with the same linear bound and completely cleaned working copy.

    def machineInTime (base : Fin 5 → List Bool) (values : List Nat)
        (tableWord : base 0 = encodeWords values) (scratchEmpty : base 4 = [])
        (index value : Nat) (selected : values[index]? = some value)
        (indexSuffix output : List Bool) (register : Option Bool) :
        StateTransition.EvalsToInTime machine.step
          ⟨some (.run .copyFirst), ((), register),
            MachinePreservingLookup.initialTapes id base index indexSuffix [] output⟩
          (some ⟨none, ((), none),
            MachinePreservingLookup.initialTapes id base 0 indexSuffix []
              (encodeWord value ++ output)⟩)
          (timePolynomial.eval (encodeWords values).length) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachinePreservingLookup.initialTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord

67. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.Alphabet line 672
68. def OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendTapes line 674
69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendTapes_source line 678
70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendTapes_destination line 683
71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendTapes_other line 687
72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendTapes_scratch line 692
73. def OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.firstTapes_inline_MachineAppendAt line 699
74. def OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.secondTapes_inline_MachineAppendAt line 702
75. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.finalTapes_eq_inline_MachineAppendAt line 706
76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendTrace line 728
77. def OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.appendInTime line 799

    Source documentation

    The timed witness stores the exact three-loop transition count.

    def appendInTime (source destination scratch : K)
        (sourceDestination : source ≠ destination) (sourceScratch : source ≠ scratch)
        (destinationScratch : destination ≠ scratch)
        (fallback : β) (firstLabel secondLabel thirdLabel : Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K) β) Λ (σ × Option β))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineAppendAt.Alphabet