Canonical terminal adapter for the paper endpoint routes #
The signed physical-root collapse and the endpoint-route construction may build their completed within-half prefixes independently. Both prefixes are algebraically reachable, have consumed the complete analytic schedule, and retain the empty suffix. Reachability is deterministic in the processed list, so the resulting residual prefix is canonical.
Only the residual prefixes are identified here. Analytic and numerical scale functions remain deliberately distinct.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.completedRoute_final_eq_certifiedTerminal
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{incomingMode : Z4}
{analyticScale : Fin (m + 1) → ℝ}
{providers : R324PaperHalfRouteProviders pairing incomingMode}
(route : R324PaperHalfEndpointRoute providers)
(trace : (initial rho lam eps pairing).R324WithinHalfCertifiedAnalyticTrace analyticScale)
:
A completed endpoint route and a certified analytic trace from the same pairing have the same literal terminal residual prefix.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.terminal_eq_ofCertifiedTraces
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{leftMode rightMode : Z4}
{leftScale rightScale : Fin (m + 1) → ℝ}
{leftProviders : R324PaperHalfRouteProviders kappaP leftMode}
{rightProviders : R324PaperHalfRouteProviders kappaM rightMode}
(routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders)
(leftTrace : (initial rho lam eps kappaP).R324WithinHalfCertifiedAnalyticTrace leftScale)
(rightTrace : (initial rho lam eps kappaM).R324WithinHalfCertifiedAnalyticTrace rightScale)
:
The two independently constructed terminal packages agree after the two canonical one-half residual prefixes are identified.