Right exceptional/direct endpoint handoff #
The incoming paired head is collapsed first, the remaining right intervals are transported exactly, and only then is the direct outgoing Fourier variable evaluated. The completed left density is an untouched parameter throughout.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.exists_of_exceptionalDirect
{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 : R324PaperHalfExceptionalDirectRoute rightProviders)
:
Nonempty (R324PaperRightRouteExactPackage left (R324PaperHalfEndpointRoute.exceptionalDirect hfirst houtgoing data))
The literal right ED row, before any endpoint estimate.