The finite-axis contradiction at the selected points

The last paragraph of Step 2 of the proof of prop:aniso:small: in the finite-axis case (r_n / λ_n ≤ A), the points selected in eq:aniso:zoom:selected have zoomed coordinates (r_n / λ_n, 0, -1) about the moving axis point (0, z_n), and the endpoint vanishing of the rescaled potential vorticity (eq:aniso:zoom:finite:endpoint, through CIV.false_of_finiteZoomCutoff_raw_selection) contradicts the lower bound c₀. The selected data are exactly those returned by the finite-axis branch of CIV.exists_seq_three_terms_dichotomy, with λ_n = √(-t_n).

theorem CIV.false_of_real_finite_selection {C h ρ : ℝ} (hC : 0 ≤ C) (hh0 : 0 < h) (hh1 : h < 1 / 2) (hρ : ρ < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hb : AnisotropicBounds C h u) {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {c₀ : ℝ} (hc₀ : 0 < c₀) {t x₁ x₃ : ℕ → ℝ} (hx₁ : ∀ (n : ℕ), 0 ≤ x₁ n) (htlim : Filter.Tendsto t Filter.atTop (nhds 0)) (hmem : ∀ (n : ℕ), meridional (x₁ n) (x₃ n) ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (htmem : ∀ (n : ℕ), t n ∈ Set.Ioo (-1) 0) (hineq : ∀ (n : ℕ), c₀ < -t n * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (x₁ n) (x₃ n), t n)| + |radialQuotient u (meridional (x₁ n) (x₃ n), t n)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 (meridional (x₁ n) (x₃ n), t n)|)) {A : ℝ} (hA : ∀ (n : ℕ), x₁ n / √(-t n) ≤ A) (hΩ0 : ∀ (q : ℝ × ℝ), 0 < q.1 → Filter.Tendsto (fun (n : ℕ) => zoomOmega (√(-t n)) h (x₃ n) u (q, -1)) Filter.atTop (nhds 0)) : False

The finite-axis branch of the selection of eq:aniso:zoom:selected is contradictory once the rescaled potential vorticity about the moving axis points (0, x₃ n), at scale λ_n = √(-t_n), tends to zero at every point of {τ = -1} off the axis.