OAI/Computability/UniqueGames/Reduction/SourceEquationLookupLemmas.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape line 18
2. inductive OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Label line 22
3. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.fieldDestination line 28
4. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readStart line 29
5. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readLoop line 30
6. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.skipLabel line 31
7. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.headerLabel line 32
8. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.program line 39

   Source documentation

   Eight binary stacks and fixed finite control. Every loop scans one actual bit or tests one actual counter bit. The arbitrary ambient state is preserved.

   def program : Label → TM2.Stmt (fun _ : Tape => Bool) Label (σ × Option Bool)
     | .copyOut => Reduction.MachineTransfer.loopAt .source .scratch id false
         .copyOut (some .copyBack)
     | .copyBack => MachineCopy.forkLoop .scratch .source .work false
         .copyBack (some .headerFirst)
     | .headerFirst => MachineLookup.discard .work .headerFirst .headerSecond
     | .headerSecond => MachineLookup.discard .work .headerSecond .guard
     | .guard => MachineUnaryCounter.guard .index (skipLabel 0) (readStart 0)
     | .skip slot => MachineLookup.discard .work (.skip slot) (skipLabel (slot.val + 1))
     | .read slot =>
         if slot.1.val < 4 then
           if slot.2 then
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Label, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.skipLabel, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readStart

9. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.atSkip line 56
10. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.atReadStart line 60
11. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.atReadLoop line 64
12. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.atReadDone line 69
13. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.discardHeadersTrace line 73

    Source documentation

    The two header fields are physically consumed from the work copy.

    theorem discardHeadersTrace (base : Tape → List Bool) (variableCount equations : Nat)
        (suffix : List Bool) (hinput : base .work = encodeWords [variableCount, equations] ++ suffix) (ambient : σ) :
        (advance (TM2.step program))^[variableCount + equations + 2]
          (some ⟨some .headerFirst, (ambient, none), base⟩) =
          some ⟨some .guard, (ambient, none), Function.update base .work suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.program

14. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.discardFourTrace line 87

    Source documentation

    The fixed skip body consumes four complete unary fields and returns to the same counter guard, preserving the counter and every other tape.

    theorem discardFourTrace (base : Tape → List Bool) (values : List Nat)
        (hlen : values.length = 4) (suffix : List Bool)
        (hinput : base .work = encodeWords values ++ suffix) (ambient : σ) :
        (advance (TM2.step program))^[(encodeWords values).length]
          (some ⟨some (skipLabel 0), (ambient, none), base⟩) =
          some ⟨some .guard, (ambient, none), Function.update base .work suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.program, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.skipLabel

15. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readFourTrace line 98

    Source documentation

    Read the selected four fields using the already checked scanner.

    theorem readFourTrace (base : Tape → List Bool) (values : List Nat)
        (hlen : values.length = 4) (suffix : List Bool)
        (hinput : base .work = encodeWords values ++ suffix) (ambient : σ) :
        (advance (TM2.step program))^[(encodeWords values).length + 5]
          (some ⟨some (readStart 0), (ambient, none), base⟩) =
          some ⟨none, (ambient, none),
            SourceFieldArray.sequenceTapes .work fieldDestination base 0 values suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.program, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readStart, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.fieldDestination

16. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.scanTapes line 115

    Source documentation

    Normal form for the changing counter and consumed work-copy prefix.

    def scanTapes (base : Tape → List Bool) (index : Nat)
        (indexSuffix input : List Bool) : Tape → List Bool :=
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape

17. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.scanTapes_work line 119
18. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.scanTapes_index line 123
19. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.scanTapes_other line 128
20. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.update_scanTapes_work line 133
21. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.skipEquationsTrace line 142

    Source documentation

    Each equation-index bit causes one genuine guard transition and exactly four field-discard loops. The final zero guard enters the field reader.

    theorem skipEquationsTrace {n : Nat} (base : Tape → List Bool)
        (prior : List (CloneGap.Equation (Fin n))) (indexSuffix suffix : List Bool)
        (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[(encodeWords (prior.flatMap equationWords)).length + prior.length + 1]
          (some ⟨some .guard, (ambient, register), scanTapes base prior.length indexSuffix
            (encodeWords (prior.flatMap equationWords) ++ suffix)⟩) =
          some ⟨some (readStart 0), (ambient, none), scanTapes base 0 indexSuffix suffix⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.program, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.scanTapes, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readStart

22. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.fieldDestination_eq line 190
23. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.fieldDestination_injective_below line 196
24. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readFour_output_field line 202
25. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readFour_output_work line 214
26. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.readFour_output_frame line 222
27. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.outputTapes line 230
28. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.scanSteps line 236
29. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.scanReadTrace line 242
30. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.lookupSteps line 270
31. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.lookupWithSplitTrace line 274
32. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_source line 304
33. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_index line 310
34. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_work line 316
35. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_field line 322
36. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_first line 329
37. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_second line 335
38. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_third line 341
39. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_rhs line 347
40. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_frame line 353
41. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.equationWords_four line 360
42. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.fieldWords line 365
43. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.output_fieldWords line 368
44. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.lookupSteps_le_input line 374
45. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.timePolynomial line 393
46. theorem OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.timePolynomial_eval line 395
47. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.lookupWithSplitInTime line 399

    Source documentation

    A polynomial bound on the actual complete copy/skip/read execution.

    def lookupWithSplitInTime (F : SourceEncoding.Input) (prior : List (CloneGap.Equation (Fin F.variables)))
        (equation : CloneGap.Equation (Fin F.variables)) (after : List (CloneGap.Equation (Fin F.variables)))
        (hsplit : F.equations = prior ++ equation :: after)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hsource : base .source = inputBits F)
        (hindex : base .index = encodeWord prior.length ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (ambient : σ) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some .copyOut, (ambient, register), base⟩
          (some ⟨none, (ambient, none),
            outputTapes base equation indexSuffix (encodeWords (after.flatMap equationWords))⟩)
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.program, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.outputTapes

48. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.lookupInTime line 419
49. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.machine line 438
50. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.machineInTime line 450

    Source documentation

    The same proved run stated directly for the concrete finite machine.

    def machineInTime (F : SourceEncoding.Input) (i : Fin F.equations.length)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hsource : base .source = inputBits F)
        (hindex : base .index = encodeWord i.val ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (register : Option Bool) :
        StateTransition.EvalsToInTime machine.step
          ⟨some .copyOut, ((), register), base⟩
          (some ⟨none, ((), none), outputTapes base F.equations[i.val] indexSuffix
            (encodeWords ((F.equations.drop (i.val + 1)).flatMap equationWords))⟩)
          (timePolynomial.eval (inputBits F).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.outputTapes

51. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.placedLookupInTime line 466

    Source documentation

    Same-tape placement into the caller's finite control. Choosing the ambient type to be τ × Unit gives the shared state (τ × Unit) × Option Bool used by the field-template machinery. The lookup's final transition enters exit.

    noncomputable def placedLookupInTime {Λ' : Type}
        (labels : Label → Λ') (exit : Option Λ')
        (target : Λ' → TM2.Stmt (fun _ : Tape => Bool) Λ' (σ × Option Bool))
        (atLabels : ∀ l, target (labels l) =
          MachineSubroutine.statement labels exit (program (σ := σ) l))
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Label, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.program

52. def OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.embeddedLookupInTime line 487

    Source documentation

    An optional disjoint-stack placement preserves arbitrary extra tapes and state. It reuses the same generic lookup and introduces no extra transitions.

    noncomputable def embeddedLookupInTime {E Λextra τ : Type} [DecidableEq E]
        (continuation : Option (Label ⊕ Λextra)) (extraState : τ)
        (extraTapes : E → List Bool)
        (extra : Λextra → TM2.Stmt
          (MachineEmbedding.Alphabet (fun _ : Tape => Bool) (fun _ : E => Bool))
          (Label ⊕ Λextra) ((σ × Option Bool) × τ))
        (input : SourceEncoding.Input) (i : Fin input.equations.length)
        (base : Tape → List Bool) (indexSuffix : List Bool)
        (hsource : base .source = inputBits input)
        (hindex : base .index = encodeWord i.val ++ indexSuffix)
        (hwork : base .work = []) (hscratch : base .scratch = [])
        (ambient : σ) (register : Option Bool) :
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Label, OAI.UniqueGamesTheorem.Reduction.SourceEquationLookup.Tape, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input

53. inductive OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Tape line 522
54. inductive OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Label line 529
55. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.place line 538
56. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.place_injective line 542
57. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.fill line 546
58. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.fill_place line 553
59. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.fill_self line 558
60. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.fill_update line 568
61. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.placedLabel line 577
62. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.placedConfiguration line 581
63. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.placedStatement line 587
64. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.placed_stepAux line 599
65. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.nextLabel line 624
66. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.program line 627
67. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.placed_step line 638
68. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.lookupOutput line 655
69. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.placedLookupInTime line 660
70. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.copiedTapes line 676
71. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.coordinateOutput line 679
72. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.cleanup_lookupOutput line 687
73. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.coordinateOutput_savedIndex line 715
74. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.coordinateOutput_field line 720
75. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.coordinateOutput_other_field line 727
76. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.suffix_length_le_input line 732
77. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.coordinateInTime line 744
78. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.labelAt line 789
79. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.nextLabel_eq line 792
80. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.stageTapes line 794
81. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.stageTapes_frame line 802
82. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.stageTapes_clean line 815
83. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.stageTapes_field line 827
84. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.prefixInTime line 852
85. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.loadInTime line 895
86. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.equations_length_le_input line 918
87. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.loadUnaryInTime line 925

    Source documentation

    Actual odometer digits have empty suffixes. The resulting complete loader runs in a polynomial whose coefficients depend only on the fixed repetition k.

    noncomputable def loadUnaryInTime (F : SourceEncoding.Input) (tuple : Fin width → Fin F.equations.length)
        (base : Tape width Extra → List Bool)
        (hsource : base .source = inputBits F)
        (hsavedIndex : ∀ j, base (.savedIndex j) = encodeWord (tuple j).val)
        (hindex : base .index = []) (hwork : base .work = [])
        (hscratch : base .scratch = []) (hcopy : base .copyScratch = []) (ambient : σ) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labelAt 0), ((ambient, ()), none), base⟩
          (some ⟨none, ((ambient, ()), none), stageTapes F tuple base width⟩)
          (width * (10 * (inputBits F).length + 20) + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Tape, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.program, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.labelAt, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.stageTapes

88. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.timePolynomial line 948
89. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.timePolynomial_eval line 951
90. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.tupleBitLength line 958

    Source documentation

    Total physical length of the saved occurrence-ID tapes.

    def tupleBitLength (base : Tape width Extra → List Bool) : Nat :=
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Tape

91. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.savedIndex_length_le_tupleBitLength line 962
92. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.loadTupleInTime line 967
93. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.loadTuplePolynomialInTime line 982

    Source documentation

    The same concrete run with a univariate polynomial in the combined size.

    noncomputable def loadTuplePolynomialInTime (F : SourceEncoding.Input)
        (tuple : Fin width → Fin F.equations.length) (base : Tape width Extra → List Bool)
        (hsource : base .source = inputBits F)
        (hsaved : ∀ j, base (.savedIndex j) = encodeWord (tuple j).val)
        (hindex : base .index = []) (hwork : base .work = [])
        (hscratch : base .scratch = []) (hcopy : base .copyScratch = []) (ambient : σ) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (labelAt 0), ((ambient, ()), none), base⟩
          (some ⟨none, ((ambient, ()), none), stageTapes F tuple base width⟩)
          ((timePolynomial width).eval ((inputBits F).length + tupleBitLength base)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Tape, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.program, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.labelAt, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.stageTapes, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.timePolynomial, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.tupleBitLength

94. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.nameSlot line 1000
95. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.nameField line 1001
96. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.rhsField line 1002
97. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.nameField_ne_rhsField line 1005
98. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.equationName line 1014
99. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.equationWords_name line 1020
100. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.output_name line 1027
101. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.output_rhs line 1034
102. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.output_savedIndex line 1042
103. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.output_savedIndex_unary line 1048
104. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.output_source line 1055
105. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.canonicalFields line 1062

     Source documentation

     The fourth canonical record field is the saved occurrence ID. The equation RHS remains separately available on rhsField j.

     def canonicalFields (tapes : Tape width Extra → List Bool) (j : Fin width) : List (List Bool) :=
     …

     Mentions: OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Tape

106. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.canonicalWords line 1065
107. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.output_canonicalFields line 1069
108. theorem OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.zeroWidthStep line 1079

     Source documentation

     Width zero executes its actual done statement in one transition.

     theorem zeroWidthStep (base : Tape 0 Extra → List Bool) (ambient : σ) :
         TM2.step program ⟨some (labelAt 0), ((ambient, ()), none), base⟩ =
           some ⟨none, ((ambient, ()), none), base⟩ := rfl

     Mentions: OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Tape, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.program, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.labelAt

109. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.placedLoadUnaryInTime line 1085

     Source documentation

     A caller shares this complete tape arena and state, mapping only labels and the final continuation. All saved occurrence IDs remain available to its body.

     noncomputable def placedLoadUnaryInTime {Λ : Type}
         (labels : Label width → Λ) (exit : Option Λ)
         (target : Λ → TM2.Stmt (fun _ : Tape width Extra => Bool) Λ ((σ × Unit) × Option Bool))
         (atLabels : ∀ l, target (labels l) = MachineSubroutine.statement labels exit (program l))
         (F : SourceEncoding.Input) (tuple : Fin width → Fin F.equations.length)
         (base : Tape width Extra → List Bool)
         (hsource : base .source = inputBits F)
         (hsaved : ∀ j, base (.savedIndex j) = encodeWord (tuple j).val)
         (hindex : base .index = []) (hwork : base .work = [])
         (hscratch : base .scratch = []) (hcopy : base .copyScratch = []) (ambient : σ) :
         StateTransition.EvalsToInTime (TM2.step target)
           ⟨some (labels (labelAt 0)), ((ambient, ()), none), base⟩
     …

     Mentions: OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Label, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.Tape, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.program, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.labelAt

110. def OAI.UniqueGamesTheorem.Reduction.MachineSourceTuple.machine line 1102