OAI/Computability/UniqueGames/PCP/SourceHeaderCounts.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.Label line 21
2. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.start line 23
3. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.inner line 24
4. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.finish line 25
5. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.word line 27
6. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.indices line 30
7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.indices_nodup line 34
8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.word_slot line 38
9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.control_not_mem line 43
10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.digit_mem line 49
11. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.prepared line 54
12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_control line 58
13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_digit line 64
14. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.clear_result line 71
15. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.statement line 90
16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.steps line 100
17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.trace line 103
18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Eval.inTime line 145
19. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.leftValue line 163
20. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.rightValue line 164
21. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.dummyValue line 165
22. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.bitValue line 166
23. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.occurrenceValue line 167
24. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Kind line 170
25. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Kind.enumList line 174
26. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_getElem?_ctorIdx_eq line 176
27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_nodup line 180
28. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.(instance at line 182) line 182
29. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.polynomial line 186
30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.polynomial_left_eval line 192
31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.polynomial_right_eval line 194
32. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.polynomial_occurrences_eval line 196
33. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.bitValue_eq_nBits line 200
34. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.occurrenceValue_eq_length line 205
35. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Control line 216
36. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Control.enumList line 221
37. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Control.enumList_getElem?_ctorIdx_eq line 224
38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Control.enumList_nodup line 228
39. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.(instance at line 230) line 230
40. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Coefficients line 234
41. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Layout line 239
42. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.coefficientBlock line 241
43. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.inputControl line 248
44. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.outputControl line 251
45. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.controlSlots line 254
46. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.localSlots line 262
47. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.control line 281
48. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots line 283
49. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots_radix line 287
50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots_accA line 289
51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots_accB line 291
52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots_destination line 293
53. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots_counter line 295
54. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots_scratch line 297
55. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalSlots_digit line 299
56. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.control_eq_iff line 303
57. structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Clean line 307
58. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Label line 319
59. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalStart line 325
60. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.afterEval line 327
61. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.statement line 332
62. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.resultTapes line 353
63. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.steps line 360
64. structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.WorkClean line 365
65. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Clean.work line 373
66. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.WorkClean.update_output line 377
67. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalPhaseTrace line 387
68. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.trace_trans line 408
69. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.trace line 415

    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.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.statement, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.control, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Clean, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.steps, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalStart, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.resultTapes

70. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.timePolynomial line 519
71. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.steps_le_timePolynomial line 526
72. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.inTime line 547
73. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.inPolynomialTime line 562
74. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.formulaInTime line 579

    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.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.statement, OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.control, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Clean, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.evalStart, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.resultTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.timePolynomial

75. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_frame line 594
76. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_left line 600
77. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_occurrences line 603
78. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_dummy line 606
79. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_bits line 609
80. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_variableCount line 612
81. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_clauseCount line 615
82. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.result_source_headers line 619
83. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.program line 628
84. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.machine line 633

    Source documentation

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

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

85. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.afterInitializationInTime line 646

    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.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.Tape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.control, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.variableHeader, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.clauseHeader, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.statement, OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceHeaderCounts.Clean, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.outputTapes