Documentation

Anderson4D.Continuum.PrimitiveBaseUniform

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.