summand_decomposition
plain-language theorem explainer
The lemma gives the per-prime-power identity that lets each term k · J(p) in the cost spectrum c(n) be rewritten as half the product kp plus half the quotient k/p minus k. Workers deriving closed forms for the arithmetic cost function or reformulating prime-counting sums in Recognition Science would invoke this identity. The proof is a short tactic sequence that unfolds the definitions of primeCost and Jcost, records that p is positive and nonzero over the reals, and finishes with field_simp.
Claim. Let p be prime and k a positive integer. Then k · J(p) = (k p)/2 + (k)/(2p) - k, where J(x) = (x + x^{-1})/2 - 1 is the Recognition Science cost function on the positive reals.
background
The Prime Cost Spectrum module extends the real-valued J-cost to a completely additive arithmetic function c on the naturals by setting c(n) = Σ v_p(n) · J(p), where the sum runs over the distinct primes in the factorization of n. The auxiliary definition primeCost p simply casts J(p) into ℝ for prime arguments, while costSpectrumValue n assembles the full sum via Nat.factorization. This local setting lets classical prime-counting functions be re-expressed directly in terms of the cost spectrum {J(p)}.
proof idea
The tactic proof first unfolds primeCost and Jcost to expose the explicit algebraic form of J(p). It then adds the two auxiliary facts that p viewed in ℝ is positive (via exact_mod_cast from hp.pos) and nonzero (via ne_of_gt). The final field_simp step cancels denominators and collects terms to reach the target identity.
why it matters
The identity supplies the algebraic step needed to obtain the closed-form decomposition referenced in the module documentation and thereby supports the surrounding theorems on costSpectrumValue_pow and costSpectrumValue_mul. It rests on the explicit J-uniqueness (T5) and the phi-forcing structures that fix the functional equation for J, allowing the cost spectrum to serve as the irreducible quanta for every integer cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.