ActualPhaseGoodness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Pure global phases remain good when read in any overlapping atlas chart. This supplies the geometric input to the compact weight choice.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase_unit_read_good line 25