pith. sign in
module module high

IndisputableMonolith.NumberTheory.PrimeCostSpectrum

show as:
view Lean formalization →

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

used by (3)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (22)