Overlapping geometric time slabs

The slabs overlap so that every positive time belongs to one of them.

theorem ESS.uc_geometric_time_cover (r s : ℝ) (hr : 0 < r) (hs : 0 < s) (hsr : s < r ^ 2) : ∃ (n : ℕ), 3 / 5 * (3 / 4) ^ n * r ^ 2 < s ∧ s < 2 * (3 / 5 * (3 / 4) ^ n * r ^ 2)

A geometric sequence of overlapping time slabs covers (0,r²).

theorem ESS.uc_geometric_cover_radius_le (r : ℝ) (hr : 0 < r) (n : ℕ) : r / 2 ^ (n + 1) ≤ √(2 * (3 / 5 * (3 / 4) ^ n * r ^ 2))

The half-radius spatial cover fits inside each Gaussian time-slab box.

theorem ESS.uc_geometric_slabs_cover (x : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r) (Set.Ioo 0 (r ^ 2)) ⊆ ⋃ (n : ℕ), CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r) (Set.Ioo (3 / 5 * (3 / 4) ^ n * r ^ 2) (2 * (3 / 5 * (3 / 4) ^ n * r ^ 2)))

The geometric slabs cover the full local positive-time cylinder.