A lower bound on the Theorem A quantity at a singular point of the blow-up slice

At a point of the singular set of the blow-up-time slice, the dimensionless smallness quantity of CIV.norm_le_of_small_L3_top_of_continuousOn cannot be small on any backward cylinder based at that point: were it small, the continuous ε-regularity conclusion would give an everywhere bound on u near the point, contradicting singularity. This is the contrapositive used at step 2 of design note R12.

theorem CIV.lintegral_gt_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 → ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder → ∀ (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ), 0 < r → r ≤ 1 → CKN.Foundation.Parabolic.vec3Ball x r ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1 → x ∈ singularSlice u → ENNReal.ofReal (ε₀ * r ^ 2) < ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x r ×ˢ Set.Ioo (-r ^ 2) 0, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (r ^ (3 * q - 3)) * ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q

At a point of singularSlice u, the Theorem A smallness quantity exceeds ε₀ r² on every backward cylinder of radius r ≤ 1 centered there and contained in the unit ball, for the same universal ε₀ as CIV.norm_le_of_small_L3_top_of_continuousOn.