PoweringRuntimeBudget.lean`

5 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.

theorem OAI.MaxCutGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_of_execution line 21

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.MaxCutGames.Foundations.Complexity.Runtime.programPushBound

theorem OAI.MaxCutGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_from_input line 32

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.MaxCutGames.Foundations.Complexity.Runtime.programPushBound

abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringRuntimeBudget.tapeCount line 41
Source documentation
Cleanup's concrete tape count is the size of the global tape enumeration.
```
abbrev tapeCount (radius : Nat) : Nat :=
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringRuntimeBudget.finish_steps_le_of_execution line 47
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.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.steps, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.enumeration, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.outputTape, OAI.MaxCutGames.Foundations.Complexity.PoweringRuntimeBudget.tapeCount, OAI.MaxCutGames.Foundations.Complexity.Runtime.programPushBound

theorem OAI.MaxCutGames.Foundations.Complexity.PoweringRuntimeBudget.total_steps_le_of_execution line 63

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.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.machine, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineFinish.steps, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.enumeration, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineGlobal.outputTape, OAI.MaxCutGames.Foundations.Complexity.PoweringRuntimeBudget.tapeCount, OAI.MaxCutGames.Foundations.Complexity.Runtime.programPushBound