twistedCostSpectrumValue
plain-language theorem explainer
This definition assigns to each natural number n and real-valued arithmetic function chi the sum over primes p dividing n of the p-adic valuation times the twisted prime cost. Researchers formalizing twisted arithmetic functions or L-series within Recognition Science cite it as the base object for additivity proofs. The definition is realized directly as a factorization sum that applies the upstream twistedPrimeCost at each prime.
Claim. Let $chi : mathbb{N} to mathbb{R}$ be an arithmetic function and $n in mathbb{N}$. The twisted cost spectrum value is defined by $c_chi(n) := sum_{p^k || n} k cdot (primeCost(p) cdot chi(p))$, where the sum is over the distinct primes dividing $n$ and $v_p(n)$ is the $p$-adic valuation.
background
The CostTwistedLSeries module extends the prime cost spectrum to a character-twisted setting. For a completely multiplicative arithmetic function chi, the twisted cost is given by $c_chi(n) := sum_p v_p(n) cdot J(p) cdot chi(p)$, with the Dirichlet series of $c_chi$ intended to factor through the corresponding L-function. The upstream twistedPrimeCost supplies the local factor primeCost(p) multiplied by chi(p), where primeCost itself encodes the J-cost from the Recognition framework.
proof idea
The definition is a direct one-line unfolding: it applies the sum over the prime factorization of n, scaling each term by the twistedPrimeCost chi p.
why it matters
This definition is the core object feeding the master certificate theorem that records zero at n=1 and complete additivity over products. It generalizes the untwisted costSpectrumValue and supplies the structural identities required for twisted L-series in Recognition Science. It sits inside the arithmetic layer built on the J-uniqueness and Recognition Composition Law, with the eight-tick octave and D=3 emerging from later steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.