twistedCostSpectrumValue_pow
plain-language theorem explainer
twistedCostSpectrumValue_pow establishes that the twisted cost spectrum value at a prime power p^k equals k times the prime cost of p multiplied by chi(p). Number theorists extending prime cost spectra to twisted Dirichlet series cite this identity when decomposing Euler factors. The term-mode proof unfolds the spectrum and prime-cost definitions, applies the prime-power factorization rewrite, and simplifies the single-term Finsupp sum.
Claim. Let $p$ be prime and $k$ a natural number. Then the twisted cost spectrum value $c_chi(p^k)$ equals $k$ times the prime cost of $p$ times $chi(p)$, where $c_chi(n) := sum_p v_p(n) J(p) chi(p)$ and $J$ is the cost function on primes.
background
The module CostTwistedLSeries generalizes the prime cost spectrum from PrimeCostSpectrum to a character-twisted setting. For a completely multiplicative chi : ℕ → ℝ the twisted cost spectrum value is defined as the sum over primes of the p-adic valuation times J(p) times chi(p). This rests on the cost function from MultiplicativeRecognizerL4, where cost is the derived cost of the comparator on positive ratios, and from ObserverForcing, where cost of a recognition event is its J-cost.
proof idea
The proof unfolds twistedCostSpectrumValue and twistedPrimeCost to expose the Finsupp sum over the prime factorization. It rewrites via Nat.Prime.factorization_pow hp to obtain the single-term factorization with multiplicity k at p, then applies simp with Finsupp.sum_single_index to collapse the sum to the stated scalar multiple.
why it matters
This lemma feeds the master certificate cost_twisted_certificate that collects the elementary properties of the twisted cost function. It supplies the prime-power case needed for the Dirichlet series of c_chi to factor through the corresponding L-function, consistent with the Recognition Composition Law and the multiplicative structure of the recognizer framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.