PoweringPolynomialBudgetLemmas.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Finishing cost from the actual preceding machine execution

Every stack can grow by at most the fixed program's push bound in one transition. Consequently an actual bounded execution from the standard input configuration supplies the uniform stack bound needed by the finishing phase. The bound below uses the same global machine for that preceding execution; no separate tape-size hypothesis or numerical simulation is substituted for it.

def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.preBudget line 14
Source documentation
Initial setup, the actual vertex loop, and the bridge to cleanup.
```
def preBudget (d n vertices inputLength : Nat) : Nat :=
…
```
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.finishBudget line 20
Source documentation
Cleanup after a preceding run bounded by prior, with fixed stack count and fixed maximum number of pushes per machine transition.
```
def finishBudget (d n pushBound tapeCount vertices inputLength prior : Nat) : Nat :=
…
```
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.totalBudget line 25
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.preBudget_mono_vertices line 30
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.finishBudget_mono line 37
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_mono_vertices line 52
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.rowTime line 62
Source documentation
The exact affine polynomial of one concrete row body.
```
noncomputable def rowTime (d n : Nat) : Polynomial Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.rowTime_eval line 69
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.vertexTime line 76
Source documentation
The actual fixed number of row commands multiplies the row polynomial.
```
noncomputable def vertexTime (d n : Nat) : Polynomial Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.vertexTime_eval line 79
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.preTime line 85
Source documentation
Replace the vertex count by the input length in the actual setup/loop bound.
```
noncomputable def preTime (d n : Nat) : Polynomial Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.preTime_eval line 89
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.time line 96
Source documentation
The explicit final polynomial. All coefficients depend only on the fixed degree/radius and the chosen finite machine's push bound and tape count.
```
noncomputable def time (d n pushBound tapeCount : Nat) : Polynomial Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.time_eval line 104
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_le_time line 111
Source documentation
The actual vertex count may be strictly smaller than the input length.
```
theorem totalBudget_le_time (d n pushBound tapeCount vertices inputLength : Nat)
    (hvertices : vertices ≤ inputLength) :
    totalBudget d n pushBound tapeCount vertices inputLength ≤
      (time d n pushBound tapeCount).eval inputLength := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.totalBudget, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.time

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.setup_loop_finish_le_time line 119

Source documentation

Direct arithmetic interface for the global setup/loop and cleanup bounds.

theorem setup_loop_finish_le_time (d n pushBound tapeCount vertices inputLength : Nat)
    (hvertices : vertices ≤ inputLength) :
    ((3 * vertices + 5) +
        (vertices * (PoweringMachineVertex.budget d n inputLength + 2) + 1)) +
      (2 * (vertices + (2 * d ^ (n + 1)) * vertices) + 6 +
        tapeCount * (inputLength +
          ((3 * vertices + 5) +
            (vertices * (PoweringMachineVertex.budget d n inputLength + 2) + 1)) * pushBound +
          vertices + (2 * d ^ (n + 1)) * vertices + 3)) ≤
      (time d n pushBound tapeCount).eval inputLength := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.budget, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.time

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.execution_budget_le_time line 133
Source documentation
Numerical bounds on two actual phases can use the same fixed polynomial.
```
theorem execution_budget_le_time (d n pushBound tapeCount vertices inputLength : Nat)
    (hvertices : vertices ≤ inputLength) {preSteps finishSteps : Nat}
    (hpre : preSteps ≤ preBudget d n vertices inputLength)
    (hfinish : finishSteps ≤ finishBudget d n pushBound tapeCount vertices inputLength
      (preBudget d n vertices inputLength)) :
    preSteps + finishSteps ≤ (time d n pushBound tapeCount).eval inputLength := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.preBudget, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.finishBudget, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.time
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.graph_totalBudget_le_time line 147
Source documentation
Typed graph input supplies the required vertex-count bound itself.
```
theorem graph_totalBudget_le_time {vertices d : Nat} (graph : PortTables.Table vertices d)
    (n pushBound tapeCount : Nat) :
    totalBudget d n pushBound tapeCount vertices (PortTables.tableBits graph).length ≤
      (time d n pushBound tapeCount).eval (PortTables.tableBits graph).length :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.totalBudget, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPolynomialBudget.time

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_of_execution line 171

Source documentation

Uniform stack growth along an actual execution, from any initial configuration.

theorem stackLength_le_of_execution (tm : FinTM2) (start finish : tm.Cfg)
    (initialBound priorBudget : Nat)
    (initial : ∀ k, (start.stk k).length ≤ initialBound)
    (prior : StateTransition.EvalsToInTime tm.step start (some finish) priorBudget)
    (k : tm.K) :
    (finish.stk k).length ≤ initialBound + priorBudget * Runtime.programPushBound tm := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_from_input line 182

Source documentation

Standard input initialization bounds every initial stack by the input length.

theorem stackLength_le_from_input (tm : FinTM2) (input : List (tm.Γ tm.k₀))
    (finish : tm.Cfg) (priorBudget : Nat)
    (prior : StateTransition.EvalsToInTime tm.step (initList tm input)
      (some finish) priorBudget) (k : tm.K) :
    (finish.stk k).length ≤ input.length + priorBudget * Runtime.programPushBound tm :=
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound

abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringRuntimeBudget.tapeCount line 191
Source documentation
Cleanup's concrete tape count is the size of the global tape enumeration.
```
abbrev tapeCount (radius : Nat) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringRuntimeBudget.finish_steps_le_of_execution line 197
Source documentation
The actual global prefix execution supplies every finishing stack bound. The physical header premises are used by PoweringMachineFinish.traceAt; this arithmetic consequence of that prefix is valid for any two proposed header values.
```
theorem finish_steps_le_of_execution (d radius : Nat) (input : List Bool)
    (before : (PoweringMachineGlobal.machine d radius).Cfg)
    (priorBudget vertices darts : Nat)
    (prior : StateTransition.EvalsToInTime (PoweringMachineGlobal.machine d radius).step
      (initList (PoweringMachineGlobal.machine d radius) input) (some before) priorBudget) :
    PoweringMachineFinish.steps (PoweringMachineGlobal.enumeration radius)
      (PoweringMachineGlobal.outputTape radius) before.stk vertices darts ≤
      2 * (vertices + darts) + 6 + tapeCount radius *
        (input.length + priorBudget * Runtime.programPushBound
          (PoweringMachineGlobal.machine d radius) + vertices + darts + 3) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.enumeration, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.outputTape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringRuntimeBudget.tapeCount, OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringRuntimeBudget.total_steps_le_of_execution line 213

Source documentation

Total transitions of the actual prefix plus the exact finishing cost.

theorem total_steps_le_of_execution (d radius : Nat) (input : List Bool)
    (before : (PoweringMachineGlobal.machine d radius).Cfg)
    (priorBudget vertices darts : Nat)
    (prior : StateTransition.EvalsToInTime (PoweringMachineGlobal.machine d radius).step
      (initList (PoweringMachineGlobal.machine d radius) input) (some before) priorBudget) :
    prior.steps + PoweringMachineFinish.steps (PoweringMachineGlobal.enumeration radius)
      (PoweringMachineGlobal.outputTape radius) before.stk vertices darts ≤
      priorBudget + (2 * (vertices + darts) + 6 + tapeCount radius *
        (input.length + priorBudget * Runtime.programPushBound
          (PoweringMachineGlobal.machine d radius) + vertices + darts + 3)) :=
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineFinish.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.enumeration, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineGlobal.outputTape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringRuntimeBudget.tapeCount, OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound

def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinish line 239
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration line 243
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget line 248
Source documentation
Initialization and the actual outer loop's proved budgets.
```
def beforeFinishBudget (graph : PortTables.Table vertices d) (n : Nat) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_ready line 252
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_output line 260
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_vertices line 271
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_darts line 279
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.serialized_eq line 290
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.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinish
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinishExecution line 299
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishSteps line 321
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishExecution line 327
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishSteps
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.execution line 354
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishSteps
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.finishSteps_le line 366
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.execution_budget_le line 377
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime line 388
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime_finite_alphabet line 417
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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime