The first-round source data on an arbitrary parabolic ball

prop:bootstrap improves u ∈ M^{3,25/3} to u ∈ M^{3,25} in one round. The round localizes eq:local-equation by a cutoff adapted to the parabolic ball 𝔅_R(z₀) and reads the two sources of the heat representation at the exponents 1/κ₂ = 1/τ + 1/τ₃ = 3/25 + 8/25 = 11/25: the heat slot in M^{6/5,25/11} and the derivative slot in M^{3,25/6}.

The statement below is the complete data of that localization — the cutoff, its compactly interior product box, the measurability and compact support of both sources, the two source Morrey norms certified finite, and the vanishing of both sources outside the half ball. The centre and radius are arbitrary and the carrier is the symmetric parabolic ball, not a one-sided cylinder.

theorem CKN.Core.Step4.first_round_source_package_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {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 : ℝ), 0 < R → Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I → morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u → (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) → ∀ {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) → morreyVecMem (6 / 5) (min q (25 / 11)) (Metric.ball z₀ (R / 2)) Dp → ∃ (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ) (KF : ENNReal) (KG : ENNReal), φ ∈ spaceTimeTestFunction Ω I ∧ localBox Ω I U J ∧ tsupport φ ⊆ U ×ˢ J ∧ U ×ˢ J ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (R / 2) ∧ (∀ z ∈ Metric.ball z₀ (R / 4), φ (z.1, z.2) = 1) ∧ (∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i) MeasureTheory.volume) ∧ (∀ (j i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceH φ u j z i) MeasureTheory.volume) ∧ (∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i) ∧ (∀ (j i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceH φ u j z i) ∧ KF < ⊤ ∧ KG < ⊤ ∧ (∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i) ≤ KF) ∧ (∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceH φ u j z i) ≤ KG) ∧ (∀ z ∉ Metric.ball z₀ (R / 2), localizedGradientSourceG φ u Du f Dp z = 0) ∧ ∀ (j : Fin 3), ∀ z ∉ Metric.ball z₀ (R / 2), localizedGradientSourceH φ u j z = 0

The first-round localized source data of eq:local-equation on the parabolic ball 𝔅_R(z₀), at the paper's first-round exponents (6/5, 25/11) for the heat slot and (3, 25/6) for the derivative slot.