AdaptiveExactControl.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed exact correction retains the C² geometry budget.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.exact_correction_with_control line 19
Source documentation
The same, concretely constructed limit is isometric and close in C² to both the initial stage and the fixed reference immersion.
```
theorem exact_correction_with_control (c : PreparedCorrection d)
    (hF : ContMDiff planeModel spaceModel ∞ F) {t : ℝ} (ht : 0 < t) (htsmall : t ≤ 1/32)
    (seed : c.Stage t 0) :
    ∃ G : M → Space, IsSmoothIsometricImmersion M g G ∧
      d.A.WeightedBound 1 2 (2*c.ρ*t) (G-seed.map) ∧
      d.A.WeightedBound 1 2 (c.ρ/4) (G-F) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion