Upper time support of the short-time cutoff

On each bounded spatial ball the normal phase tends uniformly to zero as time approaches one. The shifted-phase cutoff therefore turns off before the upper time face of lem:bu-small-time.

theorem ESS.buShortF_continuousAt_one (y : ℝ) : ContinuousAt (fun (s : ℝ) => buShortF y s) 1 ∧ buShortF y 1 = 0

At every fixed height, the normal phase is continuous at time one and equals zero there.

theorem ESS.buShortF_small_near_one (scale R : ℝ) (hscale : 0 < scale) : ∃ (σ : ℝ), 1 / 2 < σ ∧ σ < 1 ∧ ∀ (y s : ℝ), 0 ≤ y → y ≤ 2 * R → σ ≤ s → s < 1 → buShortF y s < buShortB scale / 4

On any bounded normal height range, the phase becomes smaller than a fixed positive threshold before the upper time face.

theorem ESS.buShortEtaExt_zero_near_one {scale R : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) : ∃ (σ : ℝ), 1 / 2 < σ ∧ σ < 1 ∧ ∀ y ∈ CKN.Foundation.Parabolic.vec3Ball 0 (2 * R), ∀ (s : ℝ), σ ≤ s → s < 1 → buShortEtaExt scale (y, s) = 0

The phase cutoff vanishes on a bounded spatial ball at times above a fixed level below one.

theorem ESS.buShortF_nonpos_after_one {y s : ℝ} (hy : 0 ≤ y) (hs : 1 ≤ s) : buShortF y s ≤ 0

The normal phase is nonpositive at all times from one onward.

theorem ESS.buShortEtaExt_zero_after_one {scale : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) (y : CKN.Foundation.Parabolic.Vec3) {s : ℝ} (hs : 1 ≤ s) : buShortEtaExt scale (y, s) = 0

The shifted-phase cutoff vanishes at and after the upper time face.