Joint integrability for the retained-endpoint transport

Paper Step 4(A) keeps all untouched endpoint parameters outside the signed within-half eliminations. The scalar transport in the alternating driver is therefore not enough at the retained outgoing block: Fubini needs genuine joint integrability in those parameters and the surviving spatial carrier.

This file is the parameter-carrying version of the two existing scalar handover proofs. It uses the same head/post splitting equivalence and the same fixed-section collapse identities. No norm estimate or new route is introduced.

One ordinary head

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_incomingPhasedResidualDensity_head_eq_afterHead_of_ne_zero {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix rho lam eps pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) (x y : T4) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) (hhead : MeasureTheory.Integrable (fun (t : Fin (2 * residualBlockOrder head.2) → T4) => res.incomingPhasedResidualDensity (postCoefficient v) k rho eps x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)) (hinternal : ∀ᵐ (ae_p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (kappaB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder head.2) (↑kappaB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ ae_p.1 ae_p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (↑(lamEps lam eps) ^ (2 * residualBlockOrder head.2) * ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), res.incomingPhasedResidualDensity (postCoefficient v) k rho eps x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = (res.afterHead head tail hremaining).incomingPhasedResidualDensity (postCoefficient v) k rho eps x y v

Fixed post coordinates: the ordinary phased head integral is exactly the post-head phased density. This is the pointwise identity used implicitly in the scalar integrability handover, exposed here so an arbitrary measured parameter can remain outside the head integral.

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_joint_afterHead_incomingPhasedResidualDensity_of_ne_zero {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {Y : Type u_1} [MeasurableSpace Y] (nu : MeasureTheory.Measure Y) [MeasureTheory.SFinite nu] (res : R324WithinHalfResidualPrefix rho lam eps pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) (x y : Y → T4) (postCoefficient : Y → ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (postCoefficient p.1 ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) p.2).2) k rho eps (x p.1) (y p.1) p.2) (nu.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) (hinternal : ∀ᵐ (ae_p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (kappaB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder head.2) (↑kappaB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ ae_p.1 ae_p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : MeasureTheory.Integrable (fun (p : Y × ((res.afterHead head tail hremaining).SurvivingCoordinate → T4)) => (res.afterHead head tail hremaining).incomingPhasedResidualDensity (postCoefficient p.1 p.2) k rho eps (x p.1) (y p.1) p.2) (nu.prod (MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure))

Joint integrability crosses one ordinary head while arbitrary measured endpoint parameters remain outside the head integral.

Parameter-carrying ordinary traces

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.integrable_joint_trace_end_incomingPhasedResidualDensity {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {Y : Type u_1} [MeasurableSpace Y] (nu : MeasureTheory.Measure Y) [MeasureTheory.SFinite nu] {res : R324WithinHalfResidualPrefix rho lam eps pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (hordinary : trace.OrdinaryAlong) (x y : Y → T4) (coefficient : Y → (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (coefficient p.1 (trace.terminalProjection p.2)) k rho eps (x p.1) (y p.1) p.2) (nu.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (fun (p : Y × (trace.terminalPrefix.SurvivingCoordinate → T4)) => trace.terminalPrefix.incomingPhasedResidualDensity (coefficient p.1 p.2) k rho eps (x p.1) (y p.1) p.2) (nu.prod (MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure))

Joint form of the ordinary trace handover. The external parameter is untouched by every head elimination, exactly as in paper Step 2(f).

Ordinary stopped traces and the two-phase exceptional combinator

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.integrable_joint_stop_incomingPhasedResidualDensity {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {Y : Type u_1} [MeasurableSpace Y] (nu : MeasureTheory.Measure Y) [MeasureTheory.SFinite nu] {res : R324WithinHalfResidualPrefix rho lam eps pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (hordinary : trace.OrdinaryAlong) (x y : Y → T4) (coefficient : Y → (trace.stopPrefix.SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (coefficient p.1 (trace.stopProjection p.2)) k rho eps (x p.1) (y p.1) p.2) (nu.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (fun (p : Y × (trace.stopPrefix.SurvivingCoordinate → T4)) => trace.stopPrefix.incomingPhasedResidualDensity (coefficient p.1 p.2) k rho eps (x p.1) (y p.1) p.2) (nu.prod (MeasureTheory.Measure.pi fun (x : trace.stopPrefix.SurvivingCoordinate) => paperMeasure))

Parameter-carrying ordinary transport to a retained stop.