Composition of the small-data regularity theorem

This module writes the proof of thm:A once, in the order of the manuscript, as a family of statements each of which assumes one remaining display. The theorem does not go through this file: it is proved by CKN.Core.Endgame.epsilonRegularityL3_of_instance_slots_q, whose proof is the same composition with the pressure-gradient hypothesis narrowed to the two exponent-radius triples that thm:A actually consumes. Read this file for the shape of the argument and that one for what is checked.

epsilonRegularityL3_closer_of_pending_inputs is that shape. Reading its proof against the manuscript:

• thetaDecay_T_of_inputs is eq:theta-decay-2, and fixes κ, η, Λ₀ of conv:kappa.
• theoremA_initial_uniform_of_displays is the start lemma lem:thmA-start together with Steps 1 and 2 of the proof of thm:A: the scale iteration prop:iteration at every centre of Q_{3/4}, giving eq:thmA-morrey, and the one-sided Morrey transfer onto the cylinder of radius 11/16, giving eq:step2-morrey for the velocity and its gradient. The manuscript states the transfer on Q₂^♯ of radius 5/8; the larger radius is proved here because the bootstrap round of prop:bootstrap consumes the outer cylinder and produces the inner one. The pressure Morrey norm of eq:step2-morrey is available from the same transfer and is not needed downstream, exactly as in the manuscript.
• exists_uniform_bootstrap_of_initial_pressure is prop:bootstrap at τ = τ₂ = 25/3, with the sources split at t = 0 as in Step 3, taking the velocity from 𝓜^{3,25/3} on radius 11/16 to 𝓜^{3,25} on radius 5/8. This is the single round of cor:one-round.
• exists_uniform_halfCylinder_of_final_pressure is thm:endgame on the one-sided cylinder, again with the sources split at t = 0. It consumes the velocity in both 𝓜^{3,25} and 𝓜^{3,25/3}, and produces the Hölder representative of thm:A with exponent γ₀ = min {2 - 5/q, 1/5} of eq:gamma-value.
• The hypothesis hGA is lem:pressure-gradient-morrey, asked for at the two triples (τ, R₀, R₁) = (25/3, 11/16, 43/64) and (25, 5/8, 19/32). Its Morrey exponent min ((1/τ + 8/25)⁻¹) q of eq:pressure-gradient-morrey is 25/11 at the first triple and min {q, 25/9} at the second.

The carrier of the pressure gradient is the backward cylinder about the origin rather than a symmetric parabolic ball: the only containment thm:A supplies is closure (parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I, and a symmetric ball about any point of that set contains times after it. The numerical majorant is oneSidedPressureGradientKPAffine, and all numerical constants are fixed before the solution fields.

theorem CKN.Core.Endgame.epsilonRegularityL3_closer_of_pending_inputs (q C₁₂_p1 C_CZ : ℝ) (hq : 5 / 2 < q) (hC : 0 ≤ C_CZ) (hCZ_p1 : ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} (hρ : 0 < ρ), 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm' (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f w.2 w.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal (C₁₂_p1 * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)) (hGA : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∃ KP < ⊤, ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I U J → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

The small-data conclusion thm:A from the two remaining pressure displays. The oscillation display eq:lin35-force and the localized heat representation of lem:local-equation are discharged by their suitable-weak-solution theorems.

theorem CKN.Core.Endgame.epsilonRegularityL3_closer_of_slice_and_quantitative (q C₁₂_p1 C_CZ : ℝ) (hq : 5 / 2 < q) (hC_CZ : 0 ≤ C_CZ) (hconst : C_CZ * (9 * sobolevPoincareL6Constant.toReal) ≤ C₁₂_p1) (hSlice : ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ), closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3)) (hGA : Step4.oneSidedPressureGradientQuantitative) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

The same conclusion from the two displays in the shape their own arguments produce them: the almost-every-time slice certificate of ext:CZ and the explicit-majorant form of prop:bootstrap.

