The completed right endpoint half, in all four literal cases #
This is only the paper Step 4(A) case split on the second half. Each branch has already completed its signed incoming operation, all intervening intervals, and its outgoing operation before exposing the common exact package.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.exists_of_route
{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)
(hsingles : e0.snd.fst.singles.Nonempty)
(route : R324PaperHalfEndpointRoute rightProviders)
:
Nonempty (R324PaperRightRouteExactPackage left route)
Literal four-case constructor for the completed right half.