Assembly of the regular-annulus lemma with whole-ball circulation #
lem:aniso:annulus is the paper's regular-annulus lemma: from a suitable weak solution smooth on
compact subsets of Q with a C²-bounded force, and radii R₁ < R₀ < 1, it produces a strictly
smaller annulus and a time t₀ on which u, ∇u, ∇²u are bounded, and a circulation bound on
every sub-radius. It has three ingredients: the choice of the annulus via the null Hausdorff
measure of the singular set (exists_annulus_bound_of_timeZeroSingularSetNull), the circulation
bound from an order-0 velocity bound, and the interior derivative estimate for the Navier–Stokes
system (Serrin, Section 4, m = 1). The last is the explicit hypothesis hserrin, as in
step_annulus_derivative_bounds; CIV.Main.regularAnnulus discharges it with
CIV.Main.serrinInteriorEstimates. The circulation bound here is the whole-ball form
forall_Rstar_exists_circulation_bound_ball_of_annulus_bound, which delivers the circulation
clause in the shape of the statement CIV.regularAnnulus, in place of the sub-annulus form
forall_Rstar_exists_circulation_bound_of_annulus_bound used by
exists_annulus_bound_conditional_on_serrin. The hypotheses hsolClassical, haxi and hfaxi
carry the data of the axis maximum principle that the whole-ball bound requires.
Representative radius between two annulus bounds #
The second theorem picks out a representative radius strictly between the two
annulus bounds Rm and Rp produced by the regular-annulus lemma, exactly as
lem:aniso:closure's proof does when it fixes R_* inside (R_-, R_+).