Re-quantifying the Calderón--Zygmund pressure estimate for Theorem A

The established transfer pressureP1_thetaDecay_hCZ_of_global_slice turns one almost-every-time slice certificate for the centred first pressure potential of the decomposition prop:pressure-decomposition into the r-scaled extended-real Calderón--Zygmund estimate ext:CZ on the concentric parabolic sub-cylinder. The small-data statement thm:A consumes that estimate quantified over all suitable weak solutions at a fixed force exponent q, so the slice hypothesis must itself be uniform in the solution.

This file provides the single re-quantification adapter: from a slice certificate available for every suitable weak solution, it produces the solution-uniform ext:CZ estimate with the exact binder consumed downstream.

theorem CKN.Core.Endgame.theoremA_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 ρ)

Re-quantify the singly-centred slice certificate of prop:pressure-decomposition over all suitable weak solutions, yielding the solution-uniform r-scaled extended-real Calderón--Zygmund estimate ext:CZ on the concentric parabolic sub-cylinder.