twistedCostSpectrumValue_mul
The twisted cost spectrum value function is completely additive over multiplication of positive integers for any real-valued chi. Researchers deriving Euler products for character-twisted L-series in the Recognition framework would cite this to justify the Dirichlet series factorization. The proof is a term-mode reduction that unfolds the sum definition, substitutes the product factorization, and closes via Finsupp sum additivity with coefficient ring arithmetic.
claimLet $c_chi(k) := sum_p v_p(k) J(p) chi(p)$ denote the twisted cost spectrum value of $k$. For any function $chi : mathbb{N} to mathbb{R}$ and nonzero natural numbers $m,n$, one has $c_chi(m n) = c_chi(m) + c_chi(n)$.
background
The module defines twisted cost spectrum values for a real-valued function chi on the naturals, generalizing the untwisted prime cost spectrum. The definition expresses $c_chi(n)$ as the sum over prime exponents in the factorization: $sum_p v_p(n) times$ (twisted prime cost of p under chi), where the twisted prime cost incorporates the J-cost scaled by chi(p). Upstream, the cost in MultiplicativeRecognizerL4 is the derived cost of its comparator on positive ratios, while the cost in ObserverForcing is the J-cost of a recognition event state. The factorization_mul theorem states that the factorization of a product of nonzero naturals equals the sum of the individual factorizations.
proof idea
The term proof unfolds twistedCostSpectrumValue to expose the Finsupp sum over prime exponents. It rewrites the factorization of the product using factorization_mul, then applies Finsupp.sum_add_index' to split the sum. The first subgoal is discharged by simp; the second by push_cast followed by ring to match the scaled coefficients.
why it matters in Recognition Science
This supplies the complete additivity clause inside the master certificate cost_twisted_certificate that collects all elementary properties of the twisted cost function. It generalizes the untwisted additivity result and supports the module claim that the Dirichlet series of the twisted cost factorizes through the corresponding L-function. In the Recognition framework the property is required before passing to the eight-tick octave and the phi-ladder mass formulas derived from the forcing chain.
scope and limits
- Does not require chi to be multiplicative or a Dirichlet character.
- Does not apply when either factor is zero.
- Does not produce explicit numerical values or closed forms for specific chi.
- Does not address analytic continuation or convergence of the associated L-series.
- Does not invoke the J-uniqueness formula or the phi fixed-point construction.
formal statement (Lean)
78theorem twistedCostSpectrumValue_mul (chi : ℕ → ℝ) {m n : ℕ}
79 (hm : m ≠ 0) (hn : n ≠ 0) :
80 twistedCostSpectrumValue chi (m * n)
81 = twistedCostSpectrumValue chi m + twistedCostSpectrumValue chi n := by
proof body
Term-mode proof.
82 unfold twistedCostSpectrumValue
83 rw [Nat.factorization_mul hm hn]
84 rw [Finsupp.sum_add_index']
85 · intro p
86 simp
87 · intro p i j
88 push_cast
89 ring
90
91/-- For the trivial character `chi = 1`, the twisted cost spectrum value
92 reduces to the standard cost spectrum value. -/