twistedCostSpectrumValue_prime
plain-language theorem explainer
The declaration shows that the twisted cost spectrum value at a prime p equals the prime cost at p times the character chi evaluated at p. Number theorists extending the prime cost spectrum to twisted arithmetic functions for L-series constructions in Recognition Science would cite this reduction step. The proof is a direct term-mode wrapper that unfolds the spectrum and prime-cost definitions, applies the prime factorization rewrite, and simplifies the resulting Finsupp sum.
Claim. Let $p$ be prime and let $c_chi$ denote the twisted cost spectrum value for a completely multiplicative function $chi : ℕ → ℝ$. Then $c_chi(p) = J(p) · chi(p)$, where $J$ is the cost function induced by the multiplicative recognizer.
background
The module CostTwistedLSeries generalizes the prime cost spectrum to the character-twisted setting. For each completely multiplicative arithmetic function chi : ℕ → ℝ the twisted cost spectrum value is defined by $c_chi(n) := Σ_p v_p(n) · J(p) · chi(p)$, where the sum runs over the prime factors of n. This construction rests on the cost function from MultiplicativeRecognizerL4 (the derived cost of its comparator on positive ratios) and from ObserverForcing (the J-cost of a recognition event).
proof idea
The proof unfolds twistedCostSpectrumValue and twistedPrimeCost, rewrites via Nat.Prime.factorization hp, and simplifies the single-index Finsupp sum with simp.
why it matters
The result supplies the prime case needed by the downstream master certificate cost_twisted_certificate, which assembles the elementary properties of the twisted cost function. It completes the structural identities required before the Dirichlet-series factorization (a paper-level claim left unformalized here) and sits inside the T5 J-uniqueness and multiplicative composition steps of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.