Certified terminal endpoint Fubini for R-324

This module composes the genuine terminal joint-integrability producer with the endpoint Fubini adapter. Thus two certified within-half traces and their terminal edge certificates suffice for both exact endpoint-integration identities; no separate joint-integrability hypothesis remains.

The complete residual primitive sum stays grouped throughout, and no norm or estimate is introduced.

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini_ofCertifiedTraces {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (leftTerminalScale rightTerminalScale : Fin (m + 1) → ℝ) (hleftCertificate : R324WithinHalfEdgeCertificate leftTrace.terminalPrefix.state leftTerminalScale) (hrightCertificate : R324WithinHalfEdgeCertificate rightTrace.terminalPrefix.state rightTerminalScale) : let terminal := ofCertifiedTraces leftTrace rightTrace; ∫ (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)

Certified within-half traces and their terminal edge certificates discharge the analytic premise of the exact four-endpoint Fubini identity.

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini_eq_initialNested_ofCertifiedTraces {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (leftTerminalScale rightTerminalScale : Fin (m + 1) → ℝ) (hleftCertificate : R324WithinHalfEdgeCertificate leftTrace.terminalPrefix.state leftTerminalScale) (hrightCertificate : R324WithinHalfEdgeCertificate rightTrace.terminalPrefix.state rightTerminalScale) : let terminal := ofCertifiedTraces leftTrace rightTrace; ∫ (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 certified endpoint Fubini identity followed by exact measure-preserving transport to the initial nested-cross carrier.

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini_usingStoredCertificates {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) : let terminal := ofCertifiedTraces leftTrace rightTrace; ∫ (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)

Tighter certified-trace API for the four-endpoint Fubini identity. The terminal scales and certificates are the ones genuinely stored by the two trace constructors.

theorem Anderson4D.R324TwoHalfTerminalData.integral_externalModeResidualSumIntegrand_fubini_eq_initialNested_usingStoredCertificates {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) : let terminal := ofCertifiedTraces leftTrace rightTrace; ∫ (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

Tighter certified-trace API for the exact initial nested-cross transport, using the terminal certificates stored by the traces.