Uniform paper endpoint-route providers #
This file extracts the common numerical setup used in paper Step 4(A). Proposition 4.1, the local block closure, and the inserted primitive majorant choose constants uniformly before the ambient order, pairing, and incoming Fourier mode. The resulting package is exactly the provider consumed by the four structural endpoint routes.
theorem
Anderson4D.R324WithinHalfResidualPrefix.exists_r324PaperHalfRouteProviders_at_truncation
(rho : SmoothCutoff)
:
∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ),
0 < supportConstant ∧ 0 < C ∧ 1 ≤ K ∧ 1 ≤ A ∧ ∀ (lam eps : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)) (incomingMode : Z4),
0 < lam →
0 < eps →
eps ≤ 1 →
1 ≤ |Real.log eps| →
m ≤ truncOrder eps → 0 < m → Nonempty (R324PaperHalfRouteProviders pairing incomingMode)
Uniform construction of the analytic, budget, exceptional-head, and initial-certificate inputs used by every one-half endpoint route at the paper truncation. No fullness assumption is needed: each literal residual block has order at most the ambient half-order.