Parameterized exceptional/exceptional endpoint splice

This is the one parameter-carrier variant missing from the paper Step 4(A) endpoint table. The incoming exceptional head and every prefix interval are removed first. The retained outgoing terminal is then Fourier-integrated before any norm is taken. An arbitrary already-completed opposite-half carrier remains untouched throughout.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_initialResidual_eq_singleParameter_incomingExceptional_outgoingExceptional {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly pairing initialScale) (outgoing : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324PaperOutgoingEndpointTerminal) {U : Type u_1} [MeasurableSpace U] (muU : MeasureTheory.Measure U) [MeasureTheory.SFinite muU] (coefficient : U → (outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (hm : 0 < m) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hincoming : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminal.2) (↑kappaB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (hcurrent : MeasureTheory.Integrable (data.incomingExceptionalInitialSourceDensity incomingMode (fun (omega : T4 × U) => omega.1) fun (omega : T4 × U) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1 * coefficient omega.2 ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) (outgoing.endpoint.projection v)).2) ((paperMeasure.prod (paperMeasure.prod muU)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure))) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity incomingMode (fun (omega : T4 × U) => omega.1) fun (omega : T4 × U) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1 * coefficient omega.2 ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) (outgoing.endpoint.projection v)).2) ((paperMeasure.prod (paperMeasure.prod muU)).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) (hpred : r324WithinHalfPredecessorSlot outgoing.endpoint.stop.state outgoing.terminalData.terminal ≠ 0) (hactive : outgoing.terminalPost.state.active.Nonempty) (hendpoint : MeasureTheory.Integrable (fun (q : (T4 × U) × (outgoing.endpoint.stop.SurvivingCoordinate → T4)) => outgoing.endpoint.stop.incomingPhasedResidualDensity (outgoing.endpoint.multiplier incomingMode * (↑(paperSecondOrderModeDecay incomingMode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges incomingMode * coefficient q.1.2 ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) q.2).2)) incomingMode rho eps 0 q.1.1 q.2) ((paperMeasure.prod muU).prod (MeasureTheory.Measure.pi fun (x : outgoing.endpoint.stop.SurvivingCoordinate) => paperMeasure))) (houtgoing : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder outgoing.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder outgoing.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder outgoing.terminalData.terminal.2) (↑kappaB) outgoing.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder outgoing.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder outgoing.terminalData.terminal.2 - 2)) => paperMeasure)) : ↑(lamEps lam eps) ^ (2 * (initial rho lam eps pairing).remainingOrder) * ∫ (p : (T4 × T4 × U) × ((initial rho lam eps pairing).SurvivingCoordinate → T4)), data.incomingExceptionalInitialSourceDensity incomingMode (fun (omega : T4 × U) => omega.1) (fun (omega : T4 × U) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => charT4 outgoingMode omega.1 * coefficient omega.2 ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) (outgoing.endpoint.projection v)).2) p ∂(paperMeasure.prod (paperMeasure.prod muU)).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps pairing).SurvivingCoordinate) => paperMeasure) = ∫ (u : U), ∫ (v : outgoing.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), outgoing.outgoingEndpointDefectDensity (fun (post : outgoing.terminalPost.SurvivingCoordinate → T4) => outgoing.endpoint.multiplier incomingMode * (↑(paperSecondOrderModeDecay incomingMode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges incomingMode * coefficient u post)) incomingMode outgoingMode 0 v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : outgoing.terminalPost.SurvivingCoordinate) => paperMeasure ∂muU

Exact paper-ordered exceptional-incoming/exceptional-outgoing splice with one arbitrary untouched parameter carrier. This is the EEEE seam in the two-half endpoint table: applying it to the second half leaves the already completed first half outside every signed endpoint integral.