OAI/Computability/MaxCut/Machines/MachineRegularOriginalBody.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.Tape line 22
2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.Alphabet line 23
3. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.CoreState line 24
4. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.MetaState line 25
5. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.FamilyState line 26
6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.State line 27
7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.Data line 28
8. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable line 29
9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive line 31
10. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.readyState line 34
11. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTape line 38
12. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView line 42
13. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyTape line 47
14. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyView line 51
15. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView line 56
16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_left line 60
17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_right line 63
18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_left line 71
19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_right line 74
20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_left line 82
21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_right line 84
22. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataStates line 90
23. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyStates line 96
24. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexStates line 97
25. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.Label line 100
26. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.entry line 107
27. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearTape line 109
28. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearEntry line 113
29. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearSource line 116
30. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSource line 119
31. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.program line 123
32. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.frame line 134
33. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame line 139
34. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.cfg line 142
35. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.initialData line 145
36. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataData line 158
37. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyData line 161
38. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits line 166
39. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData line 169
40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.joinTrace_inline_MachineRegularOriginalBody line 173
41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataPlacement line 177
42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTrace line 187

    Source documentation

    Genuine metadata trace transported with all other finite registers and private family tapes preserved.

    theorem metadataTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
        (output : List Bool) :
        (advance (TM2.step (program H)))^[MachineRegularMetadata.totalTime t e]
          (some (cfg H (some entry) (initialData t e output))) =
          some (cfg H (some (.family .start)) (metadataData t e output)) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.initialData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataData

43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyPlacement line 203
44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyResultPlacement line 211
45. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyExecution line 224
46. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familySteps line 229
47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyTrace line 235

    Source documentation

    Family work is performed on its physical tapes and produces the rotor from the previously computed unary cloud size.

    theorem familyTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
        (output : List Bool) :
        (advance (TM2.step (program H)))^[familySteps H t e output]
          (some (cfg H (some (.family .start)) (metadataData t e output))) =
          some (cfg H (some (.vertex (MachineRegularVertexBlock.originalEntry
            internalDegree degree_positive))) (familyData H t e output)) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familySteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyData

48. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearMemory line 253

    Source documentation

    Seven real drain loops, including the complete materialized rotor.

    def clearMemory (base : Tape → List Bool) : Nat → Tape → List Bool
      | 0 => base
      | k + 1 => if h : k < 7 then
          Function.update (clearMemory base k) (clearTape ⟨k, h⟩) [] else clearMemory base k

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearTape

49. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearSteps line 258
50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.identityPlacement_inline_MachineRegularOriginalBody line 263
51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.drainTrace line 266
52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearPrefixTrace line 282
53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearTrace line 297
54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearFrame line 303
55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame_eq line 321
56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData_eq line 341
57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexPlacement line 345
58. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps line 356
59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexTrace line 362

    Source documentation

    Every internal port and the inherited original row are emitted by their actual checked row machines, using the rotor just materialized on tape 7.

    theorem vertexTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
        (output : List Bool) :
        (advance (TM2.step (program H)))^[vertexSteps H t e output]
          (some (cfg H (some (.vertex (MachineRegularVertexBlock.originalEntry
            internalDegree degree_positive))) (familyData H t e output))) =
          some (cfg H (clearEntry 0) (emittedData H t e output)) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.familyData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.clearEntry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData

60. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps line 381
61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.originalTrace line 388

    Source documentation

    Complete execution of one original-vertex iteration, including physical cleanup of all seven retained metadata fields. The global index is preserved.

    theorem originalTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
        (output : List Bool) :
        (advance (TM2.step (program H)))^[totalSteps H t e output]
          (some (cfg H (some entry) (initialData t e output))) =
          some (cfg H none (initialData t e (output ++ emittedBits H t e))) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.initialData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits

62. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.originalExecution line 406

    Source documentation

    Exact execution witness. Its stored count is derived from the four actual phases; a polynomial estimate is supplied separately.

    noncomputable def originalExecution (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
        (output : List Bool) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          (cfg H (some entry) (initialData t e output))
          (some (cfg H none (initialData t e (output ++ emittedBits H t e))))
          (totalSteps H t e output) where
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.initialData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps

63. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Tape line 424
64. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.State line 425
65. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet line 426
66. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.sumDecidableEq_inline_MachineRegularOwnerCleanup line 429

    Source documentation

    Constructor-by-constructor equality for a fixed sum of tape alphabets.

    private def sumDecidableEq_inline_MachineRegularOwnerCleanup {A B : Type} (left : DecidableEq A) (right : DecidableEq B) :
        DecidableEq (A ⊕ B)
      | .inl a, .inl b => match left a b with
          | .isTrue h => .isTrue (congrArg (Sum.inl : A → A ⊕ B) h)
          | .isFalse h => .isFalse (fun e => h (Sum.inl.inj e))
      | .inr a, .inr b => match right a b with
          | .isTrue h => .isTrue (congrArg (Sum.inr : B → A ⊕ B) h)
          | .isFalse h => .isFalse (fun e => h (Sum.inr.inj e))
      | .inl _, .inr _ => .isFalse (by intro h; cases h)
      | .inr _, .inl _ => .isFalse (by intro h; cases h)
    
    /-- Every equality decision is explicitly assembled from fixed finite leaves.

67. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeDecidableEq line 442

    Source documentation

    Every equality decision is explicitly assembled from fixed finite leaves. There is no classical decision or recursive typeclass search on the tape sum.

    instance tapeDecidableEq : DecidableEq Tape :=
    …

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

68. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeBEq line 456

    Source documentation

    List membership uses Boolean equality in Lean 4.33. These instances are the explicit Boolean view of the executable equality procedure above.

    instance tapeBEq : BEq Tape where
    …

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

69. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeLawfulBEq line 459
70. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeFintype line 463
71. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.core line 470
72. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.localRank line 471
73. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.count line 472
74. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape line 473
75. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.rotor line 474
76. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding line 475
77. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.level line 476
78. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel line 477
79. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.scratch line 478
80. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes line 481

    Source documentation

    Every name is distinct, so the exact drain cost uses the entry lengths.

    def cleanupTapes : List Tape := [localRank, count, rotor, padding, level, dummyFuel]

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.localRank, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.count, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.rotor, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.level, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel

81. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Label line 483
82. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.entry line 489
83. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry line 491
84. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.instruction line 495

    Source documentation

    Coefficient one, no seed: the destination already contains its offset.

    def instruction (labels : Label → Λ) (exit : Option Λ) :
        Label → TM2.Stmt Alphabet Λ State
      | .scan => MachineUnaryAffineAt.scan padding scratch prefixTape 1
          (labels .scan) (labels .restore)
      | .restore => Reduction.MachineTransfer.loopAt scratch padding id false
          (labels .restore) (cleanupEntry labels exit)
      | .drain l => MachineDrainMany.instruction cleanupTapes
          (fun l => labels (.drain l)) exit l

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.State, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.scan, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.scratch, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.instruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes

85. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.afterAddition line 504
86. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes line 507
87. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.steps line 510
88. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_apply line 513
89. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_prefix line 520
90. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_empty line 525
91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_other line 529
92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_scratch line 534
93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.drainSteps_eq line 540
94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.additionTraceAt line 546
95. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.traceAt line 573

    Source documentation

    Complete physical addition followed by the six exact drain loops. No phase run or precomputed sum word is supplied as a hypothesis.

    theorem traceAt (labels : Label → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt Alphabet Λ State)
        (code : ∀ l, program (labels l) = instruction labels exit l)
        (base : Tape → List Bool) (d o : Nat)
        (paddingWord : base padding = encodeWord d)
        (prefixWord : base prefixTape = encodeWord o)
        (scratchEmpty : base scratch = [])
        (ambient : MachineRegularOriginalBody.State) (register : Option Bool) :
        (advance (TM2.step program))^[steps base d]
          (some ⟨some (labels entry), (ambient, register), base⟩) =
          some ⟨exit, (ambient, none), finalTapes base d o⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.instruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.scratch, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.steps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes

96. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerCleanup.executionAt line 593