OAI/Computability/MaxCut/Machines/MachineExpanderTableProgram.lean

GitHub source file

171 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape line 11
2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList line 15
3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_getElem?_ctorIdx_eq line 17
4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_nodup line 21
5. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.(instance at line 23) line 23
6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Tape line 27
7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet line 29
8. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.alphabetFintype line 33
9. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel line 36
10. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList line 40
11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_getElem?_ctorIdx_eq line 43
12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_nodup line 47
13. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.(instance at line 49) line 49
14. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Label line 53
15. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Position line 54
16. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State line 55
17. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.RowStatePrefix line 56
18. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.guardStates line 60

    Source documentation

    Static movement of the bit register to the last product coordinate.

    def guardStates (ρ : Type) (d : Nat) :
        ((RowStatePrefix ρ d × Position d) × Option Bool) ≃ State ρ d where
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.RowStatePrefix, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Position, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State

19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.guardStates_apply line 67
20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.guardStates_symm_apply line 71
21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowFactor_pos line 74
22. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.zeroPosition line 78
23. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.nextPosition line 81
24. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.positionPair line 84
25. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller line 87
26. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryState line 90

    Source documentation

    A fresh row call, with its residue and bit register reset.

    def boundaryState {ρ : Type} {d : Nat} (positive : 0 < d)
        (H : Table (cloudSize d) d) (ambient : ρ) (p : Position d) : State ρ d :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Position, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State

27. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.initialState line 95
28. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.prepareState line 99
29. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.resetState line 103
30. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister line 107
31. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.advancePositionState line 110
32. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.resetPositionState line 113
33. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexGuardCore line 119

    Source documentation

    The unary guard specialized to the concrete extra tape. The zero delimiter is retained; both branches clear the bit register. Its dependent alphabet is the same alphabet used by the embedded row program.

    def vertexGuardCore {ρ : Type} {d : Nat} :
        TM2.Stmt Alphabet (Label d) ((RowStatePrefix ρ d × Position d) × Option Bool) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.RowStatePrefix, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Position

34. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.outerStatement line 131

    Source documentation

    Actual statements for the table loop. No unbounded natural number is stored in the state or evaluated by a state-update function.

    def outerStatement {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d) :
        OuterLabel → TM2.Stmt Alphabet (Label d) (State ρ d)
      | .initialize =>
        .push (.inl .inputVertex) (fun _ => false)
          (.load (resetState positive H) (.goto fun _ => .inr .vertexGuard))
      | .vertexGuard => MachineControl.statement id (guardStates ρ d) vertexGuardCore
      | .prepareRow =>
        .load (prepareState positive H) (.goto fun _ => .inl .initialize)
      | .afterRow =>
        .branch (fun s => decide (s.2.val + 1 < rowFactor d))
          (.load (advancePositionState positive) (.goto fun _ => .inr .prepareRow))
          (.push (.inl .inputVertex) (fun _ => true)
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.resetState, OAI.MaxCutGames.Foundations.Complexity.MachineControl.statement, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.guardStates, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexGuardCore, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.prepareState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.advancePositionState

35. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowReturn line 151
36. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program line 155

    Source documentation

    The complete finite program. The vertex count is supplied on a tape, while the small table and all finite control types depend only on fixed d.

    def program {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d) :
        Label d → TM2.Stmt Alphabet (Label d) (State ρ d) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State

37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program_row line 160
38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program_outer line 166
39. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowExecution line 172

    Source documentation

    Every transition of an actual row run embeds with its original cost, preserving the position and both extra tapes, including its return jump.

    def rowExecution {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d)
        (position : Position d) (extra : ExtraTape → List Bool)
        {a b : TM2.Cfg (fun _ : MachineExpanderRow.Tape => Bool)
          (MachineExpanderRow.Label d) (MachineExpanderRow.State ρ d)} {budget : Nat}
        (execution : StateTransition.EvalsToInTime
          (TM2.step (MachineExpanderRow.program positive H)) a (some b) budget) :
        StateTransition.EvalsToInTime (TM2.step (program positive H))
          (MachineEmbedding.configuration (rowReturn d) position extra a)
          (some (MachineEmbedding.configuration (rowReturn d) position extra b)) budget :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Position, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderRow.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineEmbedding.configuration, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowReturn

40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowExecution_steps line 184
41. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowTapes line 192
42. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.extraTapes line 198
43. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes line 202
44. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.initialTapes line 208

    Source documentation

    Before initialization, only the old table and remaining-count word are populated. The program itself creates the initial vertex delimiter.

    def initialTapes (vertices : Nat) (oldTable countSuffix : List Bool) :
        (tape : Tape) → List (Alphabet tape) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.Alphabet

45. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.finalTapes line 214
46. def OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.tapes line 226
47. def OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.statement line 228
48. def OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration line 230
49. def OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.program line 232
50. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.castStatement line 235
51. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.castConfiguration line 236
52. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.castProgram line 237
53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.tapes_rfl line 239
54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.statement_rfl line 240
55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_rfl line 241
56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.program_rfl line 242
57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.program_apply line 244
58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.statement_roundtrip line 247
59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.statement_symm_roundtrip line 250
60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_roundtrip line 253
61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_symm_roundtrip line 256
62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.program_roundtrip line 259
63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.program_symm_roundtrip line 262
64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.tapes_roundtrip line 265
65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.tapes_symm_roundtrip line 268
66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_label line 271
67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_state line 274
68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_tapes line 277
69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_mk line 280
70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.map_configuration_rfl line 284
71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.stepAux_simulation line 289
72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.step_simulation line 294
73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.trace_transport line 301

    Source documentation

    Exact conjugacy of every finite trace, including a none endpoint.

    theorem trace_transport (h : Γ = Δ) (source : Λ → Stmt Γ Λ σ)
        (n : Nat) (start : Option (Cfg Γ Λ σ)) :
        (MachineComposition.advance (step (program h source)))^[n]
          (start.map (configuration h)) =
          ((MachineComposition.advance (step source))^[n] start).map (configuration h) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.program, OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration

74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.successfulTrace line 309
75. def OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime line 317
76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime_steps line 329
77. def OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime line 334
78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime_steps line 340
79. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape line 352
80. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList line 356
81. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_getElem?_ctorIdx_eq line 359
82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_nodup line 363
83. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 365) line 365
84. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape line 369
85. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet line 370
86. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet line 372
87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.alphabet_eq line 376

    Source documentation

    All physical tapes contain Booleans. This equality changes the static type presentation only; no runtime symbol conversion is performed.

    theorem alphabet_eq : Alphabet = BoolAlphabet := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet

88. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.alphabetFintype line 382
89. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase line 386
90. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList line 390
91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_getElem?_ctorIdx_eq line 392
92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_nodup line 396
93. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 398) line 398
94. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel line 402
95. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList line 406
96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_getElem?_ctorIdx_eq line 408
97. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_nodup line 412
98. instance OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 414) line 414
99. inductive OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.OuterLabel line 418
100. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Label line 426
101. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State line 427
102. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient line 428
103. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.registerStates line 431
104. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.registerStates_apply line 438
105. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.registerStates_symm_apply line 442
106. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller line 445
107. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialState line 448
108. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.normalizeState line 452
109. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding line 456
110. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding_eq_family line 459

     Source documentation

     The literal used by initialization is exactly the actual family's base.

     theorem initialEncoding_eq_family {d : Nat} (H : Table (cloudSize d) d) :
         initialEncoding d = encodeWords (rotationWords (family H 0)) := rfl

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.MaxCutGames.Foundations.Complexity.encodeWords

111. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableTape line 462
112. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.inputVertexTape line 463
113. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.vertexCountTape line 464
114. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.resultTape line 465
115. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineSource line 467
116. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineDestination line 471
117. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineCoefficient line 475
118. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineExit line 479
119. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.affineStatement line 483
120. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.drainStatement line 501
121. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolOuterStatement line 511

     Source documentation

     Uniform-alphabet presentation of the actual outer code. All arithmetic parameters here are fixed program constants; runtime sizes are scanned.

     def boolOuterStatement {d : Nat} (positive : 0 < d) (H : Table (cloudSize d) d) :
         OuterLabel → TM2.Stmt BoolAlphabet (Label d) (State ρ d)
       | .initialize =>
         Reduction.MachineSubstitution.pushWord tableTape (initialEncoding d).reverse
           (Reduction.MachineSubstitution.pushWord (.inr .currentSize) (encodeWord 1).reverse
             (.load (normalizeState positive H)
               (.goto fun _ => .inr .levelGuard)))
       | .levelGuard =>
         MachineControl.statement id (registerStates ρ d)
           (MachineUnaryCounter.guard (K := Tape) (Λ := Label d) (σ := RegisterAmbient ρ d)
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.OuterLabel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Reduction.MachineSubstitution.pushWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.normalizeState, OAI.MaxCutGames.Foundations.Complexity.MachineControl.statement, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.registerStates, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guard, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient

122. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.outerStatement line 540
123. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableReturn line 544
124. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program line 546
125. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program_table line 551
126. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program_outer line 558
127. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolView line 562
128. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolView_outer line 566
129. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableExecution line 575
130. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableExecution_steps line 587
131. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableFrame line 596
132. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.extraFrame line 602
133. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes line 607
134. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes line 611
135. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyTapes line 618
136. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolWord line 632
137. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord line 637
138. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes line 642
139. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes line 645
140. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord_boolWord line 648
141. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolWord_toBoolWord line 654
142. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBool_fromBool line 660
143. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.fromBool_toBool line 665
144. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.transport_tapes_apply_inline_MachineExpanderFamilyTapes line 670
145. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_eq_transport line 677
146. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_eq_transport line 685
147. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_update line 693
148. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_update line 702
149. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.configuration_fromBool line 712
150. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.configuration_toBool line 718
151. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.controlStatementInverse line 739
152. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.controlTrace line 747

     Source documentation

     Static state-coordinate transport preserves every actual transition.

     theorem controlTrace {K Λ σ τ : Type} {Γ : K → Type} [DecidableEq K]
         (states : σ ≃ τ) (target : Λ → TM2.Stmt Γ Λ τ)
         (n : Nat) (start finish : TM2.Cfg Γ Λ σ)
         (run : (advance (TM2.step (MachineControl.program (Equiv.refl Λ) states.symm target)))^[n]
           (some start) = some finish) :
         (advance (TM2.step target))^[n]
           (some (MachineControl.configuration id states start)) =
           some (MachineControl.configuration id states finish) := by
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineControl.program, OAI.MaxCutGames.Foundations.Complexity.MachineControl.configuration

153. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.controlDrainTrace line 771
154. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.controlTransferTrace line 790
155. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister line 815
156. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.registerStates_reset line 818
157. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_idempotent line 822
158. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller_clearRegister line 825
159. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_position line 828
160. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_register line 831
161. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolTraceActual line 837

     Source documentation

     The Boolean view is the same actual program under alphabet equality.

     theorem boolTraceActual (positive : 0 < d) (H : Table (cloudSize d) d)
         (growth : 1 < cloudSize d) (n : Nat)
         (start finish : TM2.Cfg BoolAlphabet (Label d) (State ρ d))
         (run : (advance (TM2.step (boolView positive H growth)))^[n] (some start) = some finish) :
         (advance (TM2.step (program positive H growth)))^[n]
           (some (MachineAlphabetTransport.configuration alphabet_eq.symm start)) =
           some (MachineAlphabetTransport.configuration alphabet_eq.symm finish) := by
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolView, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration

162. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.drainBoolTrace line 848
163. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.transferBoolTrace line 865
164. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installedTapes line 889

     Source documentation

     Only these four tape words change during installation.

     def installedTapes (base : Tape → List Bool) (newWord : List Bool) : Tape → List Bool :=
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape

165. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cleanedCounterTapes line 896
166. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installTableBoolTrace line 899
167. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersBoolTrace line 958
168. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installTableTrace line 978

     Source documentation

     Actual dependent-alphabet trace for draining the old table, installing the new forward table by two physical reversals, and clearing the old size word.

     theorem installTableTrace (positive : 0 < d) (H : Table (cloudSize d) d)
         (growth : 1 < cloudSize d) (base : (tape : Tape) → List (Alphabet tape))
         (newWord : List Bool) (resultWord : toBoolTapes base resultTape = newWord)
         (reverseEmpty : toBoolTapes base (.inr .tableReverse) = []) (state : State ρ d) :
         (advance (TM2.step (program positive H growth)))^[
             (toBoolTapes base tableTape).length + 2 * newWord.length +
               (toBoolTapes base (.inr .currentSize)).length + 4]
           (some ⟨some (.inr .clearOldTable), state, base⟩) =
           some ⟨some (.inr (.affine .multiplySize .seed)), clearRegister state,
             fromBoolTapes (installedTapes (toBoolTapes base) newWord)⟩ := by
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.resultTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installedTapes

169. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersTrace line 993

     Source documentation

     After the checked affine phase, both table-loop counters are physically drained and the actual family level guard is reached.

     theorem cleanupCountersTrace (positive : 0 < d) (H : Table (cloudSize d) d)
         (growth : 1 < cloudSize d) (base : (tape : Tape) → List (Alphabet tape))
         (state : State ρ d) :
         (advance (TM2.step (program positive H growth)))^[
             (toBoolTapes base inputVertexTape).length + (toBoolTapes base vertexCountTape).length + 2]
           (some ⟨some (.inr .drainInputVertex), state, base⟩) =
           some ⟨some (.inr .levelGuard), clearRegister state,
             fromBoolTapes (cleanedCounterTapes (toBoolTapes base))⟩ := by
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.inputVertexTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.vertexCountTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cleanedCounterTapes

170. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installTableInTime line 1004
171. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersInTime line 1019