BUAssembly

Assembly of the half-space backward uniqueness argument.

theorem ESS.bu_iteration_time_coverage {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) {t : ℝ} (ht : t < 1) : ∃ (k : ℕ), t < 1 - (1 - γ) ^ k

The geometric time sequence in lem:bu-iterate eventually passes every time strictly below one.

theorem ESS.bu_backwardUniqueness_from_halfSpaceConclusion {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hzero : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → ∀ (t : ℝ), 0 < t → t < 1 → w (x, t) = 0) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) → w z = 0

A pointwise half-space conclusion on Q⁺ implies the corresponding space-time carrier statement (thm:bu).