MachineLazyTableRuntime.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Canonical polynomial-time computation of the executable lazy preprocessing map. The raw machine's retained original input is physically drained by the checked canonical-output wrapper before it reaches the standard haltList endpoint.

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.rawProgram line 18
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.sourceMachine_eq line 26
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.cleanupTapes line 31
Source documentation
A fixed explicit list of every non-output tape, independent of input data.
```
def cleanupTapes : List Tape :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.cleanup_complete line 35
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.terminalRun line 41
Source documentation
The terminal witness is the checked full lazy-table execution. The wrapper then drains the retained original input rather than assuming it disappeared.
```
def terminalRun (d : Nat) (positive : 0 < d) (a : PortTables.Input d) :
    MachineCanonicalOutput.TerminalRun (rawProgram d positive) (PortTables.inputBits a)
      (PortTables.inputBits (PreprocessingStageMaps.lazy d a))
      ((MachineLazyTable.timePolynomial d).eval (PortTables.inputBits a).length) where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.TerminalRun, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.rawProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.timePolynomial
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.computableInPolyTime line 53
Source documentation
The actual canonical-output finite machine computes precisely the shared degree-d to degree-2d stage map in polynomial time.
```
noncomputable def computableInPolyTime (d : Nat) (positive : 0 < d) :
    TM2ComputableInPolyTime (PortTables.inputBits (ports := d))
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.finite_alphabet line 61
Source documentation
Every tape alphabet of this exact completed computation certificate is finite.
```
theorem finite_alphabet (d : Nat) (positive : 0 < d) :
    ∀ k, Finite ((computableInPolyTime d positive).tm.Γ k) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTableRuntime.computableInPolyTime