reciprocalPrimeSum
plain-language theorem explainer
The definition of reciprocalPrimeSum maps each natural number n to the real sum of k/p over its prime-power factors p^k. Number theorists extending the Recognition Science cost function to integers cite it when decomposing c(n) or analyzing additive arithmetic functions. The implementation is a direct one-line application of the factorization sum combinator.
Claim. For a natural number $n$ with prime factorization $n = 2^{k_2} 3^{k_3} 5^{k_5} 7^{k_7} 11^{k_{11}} 13^{k_{13}} 17^{k_{17}} 19^{k_{19}} 23^{k_{23}} 29^{k_{29}} 31^{k_{31}} 37^{k_{37}} 41^{k_{41}} 43^{k_{43}} 47^{k_{47}} 53^{k_{53}} 59^{k_{59}} 61^{k_{61}} 67^{k_{67}} 71^{k_{71}} 73^{k_{73}} 79^{k_{79}} 83^{k_{83}} 89^{k_{89}} 97^{k_{97}} 101^{k_{101}} 103^{k_{103}} 107^{k_{107}} 109^{k_{109}} 113^{k_{113}} 127^{k_{127}} 131^{k_{131}} 137^{k_{137}} 139^{k_{139}} 149^{k_{149}} 151^{k_{151}} 157^{k_{157}} 163^{k_{163}} 167^{k_{167}} 173^{k_{173}} 179^{k_{179}} 181^{k_{181}} 191^{k_{191}} 193^{k_{193}} 197^{k_{197}} 199^{k_{199}} 211^{k_{211}} 223^{k_{223}} 227^{k_{227}} 229^{k_{229}} 233^{k_{233}} 239^{k_{239}} 241^{k_{241}} 251^{k_{251}} 257^{k_{257}} 263^{k_{263}} 269^{k_{269}} 271^{k_{271}}
background
The Prime Cost Spectrum module extends the Recognition Science cost function J from positive reals to a completely additive arithmetic function c(n) on natural numbers. For n with prime factorization product p^k, c(n) equals sum k J(p). This makes c(m n) = c(m) + c(n) for all positive m, n. The reciprocalPrimeSum supplies the companion sum sum k/p that appears in per-summand identities decomposing contributions to c(n).
proof idea
One-line definition that applies the sum combinator directly to the factorization of n, sending each pair (p, k) to the real k / p.
why it matters
This definition supplies the reciprocal sum required for closed-form decompositions of the cost spectrum c(n) inside the Recognition Science framework. It supports the extension of J to arithmetic functions on naturals and connects to the prime cost quanta and the completely additive property. No parent theorems appear in the used-by graph, yet it underpins the module's main results on costSpectrumValue_mul and costSpectrumValue_nonneg. It touches the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.