The ext:CZ pressure interface of thm:B

The Calderón--Zygmund display ext:CZ for the centred first pressure potential enters the theta-decay display of thm:B as an almost-every-time time-slice certificate: membership of pressureP1 in L^{3/2} on the space slice together with a ball-local lpNorm bound in terms of utensorNorm. The slice transfer pressureP1_thetaDecay_hCZ_of_global_slice converts one such certificate into the r-scaled extended-real estimate on the concentric parabolic sub-cylinder.

This module re-quantifies that transfer over all suitable weak solutions at a fixed integrability exponent, so a single named hypothesis supplies the exact pressure binder consumed by the gradient criterion of thm:B. The constant relation is the one exposed by the transfer: the cylinder constant C₁₂_p1 dominates C_CZ * (9 * sobolevPoincareL6Constant).

theorem CKN.Core.Endgame.theoremB_hCZ_p1_of_slice_bounds (q C₁₂_p1 C_CZ : ℝ) (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)) (Ω : 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 ρ)

ext:CZ for the centred first pressure potential, at fixed exponent. Given the Calderón--Zygmund slice certificate for pressureP1, uniform over all suitable weak solutions at a fixed q and with a single constant C_CZ, the theta-decay pressure binder of the gradient criterion holds for every solution. The slice hypothesis is the almost-every-time MemLp membership at exponent 3/2 together with the ball-local lpNorm bound in terms of utensorNorm; the conclusion is exactly the pressureP1 display consumed by the gradient criterion.