Quartic Gauss sums over primes with a fixed numerator

David, Dunn, Hamieh and Lin proved that the normalized quartic Gauss sums g̃₄(c) at primes c ≡ β (mod 4) of Z[i], twisted by (c/|c|)^ℓ, sum to O(X^{5/6+ε}). We show that their argument gives the same bound, up to a factor (1 + |ℓ|)^{3/2}, for g̃₄(ν, c) with any fixed nonzero numerator ν. The only new ingredient is a local identity at the primes dividing ν. It splits off a prime π | ν from the coprimality condition of the Type I Dirichlet series: g₄(μ, π^k c′) = (−1)^{C(c′, π^k)} g₄(μ, π^k) g₄(μ π^{2k}, c′), with no condition linking μ and π. On the series prime to π the valuation of the numerator reduces modulo 4. Each of the four residual cases then closes up, either into a single equation with a determinant bounded away from zero on Re s ≥ 1, or into the coupled pair of DDHL (8.6) and (8.7). As a consequence the sharp sums are o(X) for every fixed numerator. This is the hypothesis on fixed numerators (Hypothesis P) used in Paper VIII of this series. The local identity and its use at every valuation of ν are formalized in Lean 4 with Mathlib (FixedNumerator, doi:10.5281/zenodo.23882652). The analytic inputs of DDHL are cited. Version 1.1 adds Remark 2.4. It writes out the splitting for the series prime to γ at every valuation e (for e ≥ 4 it has terms at k = 4j ≤ e as well as k = e + 1) and explains why Corollary 2.3 does not need it. The abstract and the formalization paragraph are updated to FixedNumerator v1.1. The results are unchanged.