Squared phase and shell error bound

The scalar heat error square is separated into a phase-gap density, a spatial shell density, and the lower-time transition density.

theorem ESS.bu_short_two_term_square {e a b x y : ℝ} (he0 : 0 ≤ e) (hbound : e ≤ a * (x + y) + b) : e ^ 2 ≤ 4 * a ^ 2 * (x ^ 2 + y ^ 2) + 2 * b ^ 2

A two-term scalar majorant gives a quadratic error bound with separate square densities.