MachineProductRuntime.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The complete explicit product computation. Every execution phase is supplied by the actual controller; the cleanup bound follows from the space reached by its actual prefix. The exponent and alphabet enter only the fixed program.

def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.loopPolynomial line 21
theorem OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.loop_budget line 25
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.prefixPolynomial line 34
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.prefixInTime line 38
Source documentation
Actual header initialization followed by every product row and odometer step.
```
def prefixInTime {q : Nat} (H : Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some (MachineProductFinish.afterRows H t))
      ((prefixPolynomial q t).eval (gameBits H).length) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.afterRows, OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.prefixPolynomial
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.timePolynomial line 60
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.outputInTime line 66
Source documentation
The complete run produces the literal full-table target code, clears all private stacks, resets its finite state, and halts.
```
def outputInTime {q : Nat} (H : Instance q)
    (presentation : MachineOutputContract.SimpleBipartite H) (t : Nat) (ht : 0 < t) :
    TM2OutputsInTime (machine q t) (gameBits H)
      (some (gameBits (ProductPaddedOutput.output H presentation t ht)))
      ((timePolynomial q t).eval (gameBits H).length) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite, OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output, OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.timePolynomial
abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.Input line 97
Source documentation
The bipartition is proof-side data. Its codec is exactly the underlying instance code and the fixed program does not inspect it.
```
abbrev Input (q : Nat) := Σ H : Instance q, MachineOutputContract.SimpleBipartite H
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.construct line 99
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.computation line 102
theorem OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.finiteAlphabet line 121
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.certify line 127
def OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.compose line 138
Source documentation
Direct composition with an actual preceding simple-bipartite producer.
```
def compose (upstream : TM2ComputableInPolyTime encode gameBits f)
    (presentation : ∀ a, MachineOutputContract.SimpleBipartite (f a))
    (t : Nat) (ht : 0 < t) :
    TM2ComputableInPolyTime encode gameBits
      (fun a => ProductPaddedOutput.output (f a) (presentation a) t ht) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite, OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output
theorem OAI.UniqueGamesTheorem.Explicit.MachineProductRuntime.compose_finiteAlphabet line 145