twistedCostSpectrumValue_zero
plain-language theorem explainer
The theorem shows that the twisted cost spectrum value vanishes at zero for any real-valued function chi from naturals to reals. Researchers extending prime cost spectra to twisted arithmetic functions within Recognition Science would cite this as the zero base case. The proof is a direct unfolding of the definition followed by simplification with the empty prime factorization of zero.
Claim. For any function $chi: ℕ → ℝ$, the twisted cost spectrum value $c_chi(0) = 0$, where $c_chi(n) := ∑_p v_p(n) · J(p) · chi(p)$ and the sum runs over primes with multiplicity from the factorization of $n$.
background
This module generalizes the prime cost spectrum to a character-twisted setting. The twisted cost spectrum value is defined as the sum over primes of the valuation times J(p) times chi(p), where J is the uniqueness function from the forcing chain. Upstream, cost is the derived cost of a multiplicative recognizer's comparator on positive ratios, and separately the J-cost of a recognition event.
proof idea
The proof unfolds the definition of the twisted cost spectrum value and applies simplification using the fact that the prime factorization of zero is empty, which makes the sum identically zero.
why it matters
This supplies the zero base case for the twisted cost spectrum and its elementary properties such as complete additivity. It supports the module's goal of relating the twisted costs to L-functions in the Recognition Science framework, consistent with the J-uniqueness step and the eight-tick octave structure. No downstream applications are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.