pith. machine review for the scientific record. sign in
def definition def or abbrev high

primeCost

show as:
view Lean formalization →

primeCost isolates the J-cost of each prime as the irreducible basis for the Recognition Science cost spectrum on the naturals. Number theorists extending J to completely additive arithmetic functions cite this definition when constructing costSpectrumValue and its twisted variants in CostTwistedLSeries. The definition is realized as a direct cast of the input natural to a real followed by application of Jcost.

claimFor a natural number $p$, the prime cost is defined by $J(p)$, where $J$ is the Recognition Science cost function on the positive reals.

background

The Prime Cost Spectrum module extends the Recognition Science cost function $J$ from positive reals to a completely additive arithmetic function on the naturals. For $n ≥ 1$ the total cost is $c(n) := ∑_{p^k ‖ n} k · J(p)$, equivalently $∑_p v_p(n) · J(p)$, so that $c(m n) = c(m) + c(n)$ for all positive $m, n$. primeCost extracts the individual term $J(p)$ for each prime, supplying the spectrum's basis elements. This construction rests on the cost function defined in ObserverForcing.cost, which sets the cost of a recognition event to Jcost of its state, and on the derived cost in MultiplicativeRecognizerL4.cost.

proof idea

One-line definition that casts the natural number $p$ to a real and applies the Jcost function.

why it matters in Recognition Science

primeCost supplies the basis elements for costSpectrumValue and for the twisted constructions in CostTwistedLSeries, including twistedPrimeCost, twistedCostSpectrumValue_prime, and the master certificate cost_twisted_certificate. It realizes the framework's identification of primes as the ledger's irreducible transactions, whose costs form the spectrum out of which all integer costs are built, consistent with the multiplicative structure from the forcing chain and the Recognition Composition Law.

scope and limits

formal statement (Lean)

  55def primeCost (p : ℕ) : ℝ := Jcost (p : ℝ)

proof body

Definition body.

  56
  57/-- For any prime `p`, the prime cost is strictly positive. -/

used by (17)

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

depends on (6)

Lean names referenced from this declaration's body.