The receding-axis case of prop:aniso:small fails

Closing argument of Step 3 of the zoom-in of Section sec:aniso:zoom (eq:aniso:zoom:receding:endpoint and eq:aniso:zoom:receding:quotient). In the recentred variables eq:aniso:zoom:receding:variables the selected point is the origin of ℝ × ℝ, the axis sits at R = -A_n with A_n → ∞, and the meridional fields live on the whole plane.

The bounds eq:aniso:zoom:derivatives make V_n(·,-1) and W_n(·,-1) bounded in C² on every centred square with one constant, so along a subsequence they converge in C¹ on those squares (CIV.exists_subseq_tendstoUniformlyOn_c1_plane). The limiting divergence identity is the quotient-free ∂_R V⁰ + ∂_Z W⁰ = 0 of eq:aniso:zoom:receding:div, the term V_n/(A_n+R) vanishing pointwise because A_n → ∞ while V_n stays bounded; together with ∂_R W⁰ = 0, which comes from Θ_n(·,-1) → 0, this is exactly the input of CIV.endpoint_vanishing_rec, the whole-plane bounded-affine argument. The final step is CIV.false_of_receding_contradiction_data, whose limit and convergence hypotheses are supplied here by the extraction rather than assumed.

Everything here happens at the single time τ = -1: the compactness used is the spatial C¹ compactness of a fixed time slice, and no equicontinuity in τ is claimed or needed. The two inputs that carry information from the equation — the recentred divergence identity of eq:aniso:zoom:receding:div and the vanishing of ∂_R W_n, which comes from Θ_n → 0 — enter as hypotheses on the sequence itself.

The C² bounds are asked for all large n on each square, since the preimage of the unit cylinder contains a given compact set only once the scale is small enough; the sequence is therefore re-indexed past the threshold of the square of index 0 before the pointwise bound |V_n(0,0)| ≤ L that eq:aniso:zoom:receding:quotient needs is read off.

The endpoint data extracted from the C² bounds

theorem CIV.exists_subseq_receding_endpoint_data {L : ℝ} (hL : 0 ≤ L) (Anseq : ℕ → ℝ) (Vseq Wseq : ℕ → ℝ × ℝ → ℝ) (hVsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hWsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Wseq n)) (hVbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ planeRectangle j, |Vseq n y| ≤ L ∧ ‖fderiv ℝ (Vseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L) (hWbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ planeRectangle j, |Wseq n y| ≤ L ∧ ‖fderiv ℝ (Wseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Wseq n)) y‖ ≤ L) (hdivn : ∀ (p : ℝ × ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, (fderiv ℝ (Vseq n) p) (1, 0) + Vseq n p / (Anseq n + p.1) + (fderiv ℝ (Wseq n) p) (0, 1) = 0) (hquot : ∀ (p : ℝ × ℝ), Filter.Tendsto (fun (n : ℕ) => Vseq n p / (Anseq n + p.1)) Filter.atTop (nhds 0)) (hdWn : ∀ (p : ℝ × ℝ), Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (Wseq n) p) (1, 0)) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (V : ℝ × ℝ → ℝ) (W : ℝ × ℝ → ℝ) (DV : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ), (∀ (p : ℝ × ℝ), HasFDerivAt V (DV p) p) ∧ (∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) ∧ (∀ (p : ℝ × ℝ), |V p| ≤ L) ∧ (∀ (p : ℝ × ℝ), (DV p) (1, 0) + (DW p) (0, 1) = 0) ∧ (∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) ∧ (∀ (j : ℕ), TendstoUniformlyOn (fun (n : ℕ) => fderiv ℝ (Vseq (φ n))) DV Filter.atTop (planeRectangle j)) ∧ ∀ (j : ℕ), TendstoUniformlyOn (fun (n : ℕ) => fderiv ℝ (Wseq (φ n))) DW Filter.atTop (planeRectangle j)

The endpoint data of eq:aniso:zoom:receding:endpoint, extracted rather than assumed: a sequence of smooth meridional fields (V_n, W_n) on the plane which is C²-bounded by one constant L on every centred square for all large n, satisfies the recentred divergence identity of eq:aniso:zoom:receding:div for all large n, whose radial quotient V_n/(A_n+R) tends to zero, and whose radial derivative ∂_R W_n tends to zero, has a subsequence along which the gradients converge uniformly on every centred square to gradients of a pair (V⁰, W⁰) that is bounded by L, divergence free with no quotient term, and independent of R in its axial component.

The seven conclusions are the seven hypotheses hV, hW, hbdd, hdiv, hWr, hDVconv, hDWconv of CIV.false_of_receding_contradiction_data, with M = L.

The contradiction

theorem CIV.step_receding_contradiction {c₀ L : ℝ} (hc₀ : 0 < c₀) (hL : 0 ≤ L) {Anseq : ℕ → ℝ} (hAtop : Filter.Tendsto Anseq Filter.atTop Filter.atTop) (hApos : ∀ (n : ℕ), 0 < Anseq n) (Vseq Wseq : ℕ → ℝ × ℝ → ℝ) (hVsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Vseq n)) (hWsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (Wseq n)) (hVbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ planeRectangle j, |Vseq n y| ≤ L ∧ ‖fderiv ℝ (Vseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Vseq n)) y‖ ≤ L) (hWbdd : ∀ (j : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ planeRectangle j, |Wseq n y| ≤ L ∧ ‖fderiv ℝ (Wseq n) y‖ ≤ L ∧ ‖fderiv ℝ (fderiv ℝ (Wseq n)) y‖ ≤ L) (hdivn : ∀ (p : ℝ × ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, (fderiv ℝ (Vseq n) p) (1, 0) + Vseq n p / (Anseq n + p.1) + (fderiv ℝ (Wseq n) p) (0, 1) = 0) (hquot : ∀ (p : ℝ × ℝ), Filter.Tendsto (fun (n : ℕ) => Vseq n p / (Anseq n + p.1)) Filter.atTop (nhds 0)) (hdWn : ∀ (p : ℝ × ℝ), Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (Wseq n) p) (1, 0)) Filter.atTop (nhds 0)) (hlower : ∀ (n : ℕ), c₀ ≤ |(fderiv ℝ (Vseq n) (0, 0)) (1, 0)| + |Vseq n (0, 0)| / Anseq n + |(fderiv ℝ (Wseq n) (0, 0)) (0, 1)|) : False

Step 3 of prop:aniso:small closes: a sequence of meridional fields (V_n, W_n) in the recentred variables, with the endpoint data of CIV.exists_subseq_receding_endpoint_data and receding offsets A_n → ∞, cannot satisfy the selection bound eq:aniso:zoom:selected at the origin. The extraction supplies exactly the convergence and limit hypotheses of CIV.false_of_receding_contradiction_data, which then produces the contradiction.