Right exceptional/exceptional endpoint handoff #
The completed left density is the untouched parameter while the paired right incoming head, the intervening intervals, and the retained right outgoing terminal are removed in the signed paper order. No norm or new estimate is introduced.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.exists_of_exceptionalExceptional
{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)
(hsingles : e0.snd.fst.singles.Nonempty)
(data : R324PaperHalfExceptionalExceptionalRoute rightProviders)
:
Nonempty
(R324PaperRightRouteExactPackage left (R324PaperHalfEndpointRoute.exceptionalExceptional hfirst houtgoing data))
The literal right EE row, before any endpoint estimate.