The regularized weighted logarithm in R-324 Step 3

The second term of the inserted Proposition 4.1 majorant is the regularized critical square

(torusDistSq z + ε²)⁻².

After one sharp binary inverse-square convolution, it must be averaged against the moving critical logarithm 1 + |log ‖x - z‖|. This file proves both the genuine integrability of that product and its uniform O(|log ε|²) integral bound.

The proof separates a ball about the moving logarithmic singularity. When x is at the regularization scale, the regularized square is bounded by ε⁻⁴. When x is farther away, the moving ball stays away from the origin and the regularized square is bounded by the square of the inverse-square kernel. Off the moving ball, the logarithmic weight has only one fixed-scale logarithmic loss. The remaining mass estimate is integral_regularizedInvSquare_le, whose proof is precisely the momentInnerBall/outer-annulus decomposition.

Integrability certificates

theorem Anderson4D.integrable_regularizedInvSquare_mul_criticalLogWeight (ε : ℝ) (x : T4) (hε : 0 < ε) : MeasureTheory.Integrable (fun (z : T4) => regularizedInvSquare ε z * criticalLogWeight (x - z)) paperMeasure

The regularized square times the translated critical logarithm is a genuine integrable function. No small-scale upper bound is needed: positivity of ε gives the global domination by ε⁻⁴ * criticalLogWeight.

Pointwise control away from the regularized origin

Uniform |log ε|² estimate

theorem Anderson4D.exists_integral_regularizedInvSquare_mul_criticalLogWeight_le : ∃ (K : ℝ), 0 < K ∧ ∀ (ε : ℝ) (x : T4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∫ (z : T4), regularizedInvSquare ε z * criticalLogWeight (x - z) ∂paperMeasure ≤ K * |Real.log ε| ^ 2

The regularized critical square averages the moving binary logarithm with at most two logarithmic losses, uniformly in the translation x.