Uniform two-half endpoint-route assembly

This is the structural entrance to paper Step 4(A). The constants from Proposition 4.1 are chosen once, the two literal half routes are selected by their actual endpoint incidences, and the independently generated analytic traces are identified with the same canonical terminal residual prefixes.

No endpoint absolute value or uniform eps ^ (-8) estimate is taken here.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_r324PaperTwoHalfEndpointRoutes_at_truncation (rho : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ), 0 < supportConstant ∧ 0 < C ∧ 1 ≤ K ∧ 1 ≤ A ∧ ∀ (lam eps : ℝ) (m : ℕ) (kappaP kappaM : PartialPairing (Fin m)) (leftMode rightMode : Z4), 0 < lam → 0 < eps → eps ≤ 1 → 1 ≤ |Real.log eps| → m ≤ truncOrder eps → 0 < m → kappaP.singles.Nonempty → kappaM.singles.Nonempty → ∃ (leftProviders : R324PaperHalfRouteProviders kappaP leftMode) (rightProviders : R324PaperHalfRouteProviders kappaM rightMode) (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) (leftTrace : (initial rho lam eps kappaP).R324WithinHalfCertifiedAnalyticTrace fun (x : Fin (m + 1)) => A) (rightTrace : (initial rho lam eps kappaM).R324WithinHalfCertifiedAnalyticTrace fun (x : Fin (m + 1)) => A), routes.terminal = R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace

Uniform structural data for the two literal half routes in paper Step 4(A). The endpoint cases remain the actual DD/DE/ED/EE cases of the two pairings; their costs are not yet uniformized.