Consuming the constructed indexed L² endpoint

The smooth global Hessian estimate supplies the indexed L² input, and the concrete restricted weak endpoint is instantiated. The first-potential pairing supplies the weak-gradient identity without an analytic input.

theorem CKN.Core.Endgame.concrete_riesz_tensor_distributional_identity {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), (∑ i : Fin 3, ∑ j : Fin 3, Foundation.Euclidean.rieszSecondP1ExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ (G i j) x) * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * mixedSecond ψ i j x

The concrete L² construction discharges the endpoint input in the global tensor-extension pressure pairing.

theorem CKN.Core.Endgame.exists_weak_pressure_gradient_of_concrete_riesz_extension (C_CZ : ℝ) (hconst : 3 * Foundation.Euclidean.czGradientComponentConstant Foundation.Euclidean.rieszSecondWeakTypeConstant 1 ≤ C_CZ) (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 C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The concrete endpoints and first-potential pairing supply the signed weak-gradient bound without an additional analytic premise.