A scale-local inverse-square approximate identity

The non-Taylor regions (4.11) and (4.12) leave, at the primitive scale, the truncated kernel

ε⁻² 1_{d(z) ≤ (S ε)²} invSqKer z.

Its mass is uniformly bounded, but that fact alone does not control the second singularity when the external point is also at scale ε. The proof below separates a ball around that moving singularity and keeps the local O(‖x‖²) mass before applying the normalization.

theorem Anderson4D.sq_norm_mul_invSqKer_le_one_r322 (z : T4) : ‖z‖ ^ 2 * invSqKer z ≤ 1

theorem Anderson4D.exists_r322ScaleBall_invSq_convolution_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ε : ℝ) (x : T4), 0 < ε → x ≠ 0 → ε⁻¹ ^ 2 * ∫ (z : T4) in r322ScaleBall supportConstant ε, invSqKer (x - z) * invSqKer z ∂paperMeasure ≤ K * invSqKer x

The scale-truncated inverse-square kernel, normalized by ε⁻², preserves the inverse-square external profile.