OAI/Computability/MaxCut/Machines/Alphabet.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet line 25
2. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits line 28

   Source documentation

   This literal is independent of the graph input.

   def equalityBits : List Bool :=
   …

3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits_length_le line 31
4. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits line 34
5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_length line 37
6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_eq_row line 42
7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation line 57

   Source documentation

   The address supplied to the physical lookup is the actual port-table row.

   theorem selected_rotation {n q : Nat} (table : ExpanderTables.Table n q)
       (i : Fin n) (p : Fin q) :
       (ExpanderTableWords.rotationWords table)[q * i.val + p.val]? =
         some (q * (ExpanderTables.lookup table (i, p)).1.val +
           (ExpanderTables.lookup table (i, p)).2.val) := by
   …

8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_div line 64
9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_mod line 72
10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotationLookupTrace line 81

    Source documentation

    A direct instantiation of the real affine getter on the actual rotor words.

    theorem rotationLookupTrace {n q : Nat} (table : ExpanderTables.Table n q)
        (i : Fin n) (p : Fin q) (source : K) (tape : Fin 5 → K)
        (distinct : Function.Injective tape) (outside : ∀ a, source ≠ tape a)
        (labels : MachineAffineLookup.Label → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet

11. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.FinishLabel line 104
12. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields line 112

    Source documentation

    Tail, selected global target, returned port, scratch, reverse field, equality field, row buffer, accumulated output.

    def finishFields (tape : Fin 8 → K) : Fin 3 → K := fun i =>
    …

13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_zero line 116
14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_one line 118
15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_two line 120
16. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishInstruction line 124

    Source documentation

    The return port is copied from its physical unary tape before fixed-slope arithmetic adds the actual selected global target.

    def finishInstruction (q : Nat) (tape : Fin 8 → K) (labels : FinishLabel → Λ)
        (exit : Option Λ) : FinishLabel → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.FinishLabel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet

17. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps line 143
18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps_le line 148
19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.joinTrace_inline_MachineRegularInternalRow line 155
20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.finishTrace line 162

    Source documentation

    Actual final arithmetic, full relation emission, row append and cleanup. The only changed tape is the accumulated output; both physical target fields and all metadata are preserved. No execution hypothesis is supplied.

    theorem finishTrace (q : Nat) (tape : Fin 8 → K) (distinct : Function.Injective tape)
        (labels : FinishLabel → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.FinishLabel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet

21. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.RotorLabel line 277
22. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes line 282
23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_injective line 286
24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_outside line 294
25. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction line 301
26. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorFinalTapes line 312
27. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps line 322
28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorTrace line 329

    Source documentation

    The actual stored reverse row is read and physically divided by the fixed degree. Both output fields equal the coordinates of the actual table lookup.

    theorem rotorTrace {n q : Nat} (positive : 0 < q) (table : ExpanderTables.Table n q)
        (i : Fin n) (p : Fin q) (tape : Fin 8 → K) (distinct : Function.Injective tape)
        (labels : RotorLabel q → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (MachineFixedDivMod.State σ q))
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.RotorLabel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineFixedDivMod.State

29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps_le line 408
30. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape line 418
31. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList line 423
32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_getElem?_ctorIdx_eq line 426
33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_nodup line 430
34. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 432) line 432
35. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape line 436
36. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet line 437
37. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAlphabet line 439
38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectAlphabet_eq line 441
39. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolWord line 447
40. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes line 452
41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.alphabet_tapes_apply_inline_MachineRegularInternalRow line 455
42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes_eq line 462
43. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectState line 470
44. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectStateEquiv line 472
45. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectScratch line 478
46. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectQuery line 479
47. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectOutput line 480
48. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.compareSlots line 482
49. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.subtractSlots line 486
50. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy line 490
51. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList line 494
52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_getElem?_ctorIdx_eq line 497
53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_nodup line 501
54. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 503) line 503
55. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd line 507
56. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList line 511
57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_getElem?_ctorIdx_eq line 513
58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_nodup line 517
59. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 519) line 519
60. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage line 523
61. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList line 526
62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_getElem?_ctorIdx_eq line 528
63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_nodup line 532
64. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 534) line 534
65. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectControl line 538
66. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectLabel line 547
67. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.copySource line 549
68. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.copyDestination line 555
69. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.afterCopy line 561
70. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.addSource line 568
71. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.afterAdd line 572
72. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.cleanupTape line 576
73. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.afterCleanup line 579
74. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectControl line 582
75. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.rawSelectProgram line 606

    Source documentation

    All arithmetic is on extra tapes. The old-dart branch literally contains the shared selector program, with only static tape, label and state transport.

    def rawSelectProgram : SelectLabel → TM2.Stmt RawSelectAlphabet SelectLabel (SelectState σ) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectLabel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectState

76. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram line 612
77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram_control line 615
78. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState line 627
79. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectComparisonTrace line 632

    Source documentation

    One physical strict comparison decides the branch and preserves both input indices. In particular equality belongs to the dummy branch.

    theorem selectComparisonTrace (base : SelectTape → List Bool) (j k : Nat)
        (hj : base (.inr .localIndex) = encodeWord j)
        (hk : base (.inr .cloudSize) = encodeWord k)
        (hl : base (.inr .savedLeft) = []) (hr : base (.inr .savedRight) = [])
        (ambient : σ) (register : Option Bool) :
        (advance (TM2.step selectProgram))^[MachineUnaryLessAt.steps j k + 1]
          (some ⟨some (.inr (.compare .scan)), selectCleanState ambient register, base⟩) =
          some ⟨some (.inr (.copy (if j < k then .oldLocal else .dummyLocal) .seed)),
            selectCleanState ambient none, base⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryLessAt.steps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState

80. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCopyTrace line 655

    Source documentation

    Actual preserving unary copy used to construct both the selector query and the dummy-index operands.

    theorem selectCopyTrace (kind : SelectCopy) (base : SelectTape → List Bool)
        (a : Nat) (hword : base (copySource kind) = encodeWord a)
        (hscratch : base selectScratch = []) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step selectProgram))^[2 * (a + 1) + 1]
          (some ⟨some (.inr (.copy kind .seed)), selectCleanState ambient register, base⟩) =
          some ⟨some (afterCopy kind), selectCleanState ambient none,
            Function.update base (copyDestination kind)
              (encodeWord a ++ base (copyDestination kind))⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.copySource, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectScratch, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.afterCopy, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.copyDestination

81. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectAddTrace line 676

    Source documentation

    The two runtime addends are read physically; no input-dependent offset is captured by a single finite instruction.

    theorem selectAddTrace (kind : SelectAdd) (base : SelectTape → List Bool)
        (a b : Nat) (hword : base (addSource kind) = encodeWord a)
        (houtput : base selectOutput = encodeWord b) (hscratch : base selectScratch = [])
        (ambient : σ) :
        (advance (TM2.step selectProgram))^[2 * (a + 1)]
          (some ⟨some (.inr (.add kind .scan)), selectCleanState ambient none, base⟩) =
          some ⟨some (afterAdd kind), selectCleanState ambient none,
            Function.update base selectOutput (encodeWord (a + b))⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.addSource, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectOutput, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectScratch, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.afterAdd

82. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape line 702
83. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreState line 703
84. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.CoreLabel line 707
85. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.coreEntry line 714
86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCloudTrace line 718

    Source documentation

    The shared cloud-selector trace is preserved exactly by static tape, register and alphabet transport. These transports add no transition.

    theorem selectCloudTrace (t : GraphTables.Table) (v : Fin t.vertices)
        (i : Fin (PreprocessingCloudIndex.cloudSize t v))
        (extra : SelectExtraTape → List Bool) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step selectProgram))^[MachineCloudSelect.cloudSelectSteps t v i []]
          (some ⟨some (.inl (.inr .initialize)), selectCleanState ambient register,
            selectToBoolTapes (MachineEmbedding.tapes
              (MachineCloudSelect.memory (GraphTables.tableBits t) []
                (MachineCloudSelect.queryWord v.val i.val []) [] [] [] []) extra)⟩) =
          some ⟨some (.inr (.cleanup 0)), selectCleanState ambient none,
            selectToBoolTapes (MachineEmbedding.tapes
              (MachineCloudSelect.memory (GraphTables.tableBits t) []
                (MachineCloudSelect.queryWord v.val i.val []) [] [] []
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes, OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.tapes, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.memory, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.queryWord

87. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectExtraMemory line 750
88. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory line 763
89. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_query line 770
90. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_output line 774
91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_scratch line 778
92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_extra line 782
93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_query line 787
94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_output line 799
95. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_local line 811
96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_size line 823
97. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_left line 835
98. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_right line 847
99. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanupTrace line 859
100. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.oldSelectSteps line 902
101. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectOldTrace line 907
102. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps line 951
103. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps_eq line 955
104. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectDummyTrace line 962

     Source documentation

     The dummy branch uses the actual truncating-subtraction scan on copied operands. The original local index, cloud size, prefix and dart count survive.

     theorem selectDummyTrace (graph : List Bool) (j v k o m : Nat) (hk : k ≤ j)
         (ambient : σ) :
         (advance (TM2.step selectProgram))^[dummySelectSteps j k o m]
           (some ⟨some (.inr (.copy .dummyLocal .seed)), selectCleanState ambient none,
             selectMemory graph j v k o m [] [] [] [] [] []⟩) =
           some ⟨none, selectCleanState ambient none,
             selectMemory graph j v k o m [] (encodeWord (m + o + (j - k))) [] [] [] []⟩ := by
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory, OAI.MaxCutGames.Foundations.Complexity.encodeWord

105. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps line 1021
106. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectionTrace line 1031

     Source documentation

     The entire actual selector program, with both runtime branches and the same clean final frame. Metadata values are premises about physical tapes.

     theorem selectionTrace (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
         (v : Fin t.vertices) (i : Fin (PreprocessingCloudIndex.cloudSize t v + padding v))
         (ambient : σ) (register : Option Bool) :
         (advance (TM2.step selectProgram))^[selectionSteps t padding v i]
           (some ⟨some (.inr (.compare .scan)), selectCleanState ambient register,
             selectMemory (GraphTables.tableBits t) i.val v.val
               (PreprocessingCloudIndex.cloudSize t v)
               (PreprocessingPaddingOffsets.offset padding v.val) t.darts [] [] [] [] [] []⟩) =
           some ⟨none, selectCleanState ambient none,
             selectMemory (GraphTables.tableBits t) i.val v.val
               (PreprocessingCloudIndex.cloudSize t v)
               (PreprocessingPaddingOffsets.offset padding v.val) t.darts []
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory