Nested one-sided cutoffs at arbitrary interior radii

A fixed cutoff is one near the closed inner cylinder and has past support in a larger cylinder. Its domain adaptation agrees with the fixed function as a germ at every nonpositive time, so all past derivative bounds remain independent of the domain and of its future-time collar.

theorem CKN.Core.Endgame.exists_fixed_nested_cutoff (a b : ℝ) (ha : 0 < a) (hab : a < b) : ∃ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ (∀ z ∈ tsupport ψ, z.1 ∈ Foundation.Parabolic.vec3Ball 0 b) ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z ∧ ψ z ≤ 1) ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), Foundation.Parabolic.parabolicHomeomorph.symm z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 a) → ψ =ᶠ[nhds z] fun (x : Foundation.Parabolic.Vec3 × ℝ) => 1) ∧ ∀ z ∈ tsupport ψ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 b

A fixed smooth cutoff is one near the closed radius-a cylinder and has nonpositive-time support in the radius-b cylinder, whenever 0<a<b.

theorem CKN.Core.Endgame.exists_domain_nested_cutoff_with_box (a b : ℝ) (ha : 0 < a) (hab : a < b) (hb : b < 1) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hsmooth : ContDiff ℝ (↑⊤) ψ) (hspace : ∀ z ∈ tsupport ψ, z.1 ∈ Foundation.Parabolic.vec3Ball 0 b) (hrange : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z ∧ ψ z ≤ 1) (hone : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), Foundation.Parabolic.parabolicHomeomorph.symm z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 a) → ψ =ᶠ[nhds z] fun (x : Foundation.Parabolic.Vec3 × ℝ) => 1) (hsupp : ∀ z ∈ tsupport ψ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 b) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hunit : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) : ∃ (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), φ ∈ spaceTimeTestFunction Ω I ∧ localBox Ω I Ω' J ∧ tsupport φ ⊆ Ω' ×ˢ J ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ φ z ∧ φ z ≤ 1) ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), Foundation.Parabolic.parabolicHomeomorph.symm z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 a) → φ =ᶠ[nhds z] fun (x : Foundation.Parabolic.Vec3 × ℝ) => 1) ∧ (∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 b) ∧ (∀ z ∈ tsupport φ, z.1 ∈ Foundation.Parabolic.vec3Ball 0 b) ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ≤ 0 → φ =ᶠ[nhds z] ψ

A nested fixed cutoff can be adapted to any domain containing the closed unit cylinder, retaining all past germs and a support-containing local product box.

theorem CKN.Core.Endgame.exists_uniform_nested_cutoff_derivative_bound (a b : ℝ) (ha : 0 < a) (hab : a < b) (hb : b < 1) : ∃ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (C : ℝ), 0 < C ∧ ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ), IsOpen Ω → IsOpen I → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∃ (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), φ ∈ spaceTimeTestFunction Ω I ∧ localBox Ω I Ω' J ∧ tsupport φ ⊆ Ω' ×ˢ J ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ φ z ∧ φ z ≤ 1) ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), Foundation.Parabolic.parabolicHomeomorph.symm z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 a) → φ =ᶠ[nhds z] fun (x : Foundation.Parabolic.Vec3 × ℝ) => 1) ∧ (∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 b) ∧ (∀ z ∈ tsupport φ, z.1 ∈ Foundation.Parabolic.vec3Ball 0 b) ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ≤ 0 → φ =ᶠ[nhds z] ψ) ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ≤ 0 → |φ z| ≤ C ∧ |timePartial φ z| ≤ C ∧ (∀ (i : Fin 3), |spatialPartial φ i z| ≤ C) ∧ |spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => φ (x, z.2)) z.1| ≤ C

One fixed function and one derivative constant work for every domain, for any nested radii 0<a<b<1. The future cutoff may depend on the domain.