twistedCostSpectrumValue_prime
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove analytic continuation or functional equations for the associated L-series.
- Does not treat non-prime positive integers.
- Does not extend the statement to complex-valued characters.
- Does not derive the full Euler-product factorization of the twisted Dirichlet series.
formal statement (Lean)
61theorem twistedCostSpectrumValue_prime (chi : ℕ → ℝ) {p : ℕ}
62 (hp : Nat.Prime p) :
63 twistedCostSpectrumValue chi p = primeCost p * chi p := by
proof body
Term-mode proof.
64 unfold twistedCostSpectrumValue twistedPrimeCost
65 rw [Nat.Prime.factorization hp]
66 simp [Finsupp.sum_single_index]
67
68/-- For a prime power `p^k`, the twisted cost is `k · J(p) · chi(p)`. -/