Right direct/direct endpoint handoff #
This is the direct/direct row of the second-half table. The completed left density remains signed while the right incoming and outgoing Fourier variables are evaluated. No norm is taken.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.exists_of_directDirect
{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 : R324PaperHalfDirectDirectRoute rightProviders)
:
Nonempty (R324PaperRightRouteExactPackage left (R324PaperHalfEndpointRoute.directDirect hfirst houtgoing data))
The paper's two exact Fourier evaluations on the right, with the completed left half as the untouched parameter.