MetricGoodPhaseData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual metric-adapted phase geometry, including all cross-chart quadratic phases needed by the small-increment construction.

structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData line 35
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.nonempty line 59
Source documentation
A metric and an immersion with nonzero coordinate second form produce all the fixed phase geometry required by the analytic step.
```
theorem nonempty (g : SmoothMetric M) {F : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F)
    (hImm : ∀ p, Function.Injective (mfderiv planeModel spaceModel F p))
    (hB : ∀ p, ∃ v w : SmallModes.Base,
      realSecondForm (coordinateMap F p) v w (coordinateCenter p) ≠ 0) :
    Nonempty (MetricGoodPhaseData g F) := by
…
```
Mentions: OAI.ClosedSurfaceR4.SmoothMetric, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.coordinateMap, OAI.ClosedSurfaceR4.coordinateCenter, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData