Past-time invariance of the localized gradient-slot sources

The admissible cutoff and the fixed cutoff agree as germs at nonpositive times. Their actual truncated equation sources therefore agree, including the pressure gradient in the order-two slot. This is an identity of formulas; it does not assert the still-needed localized representation theorem.

noncomputable def CKN.Core.Endgame.causalGradientSourceComponent (φ : Foundation.Parabolic.ParabolicPoint → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (i : Fin 3) : Foundation.Parabolic.ParabolicPoint → ℝ

The actual past-time order-two source with the pressure gradient.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Endgame.cutoff_coefficients_zero_on_past_outside_intermediate {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) {z : Foundation.Parabolic.ParabolicPoint} (ht : z.2 ≤ 0) (hz : z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) : φ z = 0 ∧ timePartial φ z = 0 ∧ (∀ (j : Fin 3), spatialPartial φ j z = 0) ∧ spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => φ (x, z.2)) z.1 = 0

All coefficients of a smooth cutoff vanish in the past outside its prescribed intermediate-cylinder support.

theorem CKN.Core.Endgame.causalGradientSourceComponent_zero_outside_intermediate {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (i : Fin 3) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) : causalGradientSourceComponent φ u Du f Dp i z = 0

The actual causal gradient-slot source vanishes outside the intermediate cylinder, regardless of the fields outside it.