module module high

`IndisputableMonolith.NumberTheory.PrimeCostSpectrum`

This module isolates the cost of each prime p as J(p) using the recognition cost function. Researchers extending the ledger to twisted L-series or prime phase distributions cite it as the basis for irreducible transaction costs. It is a definition module whose content consists of the primeCost definition together with immediate nonnegativity and monotonicity properties.

claimFor each prime $p$, the prime cost equals $J(p)$ where $J(x) = (x + x^{-1})/2 - 1$. The resulting values form the basis of the cost spectrum.

background

The module imports the J-cost definition from IndisputableMonolith.Cost and the ledger interpretation from IndisputableMonolith.NumberTheory.PrimeLedgerStructure. The latter states that primes are the irreducible transactions in the discrete multiplicative ledger and that the fundamental theorem of arithmetic supplies the balance sheet. J itself satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the prime cost spectrum that CostTwistedLSeries generalizes to character-twisted arithmetic functions and that PrimePhaseDistribution and RecognitionTheta rely upon for the 8-tick character and phi-ladder weights. It directly implements the isolation of irreducible costs described in its own doc-comment.

scope and limits

Does not prove any distribution or density statements about the costs.
Does not incorporate the eight-tick octave or spatial dimension D=3.
Does not treat composite numbers or the full cost spectrum.
Does not connect costs to physical constants such as alpha or G.

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