theorem CKN.Core.Endgame.epsilonRegularityL3_closer_of_two_displays (q C_CZ : ℝ) (hq : 5 / 2 < q) (hC_CZ : 0 ≤ C_CZ) (hSlice : ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ), closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3)) (hGA : Step4.oneSidedPressureGradientQuantitative) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

The exact conclusion of thm:A from two displays. The cylinder constant of ext:CZ is fixed to the value the slice transfer produces, so the only data preceding the solution are the force exponent and the slice constant of ext:CZ, and the only assumptions are the almost-every-time slice certificate of ext:CZ and the explicit-majorant display prop:bootstrap. Apart from those two, this is the statement of thm:A verbatim.

theorem CKN.Core.Endgame.epsilonRegularityL3_closer_of_cell_and_slice (q C_CZ : ℝ) (hq : 5 / 2 < q) (hC_CZ : 0 ≤ C_CZ) (hSlice : ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ), closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3)) (hcell : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I U J → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ Step4.oneSidedPressureGradientOriginCellOutput R₁ (min (1 / τ + 8 / 25)⁻¹ q) (Step4.oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD) Dp) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

Reduction to pressure-gradient and bootstrap estimates. The pressure-gradient input is reduced to the origin-cell estimate of prop:bootstrap, and the pressure input to the almost-every-time slice certificate of ext:CZ; the cylinder constant is fixed by the slice transfer. Everything else in thm:A is proved.

theorem CKN.Core.Endgame.epsilonRegularityL3_closer_of_gradient_display (q : ℝ) (hq : 5 / 2 < q) (hGA : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD < ⊤ ∧ ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I U J → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

thm:A from the one-sided pressure-gradient display alone. With the Calderón--Zygmund estimate ext:CZ supplied at solution level, the oscillation display eq:lin35-force of prop:lin34 supplied by its own theorem, and the localized heat representation of lem:local-equation supplied by its own theorem, the explicit-majorant form of prop:bootstrap is the only remaining assumption. Apart from it, this is the statement of thm:A verbatim.

theorem CKN.Core.Endgame.epsilonRegularityL3_closer_of_cell_producer (q : ℝ) (hq : 5 / 2 < q) (hcell : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I U J → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ Step4.oneSidedPressureGradientOriginCellOutput R₁ (min (1 / τ + 8 / 25)⁻¹ q) (Step4.oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD) Dp) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

thm:A from the origin-cell estimate of prop:bootstrap alone. This is the deepest reduction available: every other display used by the small-data argument is proved, and the single assumption is the Morrey-cell bound for the selected pressure gradient on the one-sided cylinder.

theorem CKN.Core.Endgame.theoremA_clipped_growth_of_carrier_morrey {κ R₁ : ℝ} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hm : Measurable Dp) (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) : ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ (∑ j : Fin 3, Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w j) ^ (6 / 5)) * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))

The carrier Morrey norms of a measurable field bound its clipped slice integrals on every cell.

theorem CKN.Core.Endgame.theoremA_hGA_of_full_sum_comparison (hFullSumComparison : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) → oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) R₁ (∑ i : Fin 3, Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) ^ (6 / 5)) ((∑ i : Fin 3, Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) ^ (6 / 5)) * ENNReal.ofReal (R₁ ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) ≤ Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD) (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) : 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD < ⊤ ∧ ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I U J → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD

The concrete temporal remainder and the full-sum comparison give the pressure-gradient bound with the enlarged numerical constant.

theorem CKN.Core.Endgame.epsilonRegularityL3_closer_of_full_sum_comparison (hFullSumComparison : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) → oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) R₁ (∑ i : Fin 3, Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) ^ (6 / 5)) ((∑ i : Fin 3, Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) ^ (6 / 5)) * ENNReal.ofReal (R₁ ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) ≤ Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD) (q : ℝ) (hq : 5 / 2 < q) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

The small-data regularity conclusion from the full-sum comparison, with the temporal remainder and carrier time estimates supplied by suitability.