twistedCostSpectrumValue_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume chi is completely multiplicative or a Dirichlet character.
- Does not address convergence of the associated Dirichlet series.
- Does not derive any relation to the untwisted prime cost spectrum.
- Does not treat analytic continuation or functional equations.
formal statement (Lean)
48@[simp]
49theorem twistedCostSpectrumValue_one (chi : ℕ → ℝ) :
50 twistedCostSpectrumValue chi 1 = 0 := by
proof body
Term-mode proof.
51 unfold twistedCostSpectrumValue
52 simp [Nat.factorization_one]
53