VectorOptimizerWork.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Materialized rational optimizer iterates. Finite vectors store the previous iterate and its gradient, and a scored scan stores the current best score. Counters charge rational arithmetic, comparisons, array accesses and array writes. Integer/rational bit costs are separate.

def OAI.EditApproximation.naturalPowerWithWork line 17
theorem OAI.EditApproximation.naturalPowerWithWork_spec line 22
theorem OAI.EditApproximation.vector_get_ofFn line 27
theorem OAI.EditApproximation.vectorMapWithWork_value line 34
Source documentation
A single materializing array pass. The operation count includes array construction, the value/counter traversals, and summing counters.
```
theorem vectorMapWithWork_value {α : Type*} (d : ℕ) (f : Fin d → α × ℕ) (i : Fin d) :
    (vectorMapWithWork d f).1.get i = (f i).1 := by
…
```
Mentions: OAI.EditApproximation.vectorMapWithWork
theorem OAI.EditApproximation.vectorMapWithWork_cost line 39

def OAI.EditApproximation.vectorDotListWithWork line 47

Source documentation

Dot product over an explicit list of array indices.

def vectorDotListWithWork {d : ℕ} (left right : Vector ℚ d) : List (Fin d) → ℚ × ℕ
  | [] => (0, 0)
  | i :: indices =>
    let rest := vectorDotListWithWork left right indices
…

theorem OAI.EditApproximation.vectorDotListWithWork_spec line 53
def OAI.EditApproximation.vectorDotWithWork line 62
theorem OAI.EditApproximation.vectorDotWithWork_spec line 65
def OAI.EditApproximation.rationalGradientCellWithWork line 70
theorem OAI.EditApproximation.rationalGradientCellWithWork_spec line 76
def OAI.EditApproximation.vectorGradientWithWork line 85
theorem OAI.EditApproximation.vectorGradientWithWork_value line 88
theorem OAI.EditApproximation.vectorGradientWithWork_cost line 93

def OAI.EditApproximation.scoredArgmaxWithWork line 101

Source documentation

A scored scan keeps the winning score instead of recomputing it. It retains the first maximizer, including ties.

def scoredArgmaxWithWork {α : Type*} (score : α → ℚ × ℕ) : List α → Option (α × ℚ) × ℕ
  | [] => (none, 0)
  | a :: rest =>
    let tail := scoredArgmaxWithWork score rest
…

theorem OAI.EditApproximation.scoredArgmaxWithWork_value line 111
theorem OAI.EditApproximation.scoredArgmaxWithWork_cost line 122
def OAI.EditApproximation.vectorMaximizerWithWork line 133
theorem OAI.EditApproximation.vectorMaximizerWithWork_value line 138
theorem OAI.EditApproximation.vectorMaximizerWithWork_cost line 152
def OAI.EditApproximation.materializedOptimizerWithWork line 159
theorem OAI.EditApproximation.materializedOptimizerWithWork_value line 171
def OAI.EditApproximation.materializedOptimizerStepBudget line 189
theorem OAI.EditApproximation.materializedOptimizerWithWork_cost line 192
theorem OAI.EditApproximation.optimizerStepArithmetic_bound line 206
theorem OAI.EditApproximation.move_outer_factor line 233
theorem OAI.EditApproximation.move_outer_factor_right line 236
theorem OAI.EditApproximation.materializedOptimizerStepBudget_polynomial line 239
theorem OAI.EditApproximation.materializedOptimizerWithWork_polynomial line 257
def OAI.EditApproximation.materializedSelectionWithWork line 291
Source documentation
The final scan retains the original action label, so equal vectors and tied scores do not change which listed action is returned.
```
def materializedSelectionWithWork {α : Type*} {d : ℕ}
    (vertices : List (α × Vector ℚ d)) (linear : Vector ℚ d) (G j : ℕ) : Option α × ℕ :=
…
```
theorem OAI.EditApproximation.materializedSelectionWithWork_value line 298
theorem OAI.EditApproximation.materializedSelectionWithWork_cost line 313
theorem OAI.EditApproximation.materializedSelectionWithWork_polynomial line 328