Derivatives of a locally constant cutoff

The first spatial, second spatial, and time derivatives of a smooth scalar factor vanish wherever it is locally constant. This identifies the support of the phase-cutoff errors in lem:bu-small-time.

theorem ESS.buCutScalar_derivatives_eq_zero_of_eqOn {S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {c : ℝ} (hS : IsOpen S) (hκ : Set.EqOn κ (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => c) S) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ S) : (∀ (j : Fin 3), CKN.spatialPartial (buCutScalar κ) j z = 0) ∧ (∀ (j k : Fin 3), CKN.spatialSecondPartial (buCutScalar κ) j k z = 0) ∧ CKN.timePartial (buCutScalar κ) z = 0

All derivatives used by the cutoff heat operator vanish on an open region where the scalar cutoff is constant.