OAI/Computability/UniqueGames/Reduction/MachineAddressHeaders.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.Label line 21
2. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.readStart line 25
3. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.readLoop line 26
4. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.destination line 30
5. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.statement line 32
6. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.atReadStart line 46
7. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.atReadLoop line 53
8. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.atReadDone line 61
9. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.copied line 66
10. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.readTapes line 69
11. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes line 74
12. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.clear_readTapes line 78
13. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.readTapes_work line 98
14. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes_other line 103
15. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes_source line 107
16. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes_work line 111
17. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes_n line 114
18. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes_m line 118
19. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.inTime line 123

    Source documentation

    Actual copying, two-field extraction, and complete disposal of the work copy.

    def inTime (slots : Fin 5 ↪ K) (labels : Label → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
        (base : K → List Bool) (n m : Nat) (suffix : List Bool)
        (hinput : base (slots 0) = encodeWords [n, m] ++ suffix)
        (hwork : base (slots 1) = []) (hscratch : base (slots 4) = [])
        (ambient : σ) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labels .copyOut), ((ambient, ()), register), base⟩
          (some ⟨exit, ((ambient, ()), none), resultTapes slots base n m⟩)
          (3 * (base (slots 0)).length + 6) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.Label, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.statement, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes

20. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.baseConstant line 173
21. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.radix line 174
22. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.capacity line 175
23. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.edgeFactor line 176
24. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.edgeCount line 178
25. inductive OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Kind line 182
26. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Kind.enumList line 186
27. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Kind.enumList_getElem?_ctorIdx_eq line 188
28. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Kind.enumList_nodup line 192
29. instance OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.(instance at line 194) line 194
30. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.polynomial line 198
31. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.polynomial_capacity_eval line 202
32. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.polynomial_edges_eval line 206
33. inductive OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Control line 212
34. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Control.enumList line 217
35. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Control.enumList_getElem?_ctorIdx_eq line 220
36. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Control.enumList_nodup line 224
37. instance OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.(instance at line 226) line 226
38. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Coefficients line 230
39. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Layout line 234
40. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.inputControl line 236
41. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.outputControl line 239
42. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.controlSlots line 242
43. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.coefficientBlock line 250
44. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.localSlots line 257
45. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control line 278
46. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots line 280
47. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control_eq_iff line 284
48. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_radix line 287
49. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_accA line 289
50. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_accB line 291
51. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_destination line 293
52. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_counter line 295
53. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_scratch line 297
54. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_digit line 299
55. inductive OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Label line 303
56. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalStart line 309
57. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.afterEval line 312
58. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.statement line 318

    Source documentation

    The fixed arithmetic program never captures input counts in its code.

    def statement (slots : Layout k s d noiseCount ↪ K) (labels : Label k s d noiseCount → Λ)
        (exit : Option Λ) :
        Label k s d noiseCount → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ)
      | .copyNOut => MachineTransfer.loopAt (control slots .variableCount) (control slots .scratch)
          id false (labels .copyNOut) (some (labels .copyNBack))
      | .copyNBack => MachineCopy.forkLoop (control slots .scratch) (control slots .variableCount)
          (control slots .baseValue) false (labels .copyNBack) (some (labels .copyMOut))
      | .copyMOut => MachineTransfer.loopAt (control slots .occurrenceCount) (control slots .scratch)
          id false (labels .copyMOut) (some (labels .copyMBack))
      | .copyMBack => MachineCopy.forkLoop (control slots .scratch) (control slots .occurrenceCount)
          (control slots .temporary) false (labels .copyMBack) (some (labels .addM))
      | .addM => MachineUnaryAddAt.loop (control slots .temporary) (control slots .baseValue)
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control

