ComputedCoarseReadBudget.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.computedCoarseReadBudget line 11
Source documentation
Every descriptor, stored-symbol comparison and frame operation used by a computed coarse root has a uniform fixed-power bit budget.
```
theorem computedCoarseReadBudget :
    ∀ᶠ N : ℕ in atTop, ∀ B d : ℕ, ∀ x y : List ℕ,
      B = (integerParameters N).B → d = computedCoarseDepth N (coarseEntryWidth x y) →
      coarseEntryWidth x y ≤ N → (∀ a ∈ x ++ y, Nat.size a ≤ inputHeight N ^ 3) →
      ∀ i : CoarseGuessIndex (coarseEntryWidth x y),
      CoarseReadBudget B d (coarseGuess (coarseEntryWidth x y) i) (coarseEntryWidth x y)
        x y (inputHeight N ^ 30) := by
…
```
Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.CoarseReadBudget, OAI.EditApproximation.coarseGuess