Right direct/exceptional endpoint handoff #
The completed left density stays signed while the direct right incoming Fourier variable, all intervening intervals, and the retained right outgoing terminal are removed in the paper order. No norm or endpoint estimate is introduced.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.exists_of_directExceptional
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{alpha beta : Z4}
{p : R324RefinedScheduleIndex m}
{e0 : MomentContraction m}
{leftProviders : R324PaperHalfRouteProviders e0.fst alpha}
{rightProviders : R324PaperHalfRouteProviders e0.snd.fst (-alpha)}
{leftRoute : R324PaperHalfEndpointRoute leftProviders}
(left : R324PaperLeftRouteExactPackage p e0 leftRoute beta)
(hfirst : ⟨0, ⋯⟩ ∈ finalActive e0.snd.fst)
(houtgoing : Fin.last m ∈ extractedRightEdges e0.snd.fst)
(data : R324PaperHalfDirectExceptionalRoute rightProviders)
:
Nonempty (R324PaperRightRouteExactPackage left (R324PaperHalfEndpointRoute.directExceptional hfirst houtgoing data))
The literal right DE row, using only the signed completed-left handoff
and the retained-terminal Fubini license.