59. structure OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.WorkClean line 349
60. structure OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Clean line 356
61. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.WorkClean.update_control line 362
62. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalPhaseTrace line 375

    Source documentation

    One placed invocation of the already checked preserving polynomial evaluator.

    theorem evalPhaseTrace (slots : Layout k s d noiseCount ↪ K)
        (labels : Label k s d noiseCount → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
        (kind : Kind) (base : K → List Bool) (value : Nat)
        (hinput : base (control slots (inputControl kind)) = encodeWord value)
        (hdest : base (control slots (outputControl kind)) = [])
        (clean : WorkClean slots base) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[SourceHeaderCounts.Eval.steps (polynomial k s d noiseCount kind) value]
          (some ⟨some (labels (evalStart kind)), ((ambient, ()), register), base⟩) =
          some ⟨some (labels (afterEval kind)), ((ambient, ()), none),
            Function.update base (control slots (outputControl kind))
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Kind, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.inputControl, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.outputControl, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.WorkClean, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.polynomial, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalStart, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.afterEval

63. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.headerBits line 398
64. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.resultTapes line 401
65. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.steps line 408
66. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.trace_trans line 414
67. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.preparedBase line 418
68. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.prepareBaseTrace line 423

    Source documentation

    Copies preserve both operands; addition consumes only the temporary copy.

    theorem prepareBaseTrace (slots : Layout k s d noiseCount ↪ K)
        (labels : Label k s d noiseCount → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
        (base : K → List Bool) (n m : Nat)
        (hn : base (control slots .variableCount) = encodeWord n)
        (hm : base (control slots .occurrenceCount) = encodeWord m)
        (clean : Clean slots base) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[2 * n + 3 * m + 10]
          (some ⟨some (labels .copyNOut), ((ambient, ()), register), base⟩) =
          some ⟨some (labels (evalStart .capacity)), ((ambient, ()), none),
            preparedBase slots base n m⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Clean, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.evalStart, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.capacity, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.preparedBase

69. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.doubleTrace line 496

    Source documentation

    Physical doubling emits the vertex-count word and restores the capacity.

    theorem doubleTrace (slots : Layout k s d noiseCount ↪ K)
        (labels : Label k s d noiseCount → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ label, program (labels label) = statement slots labels exit label)
        (base : K → List Bool) (value : Nat)
        (hcap : base (control slots .capacity) = encodeWord value)
        (hscratch : base (control slots .scratch) = []) (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[3 * value + 5]
          (some ⟨some (labels .doubleScan), ((ambient, ()), register), base⟩) =
          some ⟨some (labels .alphabet), ((ambient, ()), none),
            Function.update base (control slots .reversed)
              ((encodeWord (2 * value)).reverse ++ base (control slots .reversed))⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.capacity

70. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.trace line 522

    Source documentation

    All arithmetic and header emission, with exact composed transition count.

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

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Layout, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Label, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.statement, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Clean, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.steps, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.resultTapes

71. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.inTime line 604
72. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.timePolynomial line 621

    Source documentation

    A fixed polynomial in the serialized input length bounds actual steps.

    def timePolynomial (k s d noiseCount : Nat) : Polynomial Nat :=
    …

73. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.steps_le_timePolynomial line 628
74. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Layout line 651
75. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.arithmeticSlots line 655
76. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.prefixLocal line 660
77. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.prefixLocal_apply line 668
78. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.prefixSlots line 677
79. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Label line 680
80. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.statement line 682
81. structure OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Clean line 689
82. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.prefixResult_control line 696

    Source documentation

    Prefix writes only the read-copy and the two designated count tapes.

    theorem prefixResult_control (slots : Layout k s d noiseCount ↪ K) (base : K → List Bool)
        (n m : Nat) (c : Arithmetic.Control)
        (hn : c ≠ .variableCount) (hm : c ≠ .occurrenceCount) :
        Prefix.resultTapes (prefixSlots slots) base n m
          (Arithmetic.control (arithmeticSlots slots) c) =
        base (Arithmetic.control (arithmeticSlots slots) c) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Layout, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Control, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Prefix.resultTapes, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.prefixSlots, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.arithmeticSlots

83. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.prefixResult_coefficient line 706
84. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Clean.afterPrefix line 713
85. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes line 727
86. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.inTime line 732
87. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.timePolynomial line 778
88. def OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.inPolynomialTime line 781
89. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_source line 802
90. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_n line 808
91. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_m line 815
92. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_base line 822
93. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_capacity line 827
94. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_reversed line 832
95. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_other line 841

    Source documentation

    No slot other than the read-copy, saved counts, B, cap, and output is changed.

    theorem resultTapes_other (slots : Layout k s d noiseCount ↪ K)
        (base : K → List Bool) (n m : Nat) (tape : K)
        (hread : tape ≠ slots (.inl 1))
        (hn : tape ≠ Arithmetic.control (arithmeticSlots slots) .variableCount)
        (hm : tape ≠ Arithmetic.control (arithmeticSlots slots) .occurrenceCount)
        (hB : tape ≠ Arithmetic.control (arithmeticSlots slots) .baseValue)
        (hcap : tape ≠ Arithmetic.control (arithmeticSlots slots) .capacity)
        (hout : tape ≠ Arithmetic.control (arithmeticSlots slots) .reversed) :
        resultTapes slots base n m tape = base tape := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Layout, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.control, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.arithmeticSlots, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.capacity, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes

96. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.resultTapes_readCopy line 854