Uniform constants for the first primitive order #
This file packages the analytic n = 1 bounds with constants chosen once
from the cutoff, before the coupling, scale, or input kernel. It is the
uniform base case needed by the global Proposition 4.1 induction.
theorem
Anderson4D.exists_uniform_primitiveKernelBounds_one
(ρ : SmoothCutoff)
:
∃ (supportConstant : ℝ) (C : ℝ),
0 < supportConstant ∧ 0 < C ∧ ∀ (lam ε orderConstant : ℝ) (G : Fin 1 → T4 → ℝ),
PrimitiveEstimateRegime 1 lam ε orderConstant supportConstant C →
IsAdmissiblePrimitiveInput 1 G → PrimitiveKernelBounds ρ lam ε 1 ⋯ G supportConstant C
Uniform cutoff-dependent constants close both pointwise estimates of
Proposition 4.1 at order n = 1. The symmetry-class conclusion is kept
separate, since it is a structural periodization lemma rather than an
analytic estimate.