Distances inside a shifted dyadic cell

Time translation preserves the spatial distance from a cell's midpoint and shifts its time distance by one half.

theorem ESS.bu_short_shifted_cell_spatial_distance_le (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ buShortShiftedDyadicCell k m ell) : CKN.Foundation.Parabolic.vec3EuclideanNorm (z.1 - (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1) ≤ √3 * CKN.Foundation.buSmallTimeDyadicSide k

The spatial distance from a shifted cell point to its midpoint is bounded by the cell side length (lem:bu-small-time).

theorem ESS.bu_short_shifted_cell_coordinate_close (k : ℤ) (hk : 0 ≤ k) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ buShortShiftedDyadicCell k m ell) (i : Fin 3) : |z.1 i - (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 i| ≤ 1 / 64

Each coordinate of a shifted cell point is within one sixty-fourth of its spatial midpoint at nonnegative dyadic levels.

theorem ESS.bu_short_shifted_cell_normal_square_le (k : ℤ) (hk : 0 ≤ k) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ buShortShiftedDyadicCell k m ell) : z.1 2 ^ 2 ≤ 2 * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 2 ^ 2 + 1

The normal square at a cell point is controlled by twice the normal square at its midpoint.