GenericPulledPhases.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Generic phase selection after the actual invertible chart pullbacks. The two phase covectors at each crossing are expressed in one tangent chart before testing their determinant.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_generic_pulled_phases line 16