The ordinary-to-inserted majorant bridge for empty residual R-324 fibres

In the full/full branch of paper Section 4.2 Step 1, no residual primitive block remains. The surviving quadratic gap must therefore be used directly against the ordinary Proposition 4.1 majorant. This file records the honest numerical comparison: the support term costs supportConstant², while the regularized term costs 1.

This is a comparison of the two explicit nonnegative majorants. It does not assert a pointwise comparison between either signed primitive kernel.

theorem Anderson4D.torusDistSq_mul_primitiveKernelMajorant_le_max_one_sq_mul_inserted (C lam ε supportConstant : ℝ) (n : ℕ) (z : T4) : torusDistSq z * primitiveKernelMajorant C lam ε supportConstant n z ≤ max 1 (supportConstant ^ 2) * primitiveInsertedMajorant C lam ε supportConstant n z

Multiplication by the surviving squared gap converts the ordinary Proposition 4.1 majorant into the inserted majorant, at the sharp uniform factor max 1 supportConstant².

No sign assumptions on C or lam are needed because their common exponent is even. The degenerate scale ε = 0 is also valid algebraically (both majorants vanish under Lean's totalized inverse convention).

theorem Anderson4D.integral_torusDistSq_mul_primitiveKernelMajorant_le_max_one_sq_mul_integral_inserted (C lam ε supportConstant : ℝ) (n : ℕ) (hε : 0 < ε) : ∫ (z : T4), torusDistSq z * primitiveKernelMajorant C lam ε supportConstant n z ∂paperMeasure ≤ max 1 (supportConstant ^ 2) * ∫ (z : T4), primitiveInsertedMajorant C lam ε supportConstant n z ∂paperMeasure

Integrated form of torusDistSq_mul_primitiveKernelMajorant_le_max_one_sq_mul_inserted. Positivity of ε is required only for the two integrability facts; no positivity assumption on the coupling parameters is needed.