OAI/NumberTheory/CubicMoment/Estimates/PublishedKummerPrime.lean

The finite cubic prime input including the ramified part.

Thorner–Zaman, Algebra & Number Theory 13 (2019), Theorem 1.4, specialized to the Kummer extension Q(ω, ∛v)/Q(ω). For v not a cube this is cyclic of order three; weighting its three Frobenius classes by the cubic character cancels the principal and possible real exceptional terms. The conductor divides the modulus 9v supplied by cubic reciprocity (Dunn–Radziwiłł 2024, §2, supplementary laws). Thus Nv bounded by a fixed log power suffices. This is the same published finite-order prime input as PublishedHecke, with units and primes above three retained, not a Gauss-sum conclusion. Smooth weights, exclusions and convolution estimates are derived below.