AccuracyPrefixInspection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The uniform program inspects only a logarithmically bounded prefix of each accuracy word. An encoding exceeding this bound takes the exact fallback, without first scanning or retaining its unbounded suffix.

theorem OAI.EditApproximation.inspectBitPrefix_accepts line 18
Source documentation
One step reads a constructor of the input word.
```
 theorem inspectBitPrefix_accepts (budget : ℕ) (word : List Bool) :
    (inspectBitPrefix budget word).1 = true ↔ word.length ≤ budget := by
…
```
Mentions: OAI.EditApproximation.inspectBitPrefix
theorem OAI.EditApproximation.inspectBitPrefix_cost line 27
theorem OAI.EditApproximation.inspectAccuracyWithWork_spec line 40
Source documentation
On acceptance the input words are already bounded; returning the input value only retains those bounded words.
```
 theorem inspectAccuracyWithWork_spec (budget : ℕ) (epsilon : BinaryFraction) :
    (inspectAccuracyWithWork budget epsilon).1 =
      if epsilon.width ≤ budget then some epsilon else none := by
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.inspectAccuracyWithWork
theorem OAI.EditApproximation.inspectAccuracyWithWork_cost line 51
theorem OAI.EditApproximation.inspectAccuracy_eventually_accepts line 59