Margin-safe parabolic cylinders and their closures

This file records the elementary geometry behind the "doubling with a margin" step: a parabolic cylinder that meets the carrier region and whose radius is at most one third of the margin separating the carrier from the outer ball has its doubled-radius cylinder, and hence the closure of that cylinder, contained in the outer region. This is what lets a slice estimate proved at a single cell radius be applied at twice that radius, at the price of a third of the gap between the inner and outer regions.

The results are stated in the two settings used later: a one-sided cylinder based at the origin of the unit parabolic cylinder, and a parabolic metric ball about an arbitrary centre.

theorem CKN.Core.Step4.vec3EuclideanNorm_lt_of_vec3Ball_inter_nonempty {x c : Foundation.Parabolic.Vec3} {r a : ℝ} (h : (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball c a).Nonempty) : Foundation.Parabolic.vec3EuclideanNorm (x - c) < a + r

Two Euclidean balls that meet are closer than the sum of their radii: if some point lies within radius r of x and within radius a of c, then the centres themselves are less than a + r apart. This is the quantitative form of the separation between a cell that meets the carrier and the outer ball.

theorem CKN.Core.Step4.parabolicCylinder_double_subset_unit_of_margin {R₀ R₁ r t : ℝ} {x : Foundation.Parabolic.Vec3} (hR₀ : R₀ ≤ 1) (hmargin : 3 * r ≤ R₀ - R₁) (hx : Foundation.Parabolic.vec3EuclideanNorm (x - 0) < R₁ + r) (htop : t ≤ 0) (hbot : -1 ≤ t - (2 * r) ^ 2) : Foundation.Parabolic.parabolicCylinder x t (2 * r) ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1

A parabolic cylinder that meets the carrier at a radius at most a third of the margin between the carrier and the outer ball has its DOUBLED cylinder inside the outer region. Concretely, if x is within R₁ + r of the origin, 3 * r ≤ R₀ - R₁ and R₀ ≤ 1, then every point of parabolicCylinder x t (2 * r) lies in the unit cylinder parabolicCylinder 0 0 1, provided the base time t lies below zero and the doubled time-depth stays at or above the unit depth. The factor three is the margin that absorbs the doubling of the radius.

theorem CKN.Core.Step4.closure_parabolicCylinder_double_subset_spaceTimeSet_of_origin_margin {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {R₀ R₁ r t : ℝ} {x : Foundation.Parabolic.Vec3} (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR₀ : R₀ ≤ 1) (hmargin : 3 * r ≤ R₀ - R₁) (hx : Foundation.Parabolic.vec3EuclideanNorm (x - 0) < R₁ + r) (htop : t ≤ 0) (hbot : -1 ≤ t - (2 * r) ^ 2) : closure (Foundation.Parabolic.parabolicCylinder x t (2 * r)) ⊆ spaceTimeSet Ω I

The closure form of the margin-safe doubling: if the closure of the unit parabolic cylinder lies in the space-time carrier Ω × I, then so does the closure of every doubled cylinder whose radius is at most a third of the margin and whose base point lies within R₁ + r of the origin, with the same time-side bounds. The closure is taken because the slice estimate is applied on closed one-sided cylinders.

theorem CKN.Core.Step4.closure_parabolicCylinder_double_subset_metricBall_of_margin {z₀ : Foundation.Parabolic.ParabolicPoint} {R r t : ℝ} {x : Foundation.Parabolic.Vec3} (hR : 0 < R) (hr : 0 < r) (hmargin : 3 * r ≤ R) (hx : Foundation.Parabolic.vec3EuclideanNorm (x - z₀.1) < R / 2 + r) (hlow : z₀.2 - R ^ 2 / 4 - r ^ 2 < t) (hhigh : t < z₀.2 + R ^ 2 / 4 + r ^ 2) : closure (Foundation.Parabolic.parabolicCylinder x t (2 * r)) ⊆ Metric.ball z₀ (2 * R)

The margin-safe doubling for a parabolic metric ball: a closed doubled cylinder whose radius is at most a third of R, and whose base point is within R/2 + r of the centre and whose base time lies in the one-sided window around the centre time, is contained in the parabolic ball of radius 2 * R. This is the version applied when the outer region is a parabolic ball rather than the unit cylinder.

theorem CKN.Core.Step4.vec3Ball_subset_outer_of_margin {R₀ R₁ r : ℝ} {x : Foundation.Parabolic.Vec3} (hr : 0 ≤ r) (hmargin : 3 * r ≤ R₀ - R₁) (hx : Foundation.Parabolic.vec3EuclideanNorm (x - 0) < R₁ + r) : Foundation.Parabolic.vec3Ball x r ⊆ Foundation.Parabolic.vec3Ball 0 R₀

A margin-safe cell that meets the carrier ball has its own ball, and hence a fortiori the region where its slice estimate is read, inside the outer ball.

theorem CKN.Core.Step4.symmetric_margin_premises_of_meet {z₀ : Foundation.Parabolic.ParabolicPoint} {R r t : ℝ} {x : Foundation.Parabolic.Vec3} (hr : 0 < r) (hmeet : (Foundation.Parabolic.parabolicCylinder x t r ∩ Metric.ball z₀ (R / 2)).Nonempty) : Foundation.Parabolic.vec3EuclideanNorm (x - z₀.1) < R / 2 + r ∧ z₀.2 - R ^ 2 / 4 - r ^ 2 < t ∧ t < z₀.2 + R ^ 2 / 4 + r ^ 2

The three margin premises of the doubling step for a parabolic metric ball, read off a cell that meets the inner ball: the spatial centres are close, and the cell's top time lies in the one-sided window around the centre time.