Reciprocal ninth-moment payment at the actual AP level

Only the explicitly named unweighted actual AP mass is an input to the last theorem. The arbitrary-coefficient envelope and the divisor moment are proved inputs, not extra analytic hypotheses.

theorem Wu2004MeanValue.wu_weighted_sq_le_envelope : ∃ (C₉ : ℝ), 0 < C₉ ∧ ∀ (x X : ℝ) (Q : ℕ) (E : ℕ → ℝ), 2 ≤ x → ↑Q ≤ x → 0 ≤ X → (∀ d ∈ Finset.Icc 1 Q, 0 ≤ E d) → (∀ d ∈ Finset.Icc 1 Q, ↑d * E d ≤ X) → (∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * E d) ^ 2 ≤ C₉ * Real.log x ^ 9 * (X * ∑ d ∈ Finset.Icc 1 Q, E d)

One fixed divisor-moment constant works for every nonnegative error sequence with the stated elementary modulus envelope.

theorem Wu2004MeanValue.actualAP_weighted_sq_le_unweighted : ∃ (C₉ : ℝ), 0 < C₉ ∧ ∀ (x F K : ℝ) (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (b : ℕ → ℕ), 2 ≤ x → 0 ≤ F → 0 ≤ K → ↑Q ≤ √x → (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) → (∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * actualAPError S f r d (b d)) ^ 2 ≤ C₉ * Real.log x ^ 9 * (apEnvelopeConstant F K * MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant * x * (1 + Real.log x) ^ 2 * ∑ d ∈ Finset.Icc 1 Q, actualAPError S f r d (b d))

Actual arbitrary bounded coefficients and one common profile, with the residue selected by the modulus but never by the source coordinate.

theorem Wu2004MeanValue.actualAP_weighted_log_saving_of_unweighted (A F K U : ℝ) (hF : 0 ≤ F) (hK : 0 ≤ K) (hU : 0 ≤ U) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ) (Q : ℕ) (S : Finset ℕ) (f r : ℕ → ℝ) (b : ℕ → ℕ), Real.exp 1 ≤ x → ↑Q ≤ √x → (∀ m ∈ S, 1 ≤ m ∧ ↑m ≤ √x) → (∀ m ∈ S, |f m| ≤ F) → (∀ m ∈ S, 2 ≤ r m ∧ ↑m * r m ≤ K * x) → ∑ d ∈ Finset.Icc 1 Q, actualAPError S f r d (b d) ≤ U * x / Real.log x ^ (2 * A + 11) → ∑ d ∈ Finset.Icc 1 Q, wuModulusWeight d * actualAPError S f r d (b d) ≤ C * x / Real.log x ^ A

Explicit arbitrary-saving transfer. An unweighted saving 2*A+11 pays Wu's exact mu² 3^omega weight. The constant is selected before the scale, cutoff, common coefficient/profile and modulus-selected residue. The only estimate assumed is the genuine unweighted actual AP sum.