pith. machine review for the scientific record. sign in
def definition def or abbrev high

twistedCostSpectrumValue

show as:
view Lean formalization →

This definition assigns to each natural number n and real-valued arithmetic function chi the sum over primes p dividing n of the p-adic valuation times the twisted prime cost. Researchers formalizing twisted arithmetic functions or L-series within Recognition Science cite it as the base object for additivity proofs. The definition is realized directly as a factorization sum that applies the upstream twistedPrimeCost at each prime.

claimLet $chi : mathbb{N} to mathbb{R}$ be an arithmetic function and $n in mathbb{N}$. The twisted cost spectrum value is defined by $c_chi(n) := sum_{p^k || n} k cdot (primeCost(p) cdot chi(p))$, where the sum is over the distinct primes dividing $n$ and $v_p(n)$ is the $p$-adic valuation.

background

The CostTwistedLSeries module extends the prime cost spectrum to a character-twisted setting. For a completely multiplicative arithmetic function chi, the twisted cost is given by $c_chi(n) := sum_p v_p(n) cdot J(p) cdot chi(p)$, with the Dirichlet series of $c_chi$ intended to factor through the corresponding L-function. The upstream twistedPrimeCost supplies the local factor primeCost(p) multiplied by chi(p), where primeCost itself encodes the J-cost from the Recognition framework.

proof idea

The definition is a direct one-line unfolding: it applies the sum over the prime factorization of n, scaling each term by the twistedPrimeCost chi p.

why it matters in Recognition Science

This definition is the core object feeding the master certificate theorem that records zero at n=1 and complete additivity over products. It generalizes the untwisted costSpectrumValue and supplies the structural identities required for twisted L-series in Recognition Science. It sits inside the arithmetic layer built on the J-uniqueness and Recognition Composition Law, with the eight-tick octave and D=3 emerging from later steps in the forcing chain.

scope and limits

formal statement (Lean)

  45def twistedCostSpectrumValue (chi : ℕ → ℝ) (n : ℕ) : ℝ :=

proof body

Definition body.

  46  n.factorization.sum fun p k => (k : ℝ) * twistedPrimeCost chi p
  47

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.