ZeroOffsetStokes.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Removal of the positive offsets in the finite Stokes estimate. The hypothesis records arbitrarily close collar oscillation bounds, allowing upper semicontinuous boundary oscillation rather than assuming a limit.

theorem OAI.CircleDomainRigidity.zero_offset_stokes_bound line 16