FiniteEnumerationWork.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Literal finite enumeration with counters. Each callback is evaluated once and its returned work is charged; list cells and copied output cells are charged separately.

theorem OAI.EditApproximation.arithmeticMapWithWork_value line 17
theorem OAI.EditApproximation.arithmeticMapWithWork_cost line 23
theorem OAI.EditApproximation.arithmeticFlatMapWithWork_value line 36
theorem OAI.EditApproximation.arithmeticFlatMapWithWork_cost line 42
theorem OAI.EditApproximation.materializedAssignmentsWithWork_value line 59
Source documentation
Each complete assignment is stored in an array, so later coordinate access is constant time. The recursive tail is constructed once.
```
theorem materializedAssignmentsWithWork_value {α : Type*} (M : ℕ) (choices : Fin M → List α) :
    ((materializedAssignmentsWithWork M choices).1.map Vector.get) = finiteAssignments M choices := by
…
```
Mentions: OAI.EditApproximation.materializedAssignmentsWithWork, OAI.EditApproximation.finiteAssignments
theorem OAI.EditApproximation.materializedAssignmentsWithWork_cost line 74
def OAI.EditApproximation.materializedWideActionsWithWork line 140
theorem OAI.EditApproximation.materializedWideActionsWithWork_value line 144
theorem OAI.EditApproximation.materializedWideActionsWithWork_cost line 152
Source documentation
Cartesian-product construction after the endpoint lists are present. Each returned action supports direct indexed reads from its stored array.
```
theorem materializedWideActionsWithWork_cost {nx ny : ℕ} (M : ℕ) (parent : TargetInterval nx)
    (r : TargetInterval ny) (b P : ℕ) (hP : 0 < P) :
    (materializedWideActionsWithWork M parent r b P).2 ≤
      (M + 1) * (6 * M + 10) * ((40 * P + 2) ^ 2 + 1) ^ (M + 1) :=
…
```
Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.materializedWideActionsWithWork