The singular slice at the blow-up time

lem:aniso:annulus starts from the set of points of the closed ball where the velocity fails to be bounded on every backward parabolic neighbourhood ending at the blow-up time t = 0. Design note R12 records why this set, rather than a boundary version of CKN's singular set, is what the argument needs: CKN's partial-regularity theorems are stated with a limsup gradient hypothesis on open space-time sets and cannot be evaluated at t = 0 itself (design note R3).

IsBoundedNear u x is the scale-invariant version of BoundedNearOrigin, centred at a general point x and with the backward time window tied to the spatial radius; the singular slice singularSlice u is its failure set. The set is closed (isClosed_singularSlice), invariant under the axis rotations on the open unit ball when u is axisymmetric (rotZ_mem_singularSlice_iff), and agrees with BoundedNearOrigin at the origin (boundedNearOrigin_iff). The closing step of design note R12 — a sphere disjoint from the singular slice carries a uniform bound on a whole space-time annulus around it — is exists_annulus_bound_of_sphere_disjoint, obtained from compactness of the sphere by a finite-cover argument.

Two shrinking lemmas

Openness and closedness

theorem CIV.isOpen_isBoundedNear (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : IsOpen {x : CKN.Foundation.Parabolic.Vec3 | IsBoundedNear u x}

The set of points near which u is bounded is open: design note R12 needs the complementary singular slice to be closed.

theorem CIV.isClosed_singularSlice (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : IsClosed (singularSlice u)

The singular slice at the blow-up time is closed, being the complement of the open set of points of local boundedness.

Rotation invariance on the open unit ball

theorem CIV.image_rotZ_vec3Ball (φ r : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ '' CKN.Foundation.Parabolic.vec3Ball x r = CKN.Foundation.Parabolic.vec3Ball (rotZ φ x) r

The image of a Euclidean ball under a rotation about the vertical axis is the Euclidean ball of the same radius around the rotated centre: rotations preserve the Euclidean norm, so membership in the rotated ball transports along rotZ (-φ).

theorem CIV.rotZ_mem_singularSlice_iff {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {x : CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) (φ : ℝ) : rotZ φ x ∈ singularSlice u ↔ x ∈ singularSlice u

On the open unit ball, an axisymmetric field's singular slice is invariant under the axis rotations: Q_φ x is singular exactly when x is (design note R12, used to transport the smallness estimate around the torus swept by a ball).

Comparison with BoundedNearOrigin

theorem CIV.boundedNearOrigin_iff {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} : BoundedNearOrigin u ↔ IsBoundedNear u 0

At the origin, IsBoundedNear agrees with BoundedNearOrigin: the two constants r and δ of BoundedNearOrigin can always be replaced by the single radius min r (√δ), whose square is at most δ, and conversely δ = r² recovers BoundedNearOrigin from IsBoundedNear directly.

A uniform bound on an annulus disjoint from the singular slice

theorem CIV.exists_annulus_bound_of_sphere_disjoint {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R : ℝ} (hR : 0 < R) (hdisj : ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm x = R → x ∉ singularSlice u) : ∃ (δ : ℝ) (t₀ : ℝ) (M : ℝ), 0 < δ ∧ t₀ ∈ Set.Ioo (-1) 0 ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), R - δ < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < R + δ → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ M

If a sphere {|x| = R} carries no singular point, some annulus around it, over some backward time window, carries a single bound for u: the closing step of design note R12, obtained by covering the compact sphere by finitely many bounded-near balls and taking a Lebesgue-number–style radial projection.