Terminal residual-sum joint integrability for R-324

This module closes the analytic premise isolated by R324EndpointJointIntegrabilityAdapter. The two completed within-half Green chains are separately integrable on their endpoint/internal product spaces. A measure-preserving regrouping puts their product on the exact four-endpoint/terminal-coordinate carrier used by the endpoint Fubini theorem. The complete residual primitive sum is then attached as one bounded measurable factor.

No termwise norm of the primitive sum, target integrability certificate, or moment estimate is assumed.

Measurability of the terminal reconstruction and cross factor

theorem Anderson4D.R324WithinHalfResidualPrefix.measurable_reconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Measurable res.reconstruct

Reconstructing the ambient tuple from the surviving coordinates is measurable for the product measurable spaces.

theorem Anderson4D.R324TwoHalfTerminalData.measurable_terminalDoubledReconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) : Measurable terminal.terminalDoubledReconstruct

The doubled ambient tuple assembled from the two terminal sparse carriers is measurable.

theorem Anderson4D.R324TwoHalfTerminalData.measurable_residualSumCrossFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) : Measurable fun (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) => terminal.residualSumCrossFactor π p.1 p.2

The grouped residual primitive sum is measurable on the exact product of the two terminal sparse carriers.

theorem Anderson4D.R324TwoHalfTerminalData.exists_norm_residualSumCrossFactor_le {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (hε : 0 < ε) (hε1 : ε ≤ 1) (π : ↥κp.singles ≃ ↥κm.singles) : ∃ (bound : ℝ), 0 ≤ bound ∧ ∀ (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)), ‖terminal.residualSumCrossFactor π p.1 p.2‖ ≤ bound

At positive mollification scale the grouped residual primitive sum has a uniform norm bound on the terminal product carrier.

Exact endpoint/internal product regrouping

The genuine producer

theorem Anderson4D.R324TwoHalfTerminalData.terminalChainProductsJointIntegrable_of_edgeCertificates {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (leftScale rightScale : Fin (m + 1) → ℝ) (hleftCertificate : R324WithinHalfEdgeCertificate terminal.left.state leftScale) (hrightCertificate : R324WithinHalfEdgeCertificate terminal.right.state rightScale) : MeasureTheory.Integrable (fun (ep : (T4 × T4 × T4 × T4) × (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) => ↑(terminal.left.residualChainProduct ep.1.1 ep.1.2.1 (terminal.left.reconstruct ep.2.1)) * ↑(terminal.right.residualChainProduct ep.1.2.2.1 ep.1.2.2.2 (terminal.right.reconstruct ep.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 two certified terminal half chains are jointly integrable on the literal four-endpoint/terminal-coordinate carrier. This is the reusable bare analytic core of the residual-sum producer below: no covariance or selector factor has yet been attached.

theorem Anderson4D.R324TwoHalfTerminalData.terminalResidualSumJointIntegrable_of_edgeCertificates {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (π : ↥κp.singles ≃ ↥κm.singles) (hε : 0 < ε) (hε1 : ε ≤ 1) (leftScale rightScale : Fin (m + 1) → ℝ) (hleftCertificate : R324WithinHalfEdgeCertificate terminal.left.state leftScale) (hrightCertificate : R324WithinHalfEdgeCertificate terminal.right.state rightScale) : terminal.TerminalResidualSumJointIntegrable π

The two terminal edge certificates and positive-scale covariance bound produce the exact unphased joint-integrability premise of the endpoint adapter.

theorem Anderson4D.R324TwoHalfTerminalData.terminalResidualSumJointIntegrable_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) (hε : 0 < ε) (hε1 : ε ≤ 1) (leftTerminalScale rightTerminalScale : Fin (m + 1) → ℝ) (hleftCertificate : R324WithinHalfEdgeCertificate leftTrace.terminalPrefix.state leftTerminalScale) (hrightCertificate : R324WithinHalfEdgeCertificate rightTrace.terminalPrefix.state rightTerminalScale) : (ofCertifiedTraces leftTrace rightTrace).TerminalResidualSumJointIntegrable π

Specialization of the preceding producer to the terminal data packaged by two certified within-half traces.