The slice pressure-gradient bound with the explicit endpoint constant

pressure_slice_bound_of_riesz_weak_extension takes the selected weak-gradient family as a hypothesis. That hypothesis is now available without any analytic input: the completed L^{6/5} extension of the second Riesz transforms provides the field, its pairing with the first potential, and the numerical bound, with the explicit constant czGradientOperatorConstant. The two statements below record the selected family at that constant and the resulting slice bound, so the pressure gradient on a slice is controlled with no Calderón--Zygmund premise.

theorem CKN.Core.Step4.exists_weak_pressure_gradient_unconditional (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal Foundation.Euclidean.czGradientOperatorConstant * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The selected weak gradient of the first potential exists with the explicit constant czGradientOperatorConstant, with no analytic premise.

theorem CKN.Core.Step4.pressure_slice_bound_unconditional {B B' : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {p H gh G : Foundation.Parabolic.Vec3 → ℝ} {i k : Fin 3} {ρ C : ℝ} (hC : Foundation.Euclidean.czGradientOperatorConstant ≤ C) (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGc : HasCompactSupport G) (hrep : p =ᵐ[MeasureTheory.volume.restrict B] pressureNewtonianDerivativePotential i G + H) (hH : HasWeakPartialDerivOn B k H gh) (hPloc : MeasureTheory.LocallyIntegrableOn (pressureNewtonianDerivativePotential i G) B MeasureTheory.volume) (hHloc : MeasureTheory.LocallyIntegrableOn H B MeasureTheory.volume) (hghloc : MeasureTheory.LocallyIntegrableOn gh B MeasureTheory.volume) (hgh : MeasureTheory.eLpNorm gh (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B)) : ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k p g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * (MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B))

The slice bound of the pressure gradient, with the Calderón--Zygmund input discharged by the completed extension. Only the local representation p = ∂ᵢN * G + H, the harmonic slice bound for H, and the local integrability data remain; the constant is any C at least czGradientOperatorConstant.