PreparedCorrection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Fixed geometry and numerical budgets for the adaptive iteration. All the fields below are constructed from the proved small-increment theorem.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.correctionOrder line 29
Source documentation
Construction starts at order ten, as required by the scale estimates.
```
def correctionOrder (k : ℕ) : ℕ := k+10
```
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.correctionInputOrder line 31
structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection line 37
Source documentation
Uniform geometric radii and the order-dependent estimates used by the iteration. This package is obtained by preparedCorrection_nonempty.
```
structure PreparedCorrection (d : CorrectionGeometry g F) where
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CorrectionGeometry
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.preparedCorrection_large line 81
Source documentation
No new analytic input is assumed in preparing the iteration. The fixed input budget exceeds four times the baseline, and each order's threshold preserves both the input and metric neighborhoods.
```
theorem preparedCorrection_large (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) (R : ℝ) :
    ∃ c : PreparedCorrection d.toCorrectionGeometry, R < c.budget/4 := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.preparedCorrection_nonempty line 117
Source documentation
The basic preparation follows by allowing any positive finite budget.
```
theorem preparedCorrection_nonempty (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) : Nonempty (PreparedCorrection d.toCorrectionGeometry) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection