Location of the short-time cutoff error

The scalar heat error vanishes below the normal transition and on the interior plateau. Thus every nonzero error is in the phase transition, the spatial shell, or the lower-time transition.

theorem ESS.buShortFullCutoff_eq_zero_below_normal (scale R ε : ℝ) (hR : 0 < R) : Set.EqOn (buShortFullCutoff scale R hR ε) (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0) {q : CKN.Foundation.Parabolic.Vec3 × ℝ | q.1 2 < buShortYMinus scale}

The full cutoff vanishes on the open region below its normal transition height.

theorem ESS.buShortFullCutoff_derivatives_zero_below_normal (scale R ε : ℝ) (hR : 0 < R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.1 2 < buShortYMinus scale) : (∀ (j : Fin 3), CKN.spatialPartial (buCutScalar (buShortFullCutoff scale R hR ε)) j z = 0) ∧ (∀ (j k : Fin 3), CKN.spatialSecondPartial (buCutScalar (buShortFullCutoff scale R hR ε)) j k z = 0) ∧ CKN.timePartial (buCutScalar (buShortFullCutoff scale R hR ε)) z = 0

Every derivative entering the scalar heat error vanishes below the normal transition height.

theorem ESS.buShortCutoffHeatErrorSize_eq_zero_below_normal (scale R ε c₁ : ℝ) (hR : 0 < R) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.1 2 < buShortYMinus scale) : buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z = 0

The scalar cutoff error is zero below the normal transition.

theorem ESS.buShortCutoffHeatErrorSize_eq_zero_on_core (scale R ε c₁ : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortCoreRegion scale R ε) : buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z = 0

The scalar cutoff error is zero on its open plateau.

theorem ESS.buShortCutoffHeatErrorSize_location (scale R ε c₁ : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z ≠ 0) (hs : 1 / 2 < z.2) (hs1 : z.2 < 1) : buShortYMinus scale ≤ z.1 2 ∧ (z.1 ∉ CKN.Foundation.Parabolic.vec3Ball 0 R ∨ z.2 ≤ 1 / 2 + 2 * ε ∨ buShortFExt (z.1 2) z.2 - buShortB scale ≤ -buShortD scale / 2)

A nonzero scalar heat error lies in the normal transition or in one of the three other cutoff transition regions.