MachinePaddedOverlayRuntimeLemmas.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the actual regularization subcalls. These lemmas bound the established step counts; they do not assume any machine execution.

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram line 16
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.sourceMachine_eq line 24
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanupTapes line 30
Source documentation
A fixed finite list of every non-output stack. This includes both retained archives, the original input, and the physically consumed level.
```
noncomputable def cleanupTapes : List Tape :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanup_complete line 33
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.initial_configuration line 37
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.terminalRun line 48
Source documentation
The raw terminal witness is the actual three-phase execution. No phase trace, output-size bound, or complexity assertion is an input hypothesis.
```
noncomputable def terminalRun (H : BaseTable) (d : Nat) (hd : 0 < d)
    (a : PortTables.Input d) :
    MachineCanonicalOutput.TerminalRun (rawProgram H d hd) (PortTables.inputBits a)
      (PortTables.inputBits (PreprocessingStageMaps.paddedOverlay H d a))
      ((MachinePaddedOverlay.timePolynomial d).eval (PortTables.inputBits a).length) where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCanonicalOutput.TerminalRun, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.timePolynomial
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime line 62
Source documentation
A concrete machine reaches the canonical haltList encoding of the existing executable preprocessing map in polynomial time.
```
noncomputable def computableInPolyTime (H : BaseTable) (d : Nat) (hd : 0 < d) :
    TM2ComputableInPolyTime (PortTables.inputBits (ports := d))
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.finite_alphabet line 72
Source documentation
Finiteness belongs to the exact machine stored in the certificate above.
```
theorem finite_alphabet (H : BaseTable) (d : Nat) (hd : 0 < d) :
    ∀ k, Finite ((computableInPolyTime H d hd).tm.Γ k) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_mono line 88
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial line 95
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial_eval line 103
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.internal_steps_le line 112
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.familyPolynomial line 131

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.family_budget_le line 136

Source documentation

The completed reusable family call includes the three actual drains.

theorem family_budget_le (t : GraphTables.Table) (v : Fin t.vertices) :
    MachinePaddedExpanderFamilyBounds.timePolynomial.eval (cloudSize t v + 1) +
      2 * ExpanderFamily.growth * (cloudSize t v + 1) + 7 ≤
        familyPolynomial.eval (inputLength t) := by
…

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial line 149
Source documentation
A generous serialized-row bound evaluated at the actual linear vertex cap.
```
noncomputable def rowPolynomial (q : Nat) : Polynomial Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial_eval line 153
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.actual_row_bound_le line 159
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial line 167
Source documentation
The inner port loop can grow the old prefix by at most q complete rows.
```
noncomputable def blockCorePolynomial (q : Nat) : Polynomial Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_add_output line 170

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.block_core_bound_le line 178

Source documentation

Uniform cap for the actual affine bound used by the port-loop wrapper, including all rows it may already have appended during this vertex.

theorem block_core_bound_le (q : Nat) (t : GraphTables.Table)
    (tables : ∀ v, ExpanderTables.Table (cloudSize t v + padding t v) q)
    (v : Fin t.vertices) (x : PaddedCloud t (padding t) v)
    (initialOutput : Nat) (houtput : initialOutput ≤ regularPolynomial.eval (inputLength t)) :
    coreTimeBound q (GraphTables.tableBits t).length
      (encodeWords (ExpanderTableWords.rotationWords (tables v))).length
      (vertexOrder t (padding t) x.val).val v.val (paddedCloudRank t (padding t) v x).val
      (cloudSize t v) (PreprocessingPaddingOffsets.offset (padding t) v.val) t.darts
      (initialOutput + q *
        (vertexCount t (padding t) + vertexCount t (padding t) * (q + 1) + 8192)) ≤
      (blockCorePolynomial q).eval (inputLength t) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial