Integrability seam after one ordinary phased head

The one-head transport equation lamEps_pow_integral_incomingPhasedResidualDensity_eq_afterHead_of_ne_zero consumes full integrability of the incoming phased density and produces the post-head integral. Iterating it along the remaining suffix needs the same integrability statement for the post-head density itself. This file closes that seam: the post-head phased density, with its genuinely coordinate-dependent coefficient, is integrable.

Route: the incoming integrability is transported across the head/post splitting equivalence (measure-preserving), Fubini yields integrability of the head-block marginal, and on the almost-everywhere event carrying the weighted local sections the scaled marginal is exactly the post-head phased density, by the same reconstruction chain as the transport equation.

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_afterHead_incomingPhasedResidualDensity_of_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε 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) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (postCoefficient ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : MeasureTheory.Integrable (fun (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) => (res.afterHead head tail hremaining).incomingPhasedResidualDensity (postCoefficient v) k ρ ε x y v) (MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure)

After an ordinary (non-slot-zero-fed) head, the post-head phased density with a post-coordinate-dependent coefficient is integrable. This is the recursion seam matching the one-head transport equation.