Integral bounds for the primitive-kernel majorant

This file records the analytic bridge from the pointwise primitive estimate (4.3) to the ε⁻² |log ε|⁻¹ scale used in the deterministic renormalization estimate (3.22). Both summands are integrated from proved continuum estimates:

• the local |z|⁻² term uses the four-dimensional ball bound;
• the regularized (dist² + ε²)⁻³ term uses its exact scaling bound.

No integrability or numerical estimate is supplied as a hypothesis.

theorem Anderson4D.measurable_primitiveSupportIndicator (supportConstant ε : ℝ) : Measurable (primitiveSupportIndicator supportConstant ε)

theorem Anderson4D.integrable_invSqKer_mul_primitiveSupportIndicator (supportConstant ε : ℝ) : MeasureTheory.Integrable (fun (z : T4) => invSqKer z * primitiveSupportIndicator supportConstant ε z) paperMeasure

theorem Anderson4D.exists_integral_invSqKer_mul_primitiveSupportIndicator_le : ∃ (C : ℝ), 0 < C ∧ ∀ (supportConstant ε : ℝ), 0 < supportConstant → 0 < ε → ∫ (z : T4), invSqKer z * primitiveSupportIndicator supportConstant ε z ∂paperMeasure ≤ C * supportConstant ^ 2 * ε ^ 2

The local summand of (4.3) integrates to the volume scale (supportConstant * ε)².

theorem Anderson4D.integrable_primitiveKernelMajorant (C lam ε supportConstant : ℝ) (n : ℕ) (hε : 0 < ε) : MeasureTheory.Integrable (primitiveKernelMajorant C lam ε supportConstant n) paperMeasure

The full (4.3) majorant is integrable at every positive scale.

theorem Anderson4D.exists_integral_primitiveKernelMajorant_le : ∃ (Cball : ℝ) (Creg : ℝ), 0 < Cball ∧ 0 < Creg ∧ ∀ (C lam ε supportConstant : ℝ) (n : ℕ), 0 < ε → 0 < supportConstant → 1 ≤ |Real.log ε| → ∫ (z : T4), primitiveKernelMajorant C lam ε supportConstant n z ∂paperMeasure ≤ (C * lam) ^ (2 * n) * ((Cball * supportConstant ^ 2 + Creg) * ε⁻¹ ^ 2 / |Real.log ε|)

Integrated primitive majorant. If |log ε| ≥ 1, integrating (4.3) loses exactly ε⁻² |log ε|⁻¹. The two universal constants are chosen once, before every cutoff support radius, scale, coupling, order, and pointwise constant.