twistedCostSpectrumValue_one
plain-language theorem explainer
The theorem shows that the twisted cost spectrum value vanishes at the number one for any real-valued function chi. Number theorists building the elementary theory of twisted arithmetic functions in Recognition Science cite it as the zero base case inside the master certificate. The proof is a direct unfolding of the summation definition followed by simplification on the empty factorization of one.
Claim. For any function $chi : ℕ → ℝ$, the twisted cost spectrum value satisfies $c_chi(1) = 0$, where $c_chi(n) := ∑_{p^k ∥ n} k · J(p) · chi(p)$.
background
The CostTwistedLSeries module extends the prime cost spectrum to a character-twisted setting. For a function chi : ℕ → ℝ the twisted cost spectrum value is defined by summing, over the prime factorization of n, the term (valuation) times twistedPrimeCost chi p. The upstream definition twistedCostSpectrumValue realizes this as n.factorization.sum (fun p k => (k : ℝ) * twistedPrimeCost chi p). The module proves the basic algebraic properties of this function before relating it to associated L-series.
proof idea
The term-mode proof unfolds the definition of twistedCostSpectrumValue and invokes simp on the lemma Nat.factorization_one, which states that the prime factorization of 1 is empty and therefore contributes the zero sum.
why it matters
This result supplies clause (1) of the master certificate cost_twisted_certificate, which assembles the elementary identities of the twisted cost function. It fills the n = 1 base case required for the subsequent development of complete additivity and the relation to the partial sum Π_chi(x). Within the Recognition framework the identity supports the number-theoretic layer that ultimately connects the J-cost spectrum to the L-function factorization and the derivation of physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.