Signed integrability after a retained outgoing terminal

This lower-level file supplies the exact signed Fubini license used after a retained outgoing terminal in paper Step 4(A). No endpoint norm or positive majorant is introduced.

Signed Fubini license for a retained outgoing terminal

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.integrable_parameter_outgoingEndpointDefectDensity {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0) (hactive : data.terminalPost.state.active.Nonempty) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muU] (coefficient : U → (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : U → T4) (hsource : MeasureTheory.Integrable (fun (q : U × T4 × (data.endpoint.stop.SurvivingCoordinate → T4)) => data.endpoint.stop.incomingPhasedResidualDensity (coefficient q.1 ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯) q.2.2).2) incomingMode rho eps (x q.1) q.2.1 q.2.2) (muU.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : data.endpoint.stop.SurvivingCoordinate) => paperMeasure)))) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminalData.terminal.2) (↑kappaB) data.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure)) : MeasureTheory.Integrable (fun (q : U × (data.terminalPost.SurvivingCoordinate → T4)) => ∫ (first : T4), data.outgoingEndpointDefectDensity (coefficient q.1) incomingMode outgoingMode (x q.1) q.2 first ∂paperMeasure) (muU.prod (MeasureTheory.Measure.pi fun (x : data.terminalPost.SurvivingCoordinate) => paperMeasure))

Joint integrability survives the retained outgoing terminal operation with an arbitrary measured parameter outside. The proof follows the exact paper coordinates (first, gap, internal, outgoing endpoint): it transports the given stop density by measure-preserving equivalences and then takes the three signed marginals exposed by integral_lamEps_pow_terminalOutgoingFourier_gap_eq_defect.

This is an integrability statement only. It neither bounds nor replaces the signed defect density by a positive majorant.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.integrable_parameter_outgoingEndpointDefectDensity_transport {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} {left right : res.R324PaperOutgoingEndpointTerminal} (h : left = right) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) (coefficient : U → (right.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : U → T4) (hintegrable : MeasureTheory.Integrable (fun (q : U × (left.terminalPost.SurvivingCoordinate → T4)) => ∫ (first : T4), left.outgoingEndpointDefectDensity (⋯.mp (coefficient q.1)) incomingMode outgoingMode (x q.1) q.2 first ∂paperMeasure) (muU.prod (MeasureTheory.Measure.pi fun (x : left.terminalPost.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (fun (q : U × (right.terminalPost.SurvivingCoordinate → T4)) => ∫ (first : T4), right.outgoingEndpointDefectDensity (coefficient q.1) incomingMode outgoingMode (x q.1) q.2 first ∂paperMeasure) (muU.prod (MeasureTheory.Measure.pi fun (x : right.terminalPost.SurvivingCoordinate) => paperMeasure))

Transport the signed target integrability across equality of retained outgoing-terminal presentations. This is useful for the DE geometry, whose canonical presentation is propositionally (not definitionally) the route presentation.