step_finite_contradiction at the cutoff-multiplied zoom fields #
The final assembly: hVbdd/hWbdd on every halfPlaneRectangle j (value, first- and
second-derivative operator norm, by one shared constant L = 4C), together with hVsmooth,
hWsmooth, haxis, hdivn, hdWn from the earlier files, discharge every hypothesis of
CIV.step_finite_contradiction_of_dr_dz except the selection data Rsel, c₀, hlower (a
different step) and Ω_n → 0 (the endpoint vanishing of the comparison argument,
CIV/Zoom/ZoomLimitEndpoint.lean), which are taken as hypotheses.
The zoom centre zc : ℕ → ℝ moves with n, uniformly bounded by ζ < 1 (hzc, hζ): the
paper zooms about a moving axial offset z_n, and the finite-axis selection
CIV.exists_seq_three_terms_dichotomy this adapter is eventually fed returns exactly such a
moving height sequence, not a single fixed real number.
Every point of a rectangle enters unitCylinder under the zoom map, eventually #
The second derivative on a rectangle reads off the raw slice's, eventually #
hVbdd, hWbdd on halfPlaneRectangle j, eventually, with the shared constant 4C #
The instantiation: step_finite_contradiction at the cutoff-multiplied zoom fields #
step_finite_contradiction, instantiated at the cutoff-multiplied zoom fields
Vseq n := cutoffZoomV h zc hzc hζ u lam hlam0 n,
Wseq n := cutoffZoomW h zc hzc hζ u lam hlam0 n, with the shared bound L := 4C. Every
hypothesis is discharged from the standing classical-solution, anisotropic-bound and
axisymmetry data except the selection data Rsel, c₀, hlower — the conclusion of the
meridional-smallness dichotomy — and Ω_n → 0, the endpoint vanishing of the
comparison argument; both are taken here as hypotheses. The
zoom centre zc n moves with n, so hΩ0 and hlower are stated at the same moving centre,
matching a selection whose axial heights are themselves a sequence.
The payoff: hlower is supplied, eventually, by the real raw selection bound #
false_of_finiteZoomCutoff_selection's hlower in ∀ᶠ n form, produced from the raw-field
selection bound at real data: once n is large enough that the cutoff equals 1 throughout the
fixed square containing [0, A] × {0}
(CIV.eventually_forall_mem_halfPlaneRectangle_cutoffZoomV_eq,
..._cutoffZoomW_eq), the cutoff-multiplied fields and their derivatives at (Rsel n, 0)
coincide with the raw zoom slices there, at the same moving centre zc n, whose dr/dz
values are exactly what CIV.lt_of_neg_t_mul_meridionalQuantity_selection_lt bounds below by
c₀. So the ∀ n raw-field selection bound — the real selected sequence, moving centre
included, not a substitute — supplies the weaker ∀ᶠ n hypothesis that
CIV.step_finite_contradiction now needs, where it could not supply the former ∀ n
cutoff-field requirement at every finite n.
step_finite_contradiction closes end to end at real data: given the raw-field selection
bound hlowerRaw — exactly the conclusion of CIV.lt_of_neg_t_mul_meridionalQuantity_selection_lt
at the selected sequence, moving centre included, and nothing manufactured — the cutoff adapter
now supplies every hypothesis of CIV.step_finite_contradiction, hlower included via
CIV.eventually_cutoffZoom_hlower_of_raw_selection. Only the endpoint vanishing
of the comparison argument (hΩ0) and the meridional-smallness dichotomy that produces
hlowerRaw itself remain external.