WhitneyStartingGeometry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Starting geometry from the precise published C1 surface-immersion input. The upgrade to a smooth immersion is proved by finite-atlas convolution.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_three_space_immersion_of_whitney line 19
Source documentation
Whitney (1944), Theorem 8 supplies only the C1 immersion. Its smoothing is carried out here without adding a further published-input hypothesis.
```
theorem smooth_three_space_immersion_of_whitney
    (hW : PublishedInputs.WhitneySurfaceInput M) :
    ∃ f : M → PublishedInputs.ThreeSpace,
      ContMDiff planeModel 𝓘(ℝ,PublishedInputs.ThreeSpace) ∞ f ∧
      ∀ p, Function.Injective (mfderiv planeModel 𝓘(ℝ,PublishedInputs.ThreeSpace) f p) := by
…
```
Mentions: OAI.ClosedSurfaceR4.PublishedInputs.WhitneySurfaceInput, OAI.ClosedSurfaceR4.PublishedInputs.ThreeSpace, OAI.ClosedSurfaceR4.planeModel
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.metricPhaseData_of_whitney line 30
Source documentation
The cited Whitney input yields a smooth spherical immersion together with the actual finite phase data used by the metric correction.
```
theorem metricPhaseData_of_whitney (g : SmoothMetric M)
    (hW : PublishedInputs.WhitneySurfaceInput M) :
    ∃ G : M → Space, ContMDiff planeModel spaceModel ∞ G ∧
      (∀ p, ‖G p‖ = 1) ∧
      (∀ p, Function.Injective (mfderiv planeModel spaceModel G p)) ∧
      Nonempty (MetricGoodPhaseData g G) := by
…
```
Mentions: OAI.ClosedSurfaceR4.SmoothMetric, OAI.ClosedSurfaceR4.PublishedInputs.WhitneySurfaceInput, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData