Domain localization preserving a fixed negative-time cutoff

The fixed smooth cutoff is chosen independently of the domain. Multiplying it by a cutoff equal to one near the closed unit cylinder makes it admissible on any open domain containing that cylinder. At every point of time at most zero, the resulting function agrees locally with the fixed cutoff. Thus its negative-time derivatives do not acquire domain-dependent constants.

theorem CKN.Core.Endgame.exists_localBox_around_closed_unit {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hunit : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) : ∃ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J ∧ IsOpen J ∧ closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω' J

The closed unit cylinder admits a compactly interior product box with an open time interval, without any connectedness assumption on the ambient time set.