ComputedRefinementWords.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.scheduledRefinementWordWithWork_value line 17
Source documentation
The scheduled integer refinement factor is materialized by its dyadic exponent; the terminal pass materializes one.
```
theorem scheduledRefinementWordWithWork_value (N pass : ℕ)
    (hf : 3 ≤ smallLogExponent N) (hpass : pass ≤ computedSeedPassCount N) :
    (scheduledRefinementWordWithWork N pass).1.value =
      refinementFactor (scheduledSeedFactor N pass) (inputSmallLog N) := by
…
```
Mentions: OAI.EditApproximation.smallLogExponent, OAI.EditApproximation.computedSeedPassCount, OAI.EditApproximation.scheduledRefinementWordWithWork, OAI.EditApproximation.refinementFactor, OAI.EditApproximation.scheduledSeedFactor, OAI.EditApproximation.inputSmallLog
theorem OAI.EditApproximation.scheduledRefinementWordWithWork_bounds line 30
theorem OAI.EditApproximation.computedRefinementWords_bounds line 66
Source documentation
Width and range bounds for all five constructed scalar words. Tau and kappa share the same reciprocal fourth-power word.
```
theorem computedRefinementWords_bounds (N pass : ℕ) (word : List Bool)
    (hvalue : bitWordValue word = inputSmallLog N)
    (hwidth : word.length ≤ Nat.size (inputSmallLog N))
    (hH : 64 ≤ inputHeight N) (hpositive : 0 < bitWordValue word) :
    let parameters := BinaryFraction.onlineParametersWithWork word hpositive
…
```
Mentions: OAI.EditApproximation.bitWordValue, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight, OAI.EditApproximation.BinaryFraction.onlineParametersWithWork
theorem OAI.EditApproximation.refinementParameterWordsWithWork_values line 91
Source documentation
Concrete construction of the scalar words consumed by the local kernel.
```
theorem refinementParameterWordsWithWork_values (N pass : ℕ) (word : List Bool)
    (hpositive : 0 < bitWordValue word) (hvalue : bitWordValue word = inputSmallLog N)
    (hf : 3 ≤ smallLogExponent N) (hpass : pass ≤ computedSeedPassCount N) :
    let values := (refinementParameterWordsWithWork N pass word hpositive).1
…
```
Mentions: OAI.EditApproximation.bitWordValue, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.smallLogExponent, OAI.EditApproximation.computedSeedPassCount, OAI.EditApproximation.refinementParameterWordsWithWork
theorem OAI.EditApproximation.refinementParameterWordsWithWork_cost line 105