Geometry of a high-strip dyadic cell

A shifted cell meeting the high normal strip has an averaging center above the boundary and has time below the Gaussian threshold.

theorem ESS.bu_short_high_cell_geometry (scale : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (k : ℤ) (hk : 1 ≤ k) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale) : have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2; 2 < (scale • Y) 2 ∧ δ < 1 / 2 ∧ CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2) ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ∧ CKN.Foundation.Parabolic.vec3Ball Y (2 * (√δ / 8)) ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}

A high-strip cell has an averaging ball contained in the positive half-space, and its midpoint lies at normal height above two (lem:bu-small-time).