PoweringPolynomialBudget.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget line 11
Source documentation
Initial setup, the actual vertex loop, and the bridge to cleanup.
```
def preBudget (d n vertices inputLength : Nat) : Nat :=
…
```
def OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget line 17
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.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget line 22
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget_mono_vertices line 27
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget_mono line 34
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_mono_vertices line 49
def OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime line 59
Source documentation
The exact affine polynomial of one concrete row body.
```
noncomputable def rowTime (d n : Nat) : Polynomial Nat :=
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime_eval line 66
def OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime line 73
Source documentation
The actual fixed number of row commands multiplies the row polynomial.
```
noncomputable def vertexTime (d n : Nat) : Polynomial Nat :=
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime_eval line 76
def OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.preTime line 82
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.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.preTime_eval line 86
def OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.time line 93
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.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.time_eval line 101
theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_le_time line 108
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.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget, OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.time

theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.setup_loop_finish_le_time line 116

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.MaxCutGames.Foundations.Complexity.PoweringMachineVertex.budget, OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.time

theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.execution_budget_le_time line 130

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.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget, OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget, OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.time

theorem OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.graph_totalBudget_le_time line 144
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.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget, OAI.MaxCutGames.Foundations.Complexity.PoweringPolynomialBudget.time