The twists ℓ = 0 and ℓ = 1 in a conjecture on quartic Gauss sums, formalized in Lean

Conjecture 1.2 of C. David, A. Dunn, A. Hamieh and H. Lin (Quartic Gauss sums over primes and metaplectic theta functions, arXiv:2306.11875) predicts that the sums S_beta(X; l) of normalized quartic Gauss sums over primary primes of Z[i], weighted by the von Mangoldt function and twisted by (conj(c)/|c|)^l, have a main term b_beta X^(3/4) with b_beta nonzero when l = 0 and none when l is nonzero. Their identity (1.2), whose symbol factors evaluate to 1 at primary primes, gives g(c)^2 = -c/|c|. The twist by conj(c)/|c| is therefore a conjugation, and S_beta(X; 1) = -conj S_beta(X; 0) exactly. So the cases l = 0 and l = 1 of the conjecture are incompatible. More generally, S_beta(X; 1 - l) = -conj S_beta(X; l) for every l. The paper proves the inconsistency, both exactly and with an exceptional set of small weight. It also proves the corresponding identities for the twisted moments, and explains why the phenomenon is special to order four. It then states the corrected conjecture, in which l = 1 carries the main term -conj(b_beta) X^(3/4). This correction is the only main term at l = 1 compatible with the case l = 0, and the corrected conjecture is equivalent under the identity to its cases l <= 0. A remark explains the consequences for the generalization of the conjecture by David, Devin, Fazzari and Waxman (arXiv:2608.06286). All results except the evaluation of the identity are formalized in Lean 4 with Mathlib (QuarticPairing v1.1). The formal statements take the identity g(c)^2 = -kappa c/|c|, for a fixed unit kappa, as their only hypothesis on the Gauss sum, so no quartic residue symbol is needed. The evaluation for the quartic Gauss sum, with kappa = 1, is proved in the paper from DDHL (1.2) and is not formalized. A numerical check at 766 primary primes confirms the identities to about 1e-13. The mathematics is the author's. The Lean code and this paper were drafted with the assistance of Claude (Anthropic), and the Lean code is checked by the Lean kernel.