PoweringMachineRuntime.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Complete execution of the one fixed powering machine on the actual port-table input and generic graph-table output encodings. The varying vertex count remains on unary tapes throughout.

def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish line 19
Source documentation
The actual work tapes after all vertex blocks, before final headers.
```
def beforeFinish (graph : PortTables.Table vertices d) (n : Nat) : Tape n → List Bool :=
…
```
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration line 23
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget line 28
Source documentation
Initialization and the actual outer loop's proved budgets.
```
def beforeFinishBudget (graph : PortTables.Table vertices d) (n : Nat) : Nat :=
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_ready line 32
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_output line 40
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_vertices line 51
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_darts line 59
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.serialized_eq line 70
Source documentation
The serialized result is exactly the actual powering table, including its header and every relation bit, in the existing output codec.
```
theorem serialized_eq (graph : PortTables.Table vertices d) (n : Nat) :
    encodeWords [vertices, PoweringTableLayout.blockSize d n * vertices] ++
      beforeFinish graph n (outputTape n) = PoweringTables.outputBits graph n := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishExecution line 79
Source documentation
Actual execution from the literal single-input configuration through every vertex. No graph-dependent instruction or supplied body-execution premise.
```
def beforeFinishExecution (graph : PortTables.Table vertices d) (n : Nat) :
    StateTransition.EvalsToInTime (machine d n).step
      (initList (machine d n) (PortTables.tableBits graph))
      (some (finishConfiguration graph n)) (beforeFinishBudget graph n) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps line 101
Source documentation
The actual final-copy/cleanup cost on the tapes obtained from the loop.
```
def finishSteps (graph : PortTables.Table vertices d) (n : Nat) : Nat :=
…
```
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishExecution line 107
Source documentation
The terminal configuration has precisely the actual output stream and no remaining work tapes.
```
def finishExecution (graph : PortTables.Table vertices d) (n : Nat) :
    StateTransition.EvalsToInTime (machine d n).step (finishConfiguration graph n)
      (some (haltList (machine d n) (PoweringTables.outputBits graph n)))
      (finishSteps graph n) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.execution line 134
Source documentation
Whole-machine execution on the concrete input and output encodings.
```
def execution (graph : PortTables.Table vertices d) (n : Nat) :
    TM2OutputsInTime (machine d n) (PortTables.tableBits graph)
      (some (PoweringTables.outputBits graph n))
      (beforeFinishBudget graph n + finishSteps graph n) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps_le line 146
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.execution_budget_le line 157
def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime line 168
Source documentation
A genuine polynomial-time certificate for the actual finite powering constructor, with the existing concrete codecs on both sides.
```
noncomputable def computableInPolyTime (d n : Nat) :
    TM2ComputableInPolyTime (@PortTables.inputBits d) GenericGraphTables.tableBits
      (PoweringTables.transform d n) where
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime_finite_alphabet line 193
Source documentation
Every work tape, as well as the input/output tapes, has a finite alphabet.
```
theorem computableInPolyTime_finite_alphabet (d n : Nat) :
    ∀ k, Finite ((computableInPolyTime d n).tm.Γ k) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime