module module high

`IndisputableMonolith.NumberTheory.PrimeCostSpectrum`

This module isolates the cost of each prime as the J-function evaluated at that prime, treating primes as the irreducible transactions in the multiplicative ledger. Researchers building cost-twisted L-series or prime phase distributions cite it as the foundation for the spectrum. The module supplies definitions for primeCost and costSpectrumValue together with their immediate nonnegativity and monotonicity properties.

claimFor prime $p$, define prime cost $c(p) := J(p)$ where $J(x) = (x + x^{-1})/2 - 1$. The cost spectrum value at $n$ is the sum of $c(p_i)$ over the prime factorization of $n$, with $c(1) = 0$.

background

The J-cost function originates in the Cost module as the unique function satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). PrimeLedgerStructure establishes primes as the generators of the natural numbers under multiplication, per the fundamental theorem of arithmetic. This module extracts the restriction of J to primes to form the basis of the cost spectrum.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the prime cost spectrum that CostTwistedLSeries generalizes to characters and that PrimePhaseDistribution and RecognitionTheta rely on for their constructions. The module fills the step from the J-uniqueness (T5) to the spectrum basis in the forcing chain.

scope and limits

Does not establish uniqueness of the J function.
Does not compute explicit numerical values for large primes.
Does not address the eight-tick octave or spatial dimensions.
Does not prove any global distribution theorems over all primes.

used by (3)

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

IndisputableMonolith.NumberTheory.CostTwistedLSeries module_import
IndisputableMonolith.NumberTheory.PrimePhaseDistribution module_import
IndisputableMonolith.NumberTheory.RecognitionTheta module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.NumberTheory.PrimeLedgerStructure module_import

declarations in this module (22)

def primeCost L55
theorem primeCost_pos L58
theorem primeCost_nonneg L69
lemma jcost_strictMono_on_one_le L83
theorem primeCost_strictMono L118
def costSpectrumValue L132
theorem costSpectrumValue_one L135
theorem costSpectrumValue_zero L140
theorem costSpectrumValue_prime L146
theorem costSpectrumValue_pow L153
theorem costSpectrumValue_mul L162
theorem costSpectrumValue_nonneg L175
theorem costSpectrumValue_le_mul L189
theorem costSpectrumValue_pos L196
def Omega L230
def omega L233
def sopfr L236
def reciprocalPrimeSum L239
lemma summand_decomposition L245
theorem costSpectrumValue_pow_general L259
theorem costSpectrumValue_le_omega_mul_jcost L273
theorem cost_spectrum_certificate L318