Parameterized direct/direct half splice

This is the only parameter-carrier composition not already named in R324PaperEndpointTwoHalfSplice. The complete alternating transport is performed sectionwise while the expression is signed. Its multiplier is then moved back inside the terminal coefficient, and the two free endpoint variables are Fourier-integrated by integral_singleParameter_incomingPhasedResidualDensity_eq_directOutgoing. No norm occurs.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfAlternatingTransport.lamEps_pow_integral_initialResidual_eq_singleParameter_directDirect {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (transport : (initial rho lam eps pairing).R324WithinHalfAlternatingTransport) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muU] (red : U → (transport.final.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (hcurrent : MeasureTheory.Integrable (fun (q : (T4 × U) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)) => (initial rho lam eps pairing).incomingPhasedResidualDensity (charT4 outgoingMode q.1.1 * red q.1.2 (transport.projection q.2)) incomingMode rho eps 0 q.1.1 q.2) ((paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure))) (hactive : transport.final.state.active.Nonempty) (hedge : transport.final.state.edges (transport.final.terminalOutgoingEdgeSlot hactive) = greenFn) (hterminal : MeasureTheory.Integrable (fun (q : (T4 × U) × (transport.final.SurvivingCoordinate → T4)) => transport.final.incomingPhasedResidualDensity (charT4 outgoingMode q.1.1 * (transport.multiplier incomingMode * red q.1.2 q.2)) incomingMode rho eps 0 q.1.1 q.2) ((paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : transport.final.SurvivingCoordinate) => paperMeasure))) : ↑(lamEps lam eps) ^ (2 * (initial rho lam eps pairing).remainingOrder) * ∫ (q : (T4 × U) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)), (initial rho lam eps pairing).incomingPhasedResidualDensity (charT4 outgoingMode q.1.1 * red q.1.2 (transport.projection q.2)) incomingMode rho eps 0 q.1.1 q.2 ∂(paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure) = ∫ (u : U), ∫ (v : transport.final.SurvivingCoordinate → T4), transport.multiplier incomingMode * red u v * charT4 incomingMode (transport.final.terminalIncomingAnchor (transport.final.reconstruct v)) * ↑(transport.final.endpointErasedSignedChain hactive 0 0 (transport.final.reconstruct v)) * translatedGreenMode outgoingMode (transport.final.terminalOutgoingAnchor hactive (transport.final.reconstruct v)) ∂MeasureTheory.Measure.pi fun (x : transport.final.SurvivingCoordinate) => paperMeasure ∂muU

Complete signed DD operation with one arbitrary untouched parameter. The parameter is the already completed opposite half in the 4 x 4 assembly.