pith. sign in
module module moderate

IndisputableMonolith.NumberTheory.CostTwistedLSeries

show as:
view Lean formalization →

This module defines the cost of a prime p twisted by an arithmetic function chi and extends the prime cost spectrum to twisted multiplicative functions on naturals. Researchers extending Recognition Science arithmetic to characters and L-series constructions would cite these definitions when incorporating twisting into cost calculations. The module consists of a collection of definitions for the twisted prime cost together with its values at units, primes, powers, and products, plus basic sum lemmas.

claimFor an arithmetic function $\chi$ the twisted prime cost is $\tilde{c}(p,\chi):=\chi(p)J(p)$. The associated twisted spectrum value on $n$ is the multiplicative extension $\sum_{p^k\Vert n}k\,\tilde{c}(p,\chi)$, satisfying the usual rules at 1, at primes, under powers, and under coprime multiplication.

background

The module imports the cost function J from IndisputableMonolith.Cost and the prime cost spectrum from IndisputableMonolith.NumberTheory.PrimeCostSpectrum. The upstream module states that for each $n\ge1$ one defines $c(n):=\sum_{p^k\Vert n}k,J(p)=\sum_p v_p(n)J(p)$. The present module twists this construction by an arithmetic function chi, replacing each local factor J(p) by a chi-twisted version while preserving multiplicativity.

No new theoretical setting is introduced beyond the prime-factorization definition of cost already given in PrimeCostSpectrum; the module simply equips that definition with a character twist to support later L-series work.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the arithmetic-function layer needed to build twisted L-series from the Recognition Science cost function. They feed any future parent results on twisted prime-cost sums or character-twisted spectra that appear in the NumberTheory section. The construction directly continues the prime-factorization approach quoted in the upstream PrimeCostSpectrum doc-comment.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)