Paper §4.2, Step 3(c): the proper-head provider, discharged

Paper: R-324 — §4.2 Step 3(c), R324ProperHeadSharpProvider proved

R324NestedCrossBudgetIteration performs Step 3's nested-cross iteration on the actual carrier, and takes exactly one analytic input: the R324ProperHeadSharpProvider, whose single field is

∀ ctx left right, ctx.properHeadIntegral ρ lam ε left right ≤ (D·λ)^{2·order}

Unfolding, properHeadIntegral is

∫ p, |left − p₁|⁻² · crossGapPrimitiveTerm(p₁ − p₂) · |p₂ − right|⁻²

which is literally the elementary eight-dimensional integral of paper Step 3(c). So the provider is the paper's own sentence

"the induced pairing is primitive, so (4.4) bounds the inner sum"

and it follows from four proved facts, in this order:

1. crossGapPrimitiveTerm_le_insertedTerm — the moving-gap term is below the inserted pairing term at the block's own pairing (the hypotheses are normalizedInput_{measurable,nonneg,admissible});
2. primitivePairingKernelInsertedTerm_le_kernel — one pairing's term is below the primitive sum (blockPairing_mem);
3. proposition41_at_truncation — (4.4) bounds that by the inserted majorant, at any order inside the paper truncation, which order_le_ambient supplies from the cap m ≤ ⌊|log ε|⌋;
4. exists_r324ProperInsertedConvolution_le — the resulting |·|⁻² ∗ J̃ ∗ |·|⁻² convolution is bounded by (Cλ)^{2·order}·K, whose K is absorbed into the base.

The nonnegativity used in 1–2 is the |G_j| branch of (4.19)–(4.20): it is legitimate here precisely because the removals of Step 2(d)–(e) have already been performed, i.e. Step 2(f) has been passed.

theorem Anderson4D.r324NestedCross_crossGapPrimitiveTerm_le_majorant (ρ : SmoothCutoff) {lam ε supportConstant C : ℝ} (hprop : ∀ (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), 0 < lam → 0 < ε → ε ≤ 1 → n ≤ truncOrder ε → IsAdmissiblePrimitiveInput n G → ∀ (z : T4), |primitiveKernelInsertedDiff ρ lam ε n hn G z| ≤ primitiveInsertedMajorant C lam ε supportConstant n z) (hlam : 0 < lam) (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (hmtrunc : m ≤ truncOrder ε) (z : T4) : ctx.crossGapPrimitiveTerm ρ lam ε ctx.normalizedInput z 0 ≤ primitiveInsertedMajorant C lam ε supportConstant ctx.order z

Step 3(c) at one proper nested head: the moving-gap term is below the inserted majorant of (4.4).

theorem Anderson4D.exists_r324ProperHeadSharpProvider (ρ : SmoothCutoff) : ∃ (D : ℝ), 0 < D ∧ ∀ (lam ε : ℝ) {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324ProperHeadSharpProvider ρ lam ε D κp κm π

The proper-head provider of Step 3, discharged.

Every hypothesis is the paper's: a positive coupling, a small scale, and the paper truncation m ≤ ⌊|log ε|⌋ under which (3.24) is asserted at all. The constant is chosen before the coupling, the scale, the order, the pairings, and the head.