MaskedStageStokes.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Apply finite Stokes to an actual masked coordinate stage. The real terminal lifts and their complete excess budget are derived from that stage, with the singular terminal omitted.

theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.stokes_bound line 15