Clipped origin growth from the fixed derivative decomposition

The harmonic and far-force temporal envelope is the same input as in the fixed-field derivative construction. A finite relative cover of the backward origin carrier transfers the local signed decompositions to one measurable weak gradient. Its actual clipped spatial norms supply the growth estimate. The finite-cover argument uses the same-repository collar assembly pattern; its backward patches include the final time without requiring future Morrey data.

Backward patches up to the final time of an origin carrier

Relative neighborhoods of the closed inner carrier are covered by spatial half-balls and backward windows contained in the larger Morrey carrier. At final time zero the neighborhood extends past zero, while its intersection with the carrier is still controlled by a backward window ending at zero.

theorem CKN.Core.Step4.originClause_backward_derivative_patch {R₀ R₁ : ℝ} (hR₁ : 0 < R₁) (hgap : R₁ < R₀) {w : Foundation.Parabolic.ParabolicPoint} (hw : w ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁)) : ∃ (z : Foundation.Parabolic.ParabolicPoint) (ρ : ℝ) (U : Set Foundation.Parabolic.ParabolicPoint), 0 < ρ ∧ IsOpen U ∧ w ∈ U ∧ closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₀) ∧ Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 R₀ ∧ Foundation.Parabolic.vec3Ball z.1 (ρ / 2) ⊆ Foundation.Parabolic.vec3Ball 0 R₀ ∧ U ∩ Foundation.Parabolic.parabolicCylinder 0 0 R₁ ⊆ Foundation.Parabolic.vec3Ball z.1 (ρ / 2) ×ˢ Set.Ioc (z.2 - ρ ^ 2) z.2

A closed-carrier point has a relatively open neighborhood controlled by one fixed backward localization entirely inside the larger carrier.

theorem CKN.Core.Step4.originClause_localBox_of_closed_cylinder {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : localBox Ω I (Foundation.Parabolic.vec3Ball z.1 ρ) (Set.Ioc (z.2 - ρ ^ 2) z.2)

Closed cylinder containment gives the exact spatial ball and backward window as a local suitable-solution box.

theorem CKN.Core.Step4.originClause_closed_carrier_compact {R : ℝ} (hR : 0 < R) : IsCompact (closure (Foundation.Parabolic.parabolicCylinder 0 0 R))

The closure of a backward origin carrier is compact.

theorem CKN.Core.Step4.originClause_derivative_morrey_of_shared_remainder (hrem : ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {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 → ∃ (M : ℝ → ENNReal), AEMeasurable M MeasureTheory.volume ∧ ∫⁻ (s : ℝ), M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) x i‖ₑ ≤ M s) {q τ R₀ R₁ : ℝ} {KU KD : ENNReal} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτhi : τ ≤ 25) (hR₁ : 0 < R₁) (hgap : R₁ < R₀) (hR₀ : R₀ < 1) (hKU : KU < ⊤) (hKD : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hU : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => u w i) ≤ KU) (hDu : ∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Du w i j) ≤ KD) : ∃ (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) ∧ ∀ (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) < ⊤

The fixed harmonic/far temporal-envelope input gives finite Morrey norms of one selected weak pressure derivative on the entire backward origin carrier. Only the original larger-carrier velocity and gradient Morrey data are used.

theorem CKN.Core.Step4.originClause_clipped_growth_of_shared_remainder (hrem : ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {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 → ∃ (M : ℝ → ENNReal), AEMeasurable M MeasureTheory.volume ∧ ∫⁻ (s : ℝ), M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) x i‖ₑ ≤ M s) {q τ R₀ R₁ : ℝ} {KU KD : ENNReal} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτhi : τ ≤ 25) (hR₁ : 0 < R₁) (hgap : R₁ < R₀) (hR₀ : R₀ < 1) (hKU : KU < ⊤) (hKD : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hU : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => u w i) ≤ KU) (hDu : ∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Du w i j) ≤ KD) : ∃ (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) ∧ ∃ A < ⊤, ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 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) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

The actual clipped slice norms of one selected derivative obey the origin clause's growth formula with a single finite coefficient before all components, centres, and positive radii. The only analytic input beyond the standing solution data is the shared fixed harmonic/far temporal envelope.