sopfr
plain-language theorem explainer
sopfr(n) sums the prime factors of n counted with multiplicity, yielding the integer Σ k p over the prime-power factorization. Number theorists extending the Recognition Science J-cost to completely additive functions on ℕ would cite this definition when constructing the cost spectrum c(n). The implementation is a direct summation over the standard factorization map.
Claim. The sum-of-prime-factors-with-multiplicity function on natural numbers is given by $sopfr(n) := ∑_{p^k ‖ n} k · p$, where the sum runs over the prime powers in the factorization of $n$.
background
The Prime Cost Spectrum module extends the Recognition Science cost function J from positive reals to arithmetic functions on ℕ. For each n ≥ 1 the cost is defined by c(n) := Σ_{p^k ‖ n} k · J(p), making c completely additive so that c(m n) = c(m) + c(n). The cost spectrum is the set of irreducible quanta {J(p) : p prime}.
proof idea
The definition is a direct one-line wrapper that applies the Nat.factorization map and sums k * p for each prime p with exponent k.
why it matters
sopfr supplies the multiplicity-weighted integer sum that underlies costSpectrumValue and the completely additive cost function c(n) in this module. It feeds the downstream omega definition for distinct prime counting. This aligns with the framework extension of J to arithmetic functions, enabling reformulations of Chebyshev θ and ψ in cost terms and supporting the Recognition Composition Law on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.