The final complete nested-cross head

After all proper inner shells have been removed, paper Step 3 applies Proposition 4.1 once to the complete outermost primitive block. This file proves the measure-theoretic bridge needed for that last application: the complete normalized block is integrable, its full integral is the integral of its two-endpoint kernel, and a radial endpoint bound costs exactly one paper volume.

theorem Anderson4D.R324NestedCrossStepContext.measurable_completeCrossGapPrimitiveTerm_normalized {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : Measurable fun (p : T4 × T4) => ctx.completeCrossGapPrimitiveTerm ρ lam ε ctx.normalizedInput p.1 p.2

Measurability of the complete normalized two-endpoint term.

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveTerm_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * ctx.order - 1)) (z : T4), 0 ≤ G j z) (z w : T4) : 0 ≤ ctx.completeCrossGapPrimitiveTerm ρ lam ε G z w

Nonnegativity of the integrated complete head.

theorem Anderson4D.R324NestedCrossStepContext.integrable_completeNormalizedHeadDensity_of_term_le {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (J : T4 → ℝ) (hJ : MeasureTheory.Integrable J paperMeasure) (hJmeas : Measurable J) (hle : ∀ (z : T4), ctx.completeCrossGapPrimitiveTerm ρ lam ε ctx.normalizedInput z 0 ≤ J z) : MeasureTheory.Integrable (ctx.completeNormalizedHeadDensity ρ lam ε) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure)

A complete normalized block is integrable whenever its already-integrated two-endpoint term is dominated by an integrable radial kernel.

theorem Anderson4D.R324NestedCrossStepContext.integral_completeNormalizedHeadDensity_le_of_term_le {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (J : T4 → ℝ) (hJ : MeasureTheory.Integrable J paperMeasure) (hJmeas : Measurable J) (hle : ∀ (z : T4), ctx.completeCrossGapPrimitiveTerm ρ lam ε ctx.normalizedInput z 0 ≤ J z) : (∫ (t : Fin (2 * ctx.order) → T4), ctx.completeNormalizedHeadDensity ρ lam ε t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure) ≤ (2 * Real.pi) ^ dim * ∫ (z : T4), J z ∂paperMeasure

The final complete block is bounded by one radial endpoint majorant, with only the translation-volume factor left outside.

theorem Anderson4D.R324NestedCrossStepContext.exists_completeTerminalHead_bound_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (ctx : R324NestedCrossStepContext κp κm π) (lam ε : ℝ), 0 < lam → 0 < ε → ε ≤ 1 → m ≤ truncOrder ε → (∫ (t : Fin (2 * ctx.order) → T4), ctx.completeNormalizedHeadDensity ρ lam ε t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.order)) => paperMeasure) ≤ (2 * Real.pi) ^ dim * ∫ (z : T4), primitiveInsertedMajorant C lam ε supportConstant ctx.order z ∂paperMeasure

Uniform final-head form of Proposition 4.1. The constants are chosen once from the cutoff and work for every literal final block in the ambient truncation range.