One-sided cylinder covering

The truncated time shift of Step 2 in the proof of thm:A. For a cylinder 𝒞_ϱ(w) meeting the one-sided cylinder of admissible centres, and a point w' of the intersection, the new centre is w'' = (x_{w'}, min {t_w + ϱ², 0}): the spatial centre of w' and the forward time shift truncated at the top face. It stays among the admissible centres, and 𝒞_ϱ(w) ∩ {t ≤ 0} ⊆ 𝒞_{2ϱ}(w''). The covering itself needs no upper bound on the radius.

def CKN.Core.Endgame.truncatedCylinderCenter (w w' : Foundation.Parabolic.ParabolicPoint) (ρ T : ℝ) : Foundation.Parabolic.ParabolicPoint

Shift the time coordinate forward by the squared radius, stopping at the prescribed upper time, and use the selected point as spatial center.

Equations

• CKN.Core.Endgame.truncatedCylinderCenter w w' ρ T = (w'.1, min (w.2 + ρ ^ 2) T)

theorem CKN.Core.Endgame.truncatedCylinderCenter_mem {w w' : Foundation.Parabolic.ParabolicPoint} {x : Foundation.Parabolic.Vec3} {T R ρ : ℝ} (hw : w' ∈ Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ) (hinner : w' ∈ Foundation.Parabolic.parabolicCylinder x T R) : truncatedCylinderCenter w w' ρ T ∈ Foundation.Parabolic.parabolicCylinder x T R

The truncated center stays in any cylinder of upper time T that contains the selected intersection point.

theorem CKN.Core.Endgame.parabolicCylinder_inter_le_subset_truncated {w w' : Foundation.Parabolic.ParabolicPoint} {ρ T : ℝ} (hw : w' ∈ Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ) : Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ ∩ {z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ T} ⊆ Foundation.Parabolic.parabolicCylinder (truncatedCylinderCenter w w' ρ T).1 (truncatedCylinderCenter w w' ρ T).2 (2 * ρ)

The portion below time T is covered by a cylinder of twice the radius whose spatial center is any point of the original cylinder.

theorem CKN.Core.Endgame.parabolicCylinder_subset_three_quarters {a : ℝ} (ha : 0 < a) (ha34 : a < 3 / 4) : Foundation.Parabolic.parabolicCylinder 0 0 a ⊆ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4)

A positive smaller concentric cylinder lies among the admissible centers.

theorem CKN.Core.Endgame.exists_one_sided_covering_cylinder_on_cylinder {a : ℝ} (ha : 0 < a) (ha34 : a < 3 / 4) {w : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hmeet : (Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ ∩ Foundation.Parabolic.parabolicCylinder 0 0 a).Nonempty) : ∃ w' ∈ Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ ∩ Foundation.Parabolic.parabolicCylinder 0 0 a, truncatedCylinderCenter w w' ρ 0 ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4) ∧ Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ ∩ {z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0} ⊆ Foundation.Parabolic.parabolicCylinder (truncatedCylinderCenter w w' ρ 0).1 (truncatedCylinderCenter w w' ρ 0).2 (2 * ρ)

Any cylinder meeting a smaller one-sided cylinder has a truncated admissible center covering its entire portion below time zero.