The swirl-term pairing bound with a general lower bound on the radius

The fixed-scale swirl-source pairing bound of CIV.Zoom.RecedingSwirlPairingBound, with the offset A + R bounded below by an arbitrary ε > 0 rather than by 1; the source S_n²/(A+R) is then bounded by CΓ² / ε³ through the circulation bound eq:aniso:zoom:circulation.

theorem CIV.swirl_term_pairing_bound_fixed_of_le {h lam rc zc CΓ : ℝ} (hCΓ : 0 ≤ CΓ) (hlam : 0 < lam) (hdelta : lam ^ (2 * h) ≤ 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} (hK : IsCompact K) {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) (hΓ : ∀ y ∈ K, |circulation u (zoomPointRec lam h rc zc (y, τ))| ≤ CΓ) {ε : ℝ} (hε : 0 < ε) (hApos : ∀ y ∈ K, ε ≤ rc / lam + y.1) (ψ : ℝ × ℝ → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) (B : ℝ) : 0 ≤ B → ∀ (hψB : ∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B), |∫ (y : ℝ × ℝ), 1 / (rc / lam + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) (y, τ) * ψ y| ≤ CΓ ^ 2 / ε ^ 3 * (MeasureTheory.volume K).toReal * B

The swirl-source pairing bound at a fixed zoom scale: the integral of the divergence-form swirl term (1/(A+R)) ∂_Z(S_n²) of zoomTheta_pde against a test function supported in the interior of a compact set K is bounded by CΓ² times the bound B on ψ and its first two derivatives, times the volume of K.