twistedCostSpectrumValue_eq_neg
plain-language theorem explainer
Negating the arithmetic character chi negates the twisted cost spectrum value at every natural number n. Researchers building twisted L-functions from the prime cost spectrum in Recognition Science would cite this linearity property when verifying additivity and sign behavior. The proof is a direct term-mode reduction that unfolds the sum definitions, applies negation of a finite sum, and finishes with ring arithmetic on each term.
Claim. For any function $chi : ℕ → ℝ$ and natural number $n$, the twisted cost spectrum value satisfies $c_{-chi}(n) = -c_{chi}(n)$, where $c_{chi}(n) := ∑_p v_p(n) · J(p) · chi(p)$ and the sum runs over primes $p$.
background
The module develops twisted analogs of the prime cost spectrum. The twisted cost spectrum value is defined as the sum over primes of the p-adic valuation times the J-cost times the character value, extending the untwisted case from PrimeCostSpectrum. J itself is the cost function induced by multiplicative recognizers, calibrated via the structure of positive ratios and the Recognition Composition Law. Upstream results supply the J-cost as the derived cost of a comparator and the non-negativity of recognition-event costs.
proof idea
The proof unfolds twistedCostSpectrumValue and twistedPrimeCost into Finsupp sums, rewrites both sides, applies Finset.sum_neg_distrib to pull out the negation, then invokes Finset.sum_congr with the ring tactic to equate corresponding terms.
why it matters
The result supplies the sign-flip identity required by the master certificate theorem cost_twisted_certificate, which assembles the elementary properties (vanishing at 1, complete additivity) of the twisted arithmetic function. It completes the step from the untwisted prime cost sum Π(x) to its character-twisted version Π_chi(x), supporting the later claim that the Dirichlet series of the twisted cost factorizes through the corresponding L-function. The identity is consistent with the eight-tick octave and the multiplicative structure forced by J-uniqueness in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.