Balls reaching the positive normal phase

At each time before one, the positive normal-phase region reaches arbitrarily high above the boundary. A ball centered there can contain any prescribed interior point while remaining in the half-space.

theorem ESS.bu_short_phase_positive_at_high_center {scale s y₃ : ℝ} (hs : 1 / 2 < s) (hs1 : s < 1) : ∃ (H : ℝ), y₃ < H ∧ 1 < H ∧ buShortB scale < buShortF H s

The normal phase eventually exceeds its fixed threshold at every time strictly between one half and one.

theorem ESS.bu_short_positive_phase_ball {scale s : ℝ} (hs : 1 / 2 < s) (hs1 : s < 1) (y : CKN.Foundation.Parabolic.Vec3) (hy : 0 < y 2) : ∃ (c : CKN.Foundation.Parabolic.Vec3) (R : ℝ), 0 < R ∧ y ∈ CKN.Foundation.Parabolic.vec3Ball c R ∧ CKN.Foundation.Parabolic.vec3Ball c R ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ∧ buShortB scale < buShortF (c 2) s

A high center with positive normal phase admits a half-space ball containing an arbitrary target point.