OAI/Computability/MaxCut/PCP/HeaderCounts.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.Label line 19
2. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.start line 21
3. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.inner line 22
4. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.finish line 23
5. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.word line 25
6. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices line 28
7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices_nodup line 32
8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.word_slot line 36
9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.control_not_mem line 41
10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.digit_mem line 47
11. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared line 52
12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_control line 56
13. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_digit line 62
14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.clear_result line 69
15. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.statement line 88
16. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.steps line 98
17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.trace line 101
18. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Eval.inTime line 143
19. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.leftValue line 161
20. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.rightValue line 162
21. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.dummyValue line 163
22. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.bitValue line 164
23. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue line 165
24. inductive OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Kind line 168
25. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList line 171
26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_getElem?_ctorIdx_eq line 173
27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_nodup line 177
28. instance OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 179) line 179
29. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.polynomial line 183
30. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.polynomial_left_eval line 189
31. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.polynomial_right_eval line 191
32. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.polynomial_occurrences_eval line 193
33. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.bitValue_eq_nBits line 197
34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue_eq_length line 202
35. inductive OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Control line 213
36. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList line 218
37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList_getElem?_ctorIdx_eq line 222
38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList_nodup line 226
39. instance OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 228) line 228
40. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Coefficients line 232
41. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Layout line 237
42. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.coefficientBlock line 239
43. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.inputControl line 246
44. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.outputControl line 249
45. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.controlSlots line 252
46. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.localSlots line 260
47. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.control line 279
48. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots line 281
49. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_radix line 285
50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accA line 287
51. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accB line 289
52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_destination line 291
53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_counter line 293
54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_scratch line 295
55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_digit line 297
56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.control_eq_iff line 301
57. structure OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Clean line 305
58. inductive OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Label line 317
59. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalStart line 323
60. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.afterEval line 325
61. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.statement line 330
62. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.resultTapes line 351
63. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.steps line 358
64. structure OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.WorkClean line 363
65. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Clean.work line 371
66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.WorkClean.update_output line 375
67. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalPhaseTrace line 385
68. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.trace_trans_inline_SourceHeaderCounts line 406
69. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.trace line 413

    Source documentation

    The actual header program preserves its two operands and every caller frame. The four retained outputs are left-block size, dummy index, bit count, and occurrence count. The temporary and all coefficient/work tapes are restored.

    theorem trace (slots : Layout u D ↪ K) (labels : Label u D → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ l, program (labels l) = statement slots labels exit l)
        (base : K → List Bool) (n m : Nat)
        (hn : base (control slots .variableCount) = encodeWord n)
        (hm : base (control slots .clauseCount) = encodeWord m)
        (clean : Clean slots base) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[steps u D n m]
          (some ⟨some (labels (evalStart .left)), ((ambient, ()), register), base⟩) =
          some ⟨exit, ((ambient, ()), none), resultTapes slots base n m⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Label, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.program, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.statement, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.control, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Clean, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.steps, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalStart, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.resultTapes

70. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.timePolynomial line 517
71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.steps_le_timePolynomial line 524
72. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.inTime line 545
73. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.inPolynomialTime line 560
74. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.formulaInTime line 577

    Source documentation

    Formula headers supply the operand bounds for the actual transition count.

    def formulaInTime (slots : Layout u D ↪ K) (labels : Label u D → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ l, program (labels l) = statement slots labels exit l)
        (base : K → List Bool) (F : Target.Formula)
        (hn : base (control slots .variableCount) = encodeWord F.«variables»)
        (hm : base (control slots .clauseCount) = encodeWord F.clauses.length)
        (clean : Clean slots base) (ambient : σ) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labels (evalStart .left)), ((ambient, ()), register), base⟩
          (some ⟨exit, ((ambient, ()), none), resultTapes slots base F.«variables» F.clauses.length⟩)
          ((timePolynomial u D).eval (formulaBits F).length) :=
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Label, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.program, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.statement, OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.control, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Clean, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.evalStart, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.resultTapes, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.timePolynomial

75. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_frame line 592
76. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_left line 598
77. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_occurrences line 601
78. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_dummy line 604
79. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_bits line 607
80. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_variableCount line 610
81. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_clauseCount line 613
82. theorem OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.result_source_headers line 617
83. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.program line 626
84. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.machine line 631

    Source documentation

    A finite machine realizing the header phase on prepared operand registers.

    def machine (u D : Nat) : FinTM2 where
    …

85. def OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.afterInitializationInTime line 644

    Source documentation

    Consume the preserved header registers established by SourceLoopInit. The caller supplies the static placement and empty work registers.

    def afterInitializationInTime {Extra : Type} [DecidableEq Extra]
        (slots : Layout u D ↪ SourceLoopInit.Tape u Extra)
        (hnslot : control slots .variableCount = SourceLoopInit.variableHeader)
        (hmslot : control slots .clauseCount = SourceLoopInit.clauseHeader)
        (labels : Label u D → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : SourceLoopInit.Tape u Extra => Bool) Λ
          (MachineHorner.State σ))
        (atLabels : ∀ l, program (labels l) = statement slots labels exit l)
        (base : SourceLoopInit.Tape u Extra → List Bool) (F : Target.Formula)
        (hn : base SourceLoopInit.variableHeader = [])
        (hm : base SourceLoopInit.clauseHeader = [])
        (clean : Clean slots (SourceLoopInit.outputTapes F base))
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.Tape, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.control, OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.variableHeader, OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.clauseHeader, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Label, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.program, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.statement, OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceHeaderCounts.Clean, OAI.MaxCutGames.Foundations.Hastad.SourceLoopInit.outputTapes

86. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.Extra line 676
87. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.Tape line 677
88. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.State line 678
89. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.outputTape line 680
90. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.accumulatorTape line 681
91. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.headerControl line 683
92. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.headerSlots line 701
93. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.ControlAmbient line 717
94. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.controlStateEquiv line 721

    Source documentation

    Expose the existing arithmetic head register to the odometer and final cleanup. This is a static finite-state equivalence, with no machine steps.

    def controlStateEquiv (u D : Nat) :
        ControlAmbient u D × Option Bool ≃ State u D where
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.ControlAmbient, OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.State

95. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.initialQuery line 730
96. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.initialState line 733
97. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.initialAmbient line 736
98. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.control_initial line 739
99. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.coefficientKeys line 742
100. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.mem_coefficientKeys line 750
101. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.workKeys line 756
102. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.mem_workKeys line 762
103. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.allTapes line 774

     Source documentation

     An explicit tape enumeration, fixed before the input is supplied. It uses constructor lists and increasing finite coefficient indices.

     noncomputable def allTapes (u D : Nat) : List (Tape u D) :=
     …

     Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.Tape

104. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.mem_allTapes line 782
105. def OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.clearKeys line 802
106. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.mem_clearKeys line 807
107. theorem OAI.MaxCutGames.Foundations.Hastad.SourceGeneratorModel.accumulator_ne_output line 812