The local weighted logarithm in R-324 Step 3

After the sharp binary inverse-square convolution, the local part of the inserted Proposition 4.1 majorant is an inverse-square kernel restricted to an ε-scale ball and multiplied by the critical logarithmic weight. This file proves the exact support-indicator identity and its uniform ε² |log ε| integral bound.

The support radius is fixed before the constant is selected. Accordingly, the resulting constant may depend on supportConstant, but is uniform in the mollification scale and the translated logarithmic singularity.

theorem Anderson4D.integral_invSq_support_mul_criticalLogWeight_eq_setIntegral (supportConstant ε : ℝ) (x : T4) : ∫ (z : T4), invSqKer z * primitiveSupportIndicator supportConstant ε z * criticalLogWeight (x - z) ∂paperMeasure = ∫ (z : T4) in {z : T4 | torusDistSq z ≤ (supportConstant * ε) ^ 2}, invSqKer z * criticalLogWeight (x - z) ∂paperMeasure

Exact support-indicator integral identity for the local weighted logarithmic kernel.

theorem Anderson4D.integrable_invSq_support_mul_criticalLogWeight {supportConstant ε : ℝ} (hsupport : 0 < supportConstant) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (x : T4) : MeasureTheory.Integrable (fun (z : T4) => invSqKer z * primitiveSupportIndicator supportConstant ε z * criticalLogWeight (x - z)) paperMeasure

Genuine Bochner integrability of the locally supported weighted logarithmic kernel. The proof uses the same honest near/far split as the quantitative estimate below, rather than the totalized value of an otherwise non-integrable integral.

theorem Anderson4D.exists_integral_invSq_support_mul_criticalLogWeight_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ε : ℝ) (x : T4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∫ (z : T4), invSqKer z * primitiveSupportIndicator supportConstant ε z * criticalLogWeight (x - z) ∂paperMeasure ≤ K * ε ^ 2 * |Real.log ε|

The scale-local inverse-square kernel averages the critical binary logarithm with the sharp ε² |log ε| mass. This is the local half of the proper inserted convolution in R-324 Step 3.