OAI/Computability/UniqueGames/Machines/MachineExpanderTableProgramLemmas.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.ExtraTape line 15
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList line 19
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_getElem?_ctorIdx_eq line 21
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_nodup line 25
5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.(instance at line 27) line 27
6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Tape line 31
7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet line 33
8. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.alphabetFintype line 37
9. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.OuterLabel line 40
10. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList line 44
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_getElem?_ctorIdx_eq line 47
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_nodup line 51
13. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.(instance at line 53) line 53
14. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Label line 57
15. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Position line 58
16. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State line 59
17. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.RowStatePrefix line 60
18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.guardStates line 64

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.RowStatePrefix, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Position, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State

19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.guardStates_apply line 71
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.guardStates_symm_apply line 75
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowFactor_pos line 78
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.zeroPosition line 82
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.nextPosition line 85
24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.positionPair line 88
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.caller line 91
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryState line 94

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Position, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State

27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.initialState line 99
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.prepareState line 103
29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.resetState line 107
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.clearRegister line 111
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.advancePositionState line 114
32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.resetPositionState line 117
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexGuardCore line 123

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.RowStatePrefix, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Position

34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.outerStatement line 135

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.OuterLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.resetState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.guardStates, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.vertexGuardCore, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.prepareState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.advancePositionState

35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowReturn line 155
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program line 159

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

37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program_row line 164
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program_outer line 170
39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowExecution line 176

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Position, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.ExtraTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowReturn

40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowExecution_steps line 188
41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.rowTapes line 196
42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.extraTapes line 202
43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.boundaryTapes line 206
44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.initialTapes line 212

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.Alphabet

45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderTable.finalTapes line 218
46. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.ExtraTape line 229
47. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList line 233
48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_getElem?_ctorIdx_eq line 236
49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_nodup line 240
50. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.(instance at line 242) line 242
51. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape line 246
52. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet line 247
53. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet line 249
54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.alphabet_eq line 253

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet

55. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.alphabetFintype line 259
56. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffinePhase line 263
57. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList line 267
58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_getElem?_ctorIdx_eq line 269
59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_nodup line 273
60. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.(instance at line 275) line 275
61. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffineLabel line 279
62. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList line 283
63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_getElem?_ctorIdx_eq line 285
64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_nodup line 289
65. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.(instance at line 291) line 291
66. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.OuterLabel line 295
67. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Label line 303
68. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State line 304
69. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient line 305
70. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.registerStates line 308
71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.registerStates_apply line 315
72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.registerStates_symm_apply line 319
73. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller line 322
74. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialState line 325
75. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.normalizeState line 329
76. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialEncoding line 333
77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialEncoding_eq_family line 336

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

78. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableTape line 339
79. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.inputVertexTape line 340
80. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.vertexCountTape line 341
81. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.resultTape line 342
82. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineSource line 344
83. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineDestination line 348
84. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineCoefficient line 352
85. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineExit line 356
86. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.affineStatement line 360
87. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.drainStatement line 378
88. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolOuterStatement line 388

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.OuterLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.pushWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.normalizeState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineControl.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.registerStates, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryCounter.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient

89. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.outerStatement line 417
90. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableReturn line 421
91. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program line 423
92. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program_table line 428
93. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program_outer line 435
94. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolView line 439
95. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolView_outer line 443
96. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableExecution line 452
97. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableExecution_steps line 464
98. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.tableFrame line 473
99. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.extraFrame line 479
100. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boundaryTapes line 484
101. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialTapes line 488
102. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyTapes line 495