The source-data input is supplied through pressureUTensor_source_data_ae_of_sws from SliceVelocityCube.lean. That solution-level package combines the local velocity L³ slice with the fixed- time tensor-source estimate, returning all nine L^{3/2} components, compact support, and the matching factor-27 source bound. This is the normalization already consumed by the singly centred pressure assembly.

theorem CKN.theoremA_hCZ_p1_of_sws (q : ℝ) (Ω : 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 (czP1ThetaDecayConstant * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)

The exact singly centred pressure input required by Theorem A, from suitability alone. Its coefficient is fixed before the solution data.