Fixed-collar assembly of the pressure slice majorant

Local signed pressure decompositions give Morrey control on a finite cover of the enlarged cell carrier. Weak-derivative uniqueness transfers those bounds to one measurable field. The only external analytic input is the fixed harmonic and far-force remainder's temporal majorant.

theorem CKN.Core.Step4.shared_binder_of_remainder_majorant (hRemainderMajorant : ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ}, 5 / 2 < 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.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, 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 τ : ℝ) : 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → ∀ {Ω : 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 : ℝ), 0 < R → Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I → morreyVecMem 3 τ (Metric.ball z₀ R) u → (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) → ∃ (A : ENNReal) (N : Fin 3 → Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal), A < ⊤ ∧ (∀ (i : Fin 3) (c : Foundation.Parabolic.Vec3) (t ρ : ℝ), 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder c t ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - ρ ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (euclideanBall c (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall c (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall c (ρ / 2))) ≤ N i c t ρ s) ∧ ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → r ≤ R / 16 → (Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ Metric.ball z₀ (R / 2)).Nonempty → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2, N i z.1 z.2 (2 * r) s ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

A finite 3/2 temporal majorant for the fixed harmonic and far-force remainder supplies the shared small-cell pressure-gradient bound, uniformly in the full admissible range of Morrey exponents.