The cutoff adapter: globally smooth fields agreeing with the zoom slices on growing squares

CIV.step_finite_contradiction (FiniteContradictionClosure.lean) asks for a sequence of meridional fields Vseq, Wseq : ℕ → ℝ × ℝ → ℝ that is ContDiff ℝ (⊤ : ℕ∞) on all of ℝ × ℝ for every n. The actual finite-axis zoom fields zoomV (lam n) h (zc n) u (·, -1), zoomW (lam n) h (zc n) u (·, -1) are smooth only on the preimage of unitCylinder under the zoom map at scale lam n, a bounded region whose size grows without bound only as lam n → 0 (no single positive scale covers an unbounded region). This file builds the repair: for each n, a smooth cutoff supported strictly inside that preimage, equal to 1 on a square that grows without bound as lam n → 0, whose product with the zoom slice is globally smooth (ContDiff ℝ (⊤ : ℕ∞) on the whole plane, for every n, not merely eventually) because the product is identically zero on a neighbourhood of every point outside the cutoff's support, regardless of how the raw slice behaves there.

The zoom centre is a sequence zc : ℕ → ℝ, one axial offset per stage, uniformly bounded by a single ζ < 1: the paper zooms about the moving pair (0, z_n), so a single fixed centre cannot be fed the selected data of CIV.exists_seq_three_terms_dichotomy, whose third output is itself a sequence of heights.

The cutoff is a plain Mathlib ContDiffBump centred at the origin of ℝ × ℝ, which carries the sup norm (Prod.norm_def) — the same norm CIV.halfPlaneRectangle's squares use — so no Euclidean/sup conversion factor is needed anywhere in this file.

The safe radius: an explicit sup-square inside the preimage of unitCylinder

theorem CIV.zoomPoint_mem_unitCylinder_of_norm_le {h zc lam r : ℝ} (hh0 : 0 ≤ h) (hzc : |zc| < 1) (hlam0 : 0 < lam) (hlam1 : lam < 1) (hr : lam ^ (1 - 2 * h) * r ≤ (1 - |zc|) / 2) {q : ℝ × ℝ} (hq : ‖q‖ ≤ r) : zoomPoint lam h zc (q, -1) ∈ unitCylinder

If a square of sup-radius r around the origin satisfies lam ^ (1 - 2h) * r ≤ (1 - |zc|) / 2, every point of that square zooms, at the frozen time τ = -1, into unitCylinder. The margin (1 - |zc|) / 2 is what is left over from the standing bound |zc| < 1 after the meridional radius and the axial offset are each kept below it; the algebra is the same splitting used in CIV.eventually_zoomPoint_mem_unitCylinder, specialised to an explicit radius instead of an asymptotic filter.

A bump-multiplied local field is globally smooth

theorem CIV.contDiff_bump_mul_of_contDiffOn_of_subset_closedBall (bump : ContDiffBump 0) {g : ℝ × ℝ → ℝ} {S : Set (ℝ × ℝ)} (hSopen : IsOpen S) (hgS : ContDiffOn ℝ (↑⊤) g S) (hsub : Metric.closedBall 0 bump.rOut ⊆ S) : ContDiff ℝ ↑⊤ fun (q : ℝ × ℝ) => ↑bump q * g q

A bump function whose closed outer ball lies inside an open set on which g is smooth gives a globally smooth product. At a point of the open set both factors are smooth there; at a point outside the bump's outer ball the product is identically zero on a neighbourhood (because the bump itself is, ContDiffBump.zero_of_le_dist), regardless of g's behaviour there — g need not even be continuous outside the open set.

The cutoff attached to a zoom scale

noncomputable def CIV.cutoffBump (h : ℝ) (zc : ℕ → ℝ) {ζ : ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ζ) (hζ : ζ < 1) (lam : ℝ) (hlam0 : 0 < lam) (n : ℕ) : ContDiffBump 0

The cutoff attached to the scale lam, stage n of the axial-offset sequence zc (uniformly bounded by ζ < 1 through hzc), and the vertical exponent h: its outer radius (1 - |zc n|) / (2 lam ^ (1 - 2h)) is exactly the radius at which zoomPoint_mem_unitCylinder_of_norm_le certifies safety, so its closed outer ball lies inside the preimage of unitCylinder; its inner radius is half of that, so it equals 1 on the sup-square of that half-radius.

Equations

• CIV.cutoffBump h zc hzc hζ lam hlam0 n = { rIn := (1 - |zc n|) / (4 * lam ^ (1 - 2 * h)), rOut := (1 - |zc n|) / (2 * lam ^ (1 - 2 * h)), rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem CIV.cutoffBump_rOut (h : ℝ) (zc : ℕ → ℝ) {ζ : ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ζ) (hζ : ζ < 1) (lam : ℝ) (hlam0 : 0 < lam) (n : ℕ) : (cutoffBump h zc hzc hζ lam hlam0 n).rOut = (1 - |zc n|) / (2 * lam ^ (1 - 2 * h))

theorem CIV.cutoffBump_rIn (h : ℝ) (zc : ℕ → ℝ) {ζ : ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ζ) (hζ : ζ < 1) (lam : ℝ) (hlam0 : 0 < lam) (n : ℕ) : (cutoffBump h zc hzc hζ lam hlam0 n).rIn = (1 - |zc n|) / (4 * lam ^ (1 - 2 * h))

theorem CIV.cutoffBump_safe {h : ℝ} (hh0 : 0 ≤ h) {zc : ℕ → ℝ} {ζ : ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ζ) (hζ : ζ < 1) {lam : ℝ} (hlam0 : 0 < lam) (hlam1 : lam < 1) (n : ℕ) : Metric.closedBall 0 (cutoffBump h zc hzc hζ lam hlam0 n).rOut ⊆ {q : ℝ × ℝ | zoomPoint lam h (zc n) (q, -1) ∈ unitCylinder}

The cutoff's outer radius is exactly the safe radius, so its closed outer ball lies inside the preimage of unitCylinder at the frozen time τ = -1, at the stage-n centre zc n.

theorem CIV.eventually_cutoffBump_rIn_gt {h : ℝ} (hh1 : h < 1 / 2) {zc : ℕ → ℝ} {ζ : ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ζ) (hζ : ζ < 1) {lam : ℕ → ℝ} (hlam0 : ∀ (n : ℕ), 0 < lam n) (hlamTendsto : Filter.Tendsto lam Filter.atTop (nhds 0)) (r : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, r < (cutoffBump h zc hzc hζ (lam n) ⋯ n).rIn

As the scale lam tends to 0 the cutoff's inner radius grows without bound, uniformly over the stage n: for every target square radius r, eventually (for lam n small) the inner radius at stage n exceeds r, so the cutoff equals 1 throughout that square (ContDiffBump.eventuallyEq_one_of_mem_ball gives it pointwise; the radius bound gives every point of the square membership in that inner ball). Only the shared bound ζ on |zc n| is used, so the bound is uniform over the whole moving sequence at once.