twistedPrimeCostSum
plain-language theorem explainer
The definition twistedPrimeCostSum introduces the partial sum Π_chi(N) over primes p ≤ N of J(p) chi(p), where J is the Recognition cost function. Number theorists extending the prime cost spectrum to Dirichlet characters would reference this when establishing properties of twisted L-series in the Recognition framework. The implementation directly encodes the sum using a range finset and a primality test, delegating the cost evaluation to the upstream primeCost definition.
Claim. Let $Π_χ(N) := ∑_{p ≤ N, p prime} J(p) χ(p)$, where $J$ is the J-cost function and $χ : ℕ → ℝ$ is an arithmetic function.
background
In the CostTwistedLSeries module the framework extends the prime cost spectrum to twisted settings using completely multiplicative functions chi. The primeCost definition isolates Jcost(p) for primes p, as primes form the irreducible basis for the ledger transactions. This sum Π_chi(x) is the prime-restricted partial sum that appears in the factorization of the Dirichlet series for the twisted cost function c_chi.
proof idea
This definition is a direct one-line construction that sums over the finset of natural numbers up to N, applying the primeCost multiplier only when the argument is prime via the conditional, and zero otherwise. It relies on the upstream primeCost and the standard Finset.sum operation.
why it matters
This definition supplies the twisted analogue of the prime cost partial sum, which is invoked by the sibling theorems twistedPrimeCostSum_zero and twistedPrimeCostSum_one_char to recover the untwisted case for the trivial character. It fills the role of Π_chi(x) in the module's development of cost-twisted L-functions, connecting to the Recognition framework's J-uniqueness (T5) and the phi-ladder structure for costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.