Geometry of the physical Gaussian cylinder

The affine image of a normalized averaging box is the physical Gaussian averaging cylinder at half the elapsed time.

theorem ESS.bu_short_physical_average_radius (scale δ : ℝ) (hscale : 0 < scale) : have t := scale ^ 2 * δ / 2; √(3 * t) = scale * √(3 * δ / 2)

The physical Gaussian radius is the scaled normalized averaging radius (lem:bu-small-time).