The public statement CIV.Main.timeZeroSingularSetNull

This module proves the statement CIV.timeZeroSingularSetNull: from the uniform interior route (the top-cylinder Theorem A smallness of CIV.top_cylinder_smallness_of_gradient_small together with the Theorem A lower bound CIV.lintegral_gt_of_mem_singularSlice at a point of the singular slice), the scale-invariant Dirichlet integral of the spatial gradient over top-boundary cylinders based at a singular point has limsup, as the radius shrinks to 0 from the right, bounded below by a universal positive constant. The spatial Vitali covering step CIV.hausdorffMeasure_one_null_of_gradient_density, fed by that lower bound through CIV.density_of_le_limsup and the finite global Dirichlet integral of CIV.lintegral_gradSq_lt_top, then gives the one-dimensional Hausdorff-measure-zero conclusion.

theorem CIV.Main.timeZeroSingularSetNull (q : ℝ) (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) (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (henergy : GlobalEnergyClass u Du p) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hMf : ForceC2Bounded f) : (MeasureTheory.Measure.hausdorffMeasure 1) (singularSlice u ∩ CKN.Foundation.Parabolic.vec3Ball 0 1) = 0

The public statement of time-zero partial regularity: the set of points of the open unit ball near which u is unbounded on every backward parabolic neighbourhood ending at the blow-up time t = 0 has one-dimensional Hausdorff measure zero, proved from the uniform interior route through the top-cylinder Theorem A smallness and the spatial Vitali covering step.