pith. sign in
module module moderate

IndisputableMonolith.NumberTheory.CostTwistedLSeries

show as:
view Lean formalization →

This module defines the twisted prime cost and associated spectrum values by incorporating an arithmetic function chi into the base cost spectrum. Researchers extending Recognition Science to arithmetic L-series analogs would cite these definitions when twisting sums over primes. The module consists of direct definitions for twistedPrimeCost and spectrum variants together with elementary algebraic properties.

claimFor an arithmetic function $chi$ the twisted prime cost is $c_chi(p) := chi(p)cdot J(p)$ where $J$ is the Recognition cost function; the twisted cost spectrum value is the corresponding extension $c_chi(n) := sum_p v_p(n)cdot chi(p)cdot J(p)$ for $ngeq 1$.

background

The module sits in the NumberTheory domain and imports the Cost module together with PrimeCostSpectrum. The upstream PrimeCostSpectrum module extends the real-valued Recognition cost $J$ to a complete arithmetic function on natural numbers via prime factorization: for each $ngeq 1$ one defines $c(n) := sum_{p^kparallel n} kcdot J(p) = sum_p v_p(n)cdot J(p)$. The present module twists this construction by an arbitrary arithmetic function chi, producing twistedPrimeCost and the family of twistedCostSpectrumValue lemmas that handle the cases of units, primes, powers and products.

proof idea

This is a definition module, no proofs. It supplies direct definitions for twistedPrimeCost and twistedCostSpectrumValue together with one-line lemmas establishing the values on zero, one, primes, powers and products, plus the corresponding sum lemmas twistedPrimeCostSum.

why it matters in Recognition Science

The module supplies the twisted-cost primitives required to build L-series analogs inside the Recognition framework. It directly extends the Prime Cost Spectrum construction to allow character twists, thereby supporting later arithmetic developments that combine the J-cost ladder with multiplicative functions. No downstream uses are recorded in the current graph.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)