Smooth moments with the additional prime-argument totient power

The finite envelope uses degree plus one, but the growth condition remains that of the original polynomial family.

theorem NairTenenbaum.PolynomialSystem.primeArgument_smooth_moment_uniform {k r : ℕ} (P : PolynomialSystem k r) {A B ε κ z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hzκ : 4 ^ ((↑P.total.natDegree + 1) * κ) ≤ z) (hgε : ↑P.total.natDegree * ε ≤ 1 / 8) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, (rootTupleWeight P.exponent F P.R n * ∏ i : Fin r, totientTwist (P.total.natDegree + 1) ↑(n i)) * ↑(weightedMass P.exponent n) ^ (κ / Real.log z) ≤ smoothTailUniformBound A B κ (P.total.natDegree + 1) P.badDiscriminant * ∑ m ∈ positiveUpTo z, P.weight F m

Coefficient-uniform smooth moment for the totient-modified weight.