primeCost_pos
plain-language theorem explainer
The declaration establishes that the prime cost, obtained by evaluating the Recognition Science J-cost at any prime p, is strictly positive. Number theorists extending the cost spectrum to arithmetic functions cite it when proving non-negativity of composite costs built from prime quanta. The proof is a short tactic sequence that reduces the claim to the general positivity lemma for Jcost on positive reals distinct from one.
Claim. For every prime number $p$, $0 < J(p)$, where $J$ is the Recognition Science cost function and $p$ is embedded as a positive real.
background
The Prime Cost Spectrum module extends the J-cost from positive reals to natural numbers by defining the cost $c(n)$ of an integer $n$ as the sum over its prime factorization of $k · J(p)$ for each $p^k || n$. This yields a completely additive function. The auxiliary function primeCost extracts the value $J(p)$ for each prime $p$, providing the irreducible quanta of the spectrum. The key upstream result is the lemma Jcost_pos_of_ne_one, which states that $J(x) > 0$ for $x > 0$ and $x ≠ 1$, proved by rewriting $Jcost$ as a square and verifying positivity of the resulting numerator.
proof idea
The proof unfolds the definition of primeCost. It then obtains positivity of the real embedding of $p$ by casting the known positivity of primes, and shows that this embedding differs from 1 by using that every prime exceeds 1. The argument concludes by direct application of the lemma Jcost_pos_of_ne_one.
why it matters
This result forms part of the master certificate cost_spectrum_certificate that collects the elementary properties of the cost spectrum for the companion paper. It directly supports the non-negativity theorem costSpectrumValue_nonneg and the strict positivity theorem costSpectrumValue_pos for composite integers. In the Recognition framework it confirms that the irreducible cost quanta $J(p)$ remain positive, consistent with the forcing chain construction of positive costs for recognition events away from unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.