A first-round localization cutoff at arbitrary centre

Paper label eq:local-equation localizes the equation to a parabolic ball of arbitrary centre and radius. This file supplies the geometry and the smooth cutoff that the first bootstrap round uses. The open parabolic box B_r(x) × (t - r², t + r²) is exactly the parabolic metric ball of eq:parabolic-ball read through spaceTimeSet, the same set is its own preimage along the product identification, and a ball sitting compactly inside the space-time domain admits a smooth cutoff equal to one on the inner quarter-ball, supported inside the three-eighths-ball, and contained in the product box of half radius.

theorem CKN.Core.Step4.parabolic_box_eq_ball (z₀ : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : spaceTimeSet (Foundation.Parabolic.vec3Ball z₀.1 r) (Set.Ioo (z₀.2 - r ^ 2) (z₀.2 + r ^ 2)) = Metric.ball z₀ r

Equation eq:local-equation, in box form: spaceTimeSet applied to the spatial ball vec3Ball z₀.1 r and the time interval (z₀.2 - r², z₀.2 + r²) is the parabolic metric ball Metric.ball z₀ r of eq:parabolic-ball.

theorem CKN.Core.Step4.parabolic_box_subset_ball_preimage (z₀ : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : Foundation.Parabolic.vec3Ball z₀.1 r ×ˢ Set.Ioo (z₀.2 - r ^ 2) (z₀.2 + r ^ 2) ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ r

Equation eq:local-equation, preimage form: the product box of spatial ball and open time interval is contained in the preimage of the parabolic metric ball under the product identification parabolicHomeomorph.symm.

theorem CKN.Core.Step4.exists_first_round_cutoff {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I) : ∃ φ ∈ spaceTimeTestFunction Ω I, (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ φ z ∧ φ z ≤ 1) ∧ (∀ z ∈ Metric.ball z₀ (R / 4), φ (z.1, z.2) = 1) ∧ tsupport φ ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (3 * R / 8) ∧ localBox Ω I (Foundation.Parabolic.vec3Ball z₀.1 (R / 2)) (Set.Ioo (z₀.2 - (R / 2) ^ 2) (z₀.2 + (R / 2) ^ 2)) ∧ tsupport φ ⊆ Foundation.Parabolic.vec3Ball z₀.1 (R / 2) ×ˢ Set.Ioo (z₀.2 - (R / 2) ^ 2) (z₀.2 + (R / 2) ^ 2)

Equation eq:local-equation, first-round cutoff: a parabolic ball of radius 2R inside the space-time domain Ω × I admits a smooth cutoff φ with values in [0, 1], equal to one on the ball of radius R/4, supported in the ball of radius 3R/8, and supported in the product box of spatial radius R/2 and time half-width (R/2)², which is compactly interior to Ω × I.