GenericIndependentPhases.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One finite phase family simultaneously has nondegenerate boundary critical points and the required independent crossing covectors. All parameters can be chosen in an arbitrarily prescribed open neighborhood.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_generic_independent_phases line 16