Global endpoint/internal Fubini bridge for R-324

The frozen doubled moment term has the four external variables outside the terminal internal coordinate integral. The fixed-internal-coordinate identity in R324EndpointIntegratedResidualBridge may therefore be used only after an honest global Fubini interchange.

This file performs precisely that interchange. Its hypothesis is joint Bochner integrability of the exact signed externalModeResidualSumIntegrand on

(x, (y, (z, w))) × (left terminal coordinates × right terminal coordinates).

No norm and no termwise absolute value are introduced, so the complete primitive covariance sum remains grouped. Establishing the displayed joint integrability from the initial root and the certified within-half traces is a separate analytic obligation.

Fourfold endpoint-product normal form

theorem Anderson4D.R324TwoHalfTerminalData.integral_fourEndpoints (f : T4 → T4 → T4 → T4 → ℂ) (hf : MeasureTheory.Integrable (fun (e : T4 × T4 × T4 × T4) => f e.1 e.2.1 e.2.2.1 e.2.2.2) (paperMeasure.prod (paperMeasure.prod (paperMeasure.prod paperMeasure)))) : ∫ (e : T4 × T4 × T4 × T4), f e.1 e.2.1 e.2.2.1 e.2.2.2 ∂paperMeasure.prod (paperMeasure.prod (paperMeasure.prod paperMeasure)) = ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), f x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure

Fubini expansion of the explicitly right-associated product of the four endpoint measures. Keeping this lemma local makes the association used by the global joint-integrability hypothesis visible in the theorem below.

theorem Anderson4D.R324TwoHalfTerminalData.integral_fourEndpoints_with_internal_swap {P : Type u_1} [MeasurableSpace P] (μ : MeasureTheory.Measure P) [MeasureTheory.SFinite μ] (f : P → T4 → T4 → T4 → T4 → ℂ) (g : P → ℂ) (hjoint : MeasureTheory.Integrable (fun (ep : (T4 × T4 × T4 × T4) × P) => f ep.2 ep.1.1 ep.1.2.1 ep.1.2.2.1 ep.1.2.2.2) ((paperMeasure.prod (paperMeasure.prod (paperMeasure.prod paperMeasure))).prod μ)) (heval : ∀ (p : P), ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), f p x y z w ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = g p) : ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (p : P), f p x y z w ∂μ ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = ∫ (p : P), g p ∂μ

Reusable four-endpoint/internal Fubini substitution. The endpoint evaluation is supplied as one exact signed identity for each internal coordinate; this theorem introduces neither a norm nor a termwise sum.

Honest global endpoint/internal interchange

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (hjoint : MeasureTheory.Integrable (fun (ep : (T4 × T4 × T4 × T4) × (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) => terminal.externalModeResidualSumIntegrand π α β ep.2 ep.1.1 ep.1.2.1 ep.1.2.2.1 ep.1.2.2.2) ((paperMeasure.prod (paperMeasure.prod (paperMeasure.prod paperMeasure))).prod ((MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure)))) : ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), terminal.externalModeResidualSumIntegrand π α β p x y z w ∂(MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure) ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = ∫ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), terminal.endpointIntegratedResidualDensity π hleft hright α β p ∂(MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure)

Global Fubini substitution in the exact order required before passing from the signed expression (4.18) to the endpoint estimates of §4.2, Steps 3--4.

The left side is the frozen order: x, then y, then z, then w, with the terminal product coordinate innermost. The hypothesis is joint integrability on the corresponding endpoint product, followed by the terminal product measure. The right side has the terminal coordinate outside and all four endpoint integrations already evaluated by integral_externalModeResidualSumIntegrand.

The complete residual primitive sum is never split and no norm is taken.

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini_eq_initialNested {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (α β : Z4) (hjoint : MeasureTheory.Integrable (fun (ep : (T4 × T4 × T4 × T4) × (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) => terminal.externalModeResidualSumIntegrand π α β ep.2 ep.1.1 ep.1.2.1 ep.1.2.2.1 ep.1.2.2.2) ((paperMeasure.prod (paperMeasure.prod (paperMeasure.prod paperMeasure))).prod ((MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure)))) : ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), terminal.externalModeResidualSumIntegrand π α β p x y z w ∂(MeasureTheory.Measure.pi fun (x : terminal.left.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : terminal.right.SurvivingCoordinate) => paperMeasure) ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

The global Fubini identity followed by the already proved measure-preserving transport to the literal initial nested-cross carrier.