module module high

`IndisputableMonolith.NumberTheory.PrimeCostSpectrum`

The PrimeCostSpectrum module isolates J-cost on primes as the basis for the recognition cost spectrum. Researchers extending the multiplicative ledger to twisted L-series or phase distributions cite these objects. It supplies the core definitions together with their monotonicity and non-negativity properties.

claimLet $J(x) = \frac{x + x^{-1}}{2} - 1$. For each prime $p$ the prime cost equals $J(p)$. The cost spectrum value at a natural number $n$ is the $J$-cost of its prime-power factors, with the spectrum non-negative and strictly increasing on primes.

background

Recognition Science treats the natural numbers as a multiplicative ledger whose irreducible entries are the primes (PrimeLedgerStructure). The J-cost function, imported from the Cost module, assigns to each ledger entry its recognition cost via the functional equation that yields $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. This module extracts the prime costs and assembles them into the spectrum function costSpectrumValue together with its elementary properties.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the prime cost spectrum that CostTwistedLSeries generalizes to characters, that PrimePhaseDistribution instantiates for the Erdős-Straus square-budget search, and that RecognitionTheta folds into the candidate modular theta function. It therefore anchors the arithmetic foundation for the T5 J-uniqueness and T7 eight-tick steps in the forcing chain.

scope and limits

Does not derive prime densities or the prime number theorem.
Does not treat composite numbers beyond their prime factorization.
Does not link costs to physical constants such as alpha or G.
Does not prove completeness or uniqueness of the spectrum.

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