Joint-integrability adapter for the R-324 endpoint bridge

The global endpoint/internal Fubini theorem requires joint integrability of the character-decorated terminal residual-sum density. The four Fourier characters are bounded measurable multipliers of norm one, so the exact upstream analytic obligation is instead joint integrability of the unphased terminalResidualSumPhysicalCore.

This file isolates that obligation and proves that it produces the exact hjoint hypothesis, without splitting the complete residual primitive sum or taking a termwise norm. It also supplies direct composition theorems for the two Fubini conclusions.

The predicate below packages the unphased joint-integrability hypothesis. The theorems in this file show that it suffices for the character-decorated Fubini conclusions without splitting the signed primitive sum.

def Anderson4D.R324TwoHalfTerminalData.TerminalResidualSumJointIntegrable {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : Prop

The exact unphased analytic certificate for the global endpoint/internal Fubini bridge. Its endpoint association agrees literally with integral_externalModeResidualSumIntegrand_fubini.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324TwoHalfTerminalData.integrable_externalModeResidualSumIntegrand_of_terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (α β : Z4) (hterminal : terminal.TerminalResidualSumJointIntegrable π) : 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)))

The unphased terminal certificate produces the exact hjoint hypothesis of the global Fubini theorem. Only multiplication by the four unit-norm characters is used; the grouped residual primitive sum remains inside terminalResidualSumPhysicalCore.

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini_of_terminal {ρ : 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) (hterminal : terminal.TerminalResidualSumJointIntegrable π) : ∫ (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)

The unphased terminal certificate discharges the global Fubini premise and evaluates all four endpoint integrations before the terminal internal integral.

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini_eq_initialNested_of_terminal {ρ : 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) (hterminal : terminal.TerminalResidualSumJointIntegrable π) : ∫ (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 preceding Fubini evaluation followed by the exact measure-preserving transport to the literal initial nested-cross carrier.