Joint integrability through one R-324 residual head

The scalar one-head theorem in R324ConcretePhaseATraceAssembly preserves integrability at fixed endpoints. The physical two-half argument also needs the corresponding statement with an arbitrary measured parameter carried jointly with the surviving coordinates.

The proof does not infer joint integrability from pointwise section integrability. Instead it transports the current joint density through the actual head/post coordinate split, moves the head coordinates to the front, and obtains an integrable parameterized head integral by Bochner--Fubini. The existing weighted local collapse then identifies that integral with the post-head residual density almost everywhere.

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_joint_residualIntegrand_mul_postOuter_afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : Y → T4) (postOuter : Y → ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (hfull : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => ↑(res.residualIntegrand ρ ε (x p.1) (y p.1) (res.reconstruct p.2)) * postOuter p.1 ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) p.2).2) (ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) (internal : res.R324WithinHalfResidualInternalReady head tail hremaining) : MeasureTheory.Integrable (fun (p : Y × ((res.afterHead head tail hremaining).SurvivingCoordinate → T4)) => ↑((res.afterHead head tail hremaining).residualIntegrand ρ ε (x p.1) (y p.1) ((res.afterHead head tail hremaining).reconstruct p.2)) * postOuter p.1 p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure))

One concrete residual head preserves integrability jointly with an arbitrary measured parameter.

The parameter may control both displayed endpoints and the post-head outer factor. The only analytic hypotheses are joint integrability of the genuine current weighted residual density and the endpoint-independent internal certificate already carried by a certified R-324 trace.