The two bridges to the selected sequence

theorem CIV.eventually_zoomPoint_mem_unitCylinder {h zc ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hzc : |zc| < ρ) (hρ : ρ < 1) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) (hKt : ∀ p ∈ K, p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, zoomPoint lam h zc p ∈ unitCylinder

theorem CIV.eventually_zoomPoint_mem_ball {h zc ρ Rstar : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hzc : |zc| < ρ) (hρ : ρ < Rstar) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, (zoomPoint lam h zc p).1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar

theorem CIV.eventually_zoomPoint_time_mem {h zc tstar : ℝ} (htstar : tstar < 0) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) (hKt : ∀ p ∈ K, p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, (zoomPoint lam h zc p).2 ∈ Set.Ioo tstar 0

theorem CIV.eventually_zoomPoint_mem_ball_and_time {h zc ρ Rstar tstar : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hzc : |zc| < ρ) (hρ : ρ < Rstar) (htstar : tstar < 0) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) (hKt : ∀ p ∈ K, p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, (zoomPoint lam h zc p).1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar ∧ (zoomPoint lam h zc p).2 ∈ Set.Ioo tstar 0

The ball and time clauses of the preimage statement, taken together: for a compact set of rescaled points with negative times, the zoom point of every one of them eventually lies in B(R_*) × (t_*, 0), which is the set on which the circulation bound eq:aniso:zoom:circulation holds.

theorem CIV.tendsto_radialLength_nhdsGT : Filter.Tendsto radialLength (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))

The radial length eq:aniso:lengths is strictly positive at negative times, so it tends to 0 through positive values. This is the refinement of tendsto_radialLength that the preimage statements need, since they are stated along 𝓝[>] 0.

theorem CIV.tendsto_atTop_nhdsLT {t : ℕ → ℝ} (hneg : ∀ (n : ℕ), t n < 0) (htend : Filter.Tendsto t Filter.atTop (nhds 0)) : Filter.Tendsto t Filter.atTop (nhdsWithin 0 (Set.Iio 0))

A sequence of negative times converging to the singular time converges within the negative reals, which is the filter tendsto_radialLength_nhdsGT starts from.

theorem CIV.eventually_atTop_radialLength {P : ℝ → Prop} {t : ℕ → ℝ} (hneg : ∀ (n : ℕ), t n < 0) (htend : Filter.Tendsto t Filter.atTop (nhds 0)) (hP : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), P lam) : ∀ᶠ (n : ℕ) in Filter.atTop, P (radialLength (t n))

The passage from the filter 𝓝[>] 0 to the selected sequence: whatever holds eventually in the zoom scale holds for all large n at the scales λ_n = ℓ_r(t_n) attached to a sequence of negative times increasing to the singular time, as selected after eq:aniso:zoom:selected. Applied to eventually_zoomPoint_mem_unitCylinder, eventually_zoomPoint_mem_ball, eventually_zoomPoint_time_mem or their conjunction, this is the statement that the preimage of Q contains a given compact set for all large n.