The criterion the covering step consumes

At a point of the singular slice of the blow-up-time slice, the scale-invariant Dirichlet integral of the spatial gradient over top-boundary cylinders cannot shrink to 0 faster than linearly in the radius: its limsup, as the radius shrinks to 0 from the right, is bounded below by a universal positive constant. This is the contrapositive of the top-cylinder Theorem A smallness of CIV.top_cylinder_smallness_of_gradient_small, composed with the Theorem A lower bound CIV.lintegral_gt_of_mem_singularSlice at a point of the singular slice: were the limsup below the threshold, the gradient integral would eventually be small enough on some (0, r₀] to feed the uniform interior Morrey decay chain, producing a radius at which the Theorem A smallness quantity falls below its own universal lower bound at a singular point, a contradiction.

theorem CIV.le_limsup_gradient_of_mem_singularSlice (q : ℝ) (hq : 5 / 2 < q) : ∃ (ε₁ : ℝ), 0 < ε₁ ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f → GlobalEnergyClass u Du p → ForceC2Bounded f → ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder → ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 1, x ∈ singularSlice u → ENNReal.ofReal ε₁ ≤ Filter.limsup (fun (r : ℝ) => (ENNReal.ofReal r)⁻¹ * ∫⁻ (w : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x r ×ˢ Set.Ioo (-r ^ 2) 0, ENNReal.ofReal (CKN.spatialGradientSq u Du w)) (nhdsWithin 0 (Set.Ioi 0))

The criterion the spatial Vitali covering step consumes: at a point of the singular slice inside the open unit ball, the limsup, as the radius shrinks to 0 from the right, of the scale-invariant Dirichlet integral of the spatial gradient over the top-boundary cylinder based at that point, is bounded below by a universal positive constant ε₁.