MachineSingleOrbitFinishLemmas.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Actual tape cleanup, accumulator reversal, and halt for the one-orbit postprocessor. The time bound is derived from an actual executed prefix.

theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitFinish.haltList_eq line 16
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitFinish.finishStartInTime line 23
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitFinish.timePolynomial line 31

def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitFinish.completePrefix line 36

Source documentation

This helper consumes a proved prefix trace. The final runtime theorem supplies that trace from the concrete header and complete row traversal.

def completePrefix (q : Nat) (input : List Bool) (prefixTime : Polynomial Nat)
    (base : Tape → List Bool)
    (execution : StateTransition.EvalsToInTime (machine q).step
      (initList (machine q) input)
      (some ⟨some .finishStart, initialState, base⟩) (prefixTime.eval input.length))
    (outputEmpty : base .output = []) :
    TM2OutputsInTime (machine q) input (some (base .accumulator).reverse)
      ((timePolynomial q prefixTime).eval input.length) := by
…

Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitFinish.timePolynomial

def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.finalTapes line 80
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.prefixCost line 83
theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.prefixTrace line 87
Source documentation
The complete prefix is obtained from the actual header and row traces.
```
theorem prefixTrace {q : Nat} (I : Instance q) :
    (advance (TM2.step (program q)))^[prefixCost I]
      (some (initList (machine q) (gameBits (doubleInstance I)))) =
      some ⟨some .finishStart, initialState, finalTapes I⟩ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.prefixCost, OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.finalTapes
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.prefixPolynomial line 115
theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.prefixCost_le line 118
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.prefixInTime line 127
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.timePolynomial line 136
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.fullRunInTime line 140
Source documentation
Literal init-to-halt execution, with every non-output tape empty at halt.
```
def fullRunInTime {q : Nat} (I : Instance q) :
    TM2OutputsInTime (machine q) (gameBits (doubleInstance I))
      (some (gameBits I)) ((timePolynomial q).eval (gameBits (doubleInstance I)).length) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.timePolynomial
def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.computableInPolyTime line 149
Source documentation
A proved polynomial-time codec conversion, without an assumed time bound, an output-size certificate, or an unbounded integer in finite machine state.
```
def computableInPolyTime (q : Nat) :
    TM2ComputableInPolyTime (fun I : Instance q => gameBits (doubleInstance I)) gameBits id where
…
```
theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitRuntime.workAlphabetFinite line 162