summand_decomposition
The lemma states that for prime p and natural k the scaled prime cost equals half k times p plus half k over p minus k. Researchers decomposing costs over prime factorizations in additive arithmetic functions cite this per-summand identity. The proof unfolds primeCost into the J-cost formula, records positivity of p, and finishes by field simplification.
claimLet p be a prime natural number and k a natural number. Then k · J(p) = (1/2) k p + (1/2)(k / p) − k, where J(x) = (x + x^{-1})/2 − 1 is the Recognition Science cost function.
background
The module defines the prime cost spectrum by extending the real-valued J-cost to natural numbers via prime factorization. For n ≥ 1 one sets c(n) := Σ v_p(n) · J(p), making c completely additive: c(m n) = c(m) + c(n). The auxiliary primeCost p is simply J(p) viewed in ℝ and restricted to primes. J itself arises from the forcing chain as the unique solution to the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y).
proof idea
The tactic proof first unfolds primeCost and Jcost to expose the explicit formula J(p) = (p + 1/p)/2 − 1. It records that p > 0 and p ≠ 0 in ℝ by casting the primality hypothesis. Field_simp then cancels denominators and collects terms to obtain the target identity.
why it matters in Recognition Science
The identity supplies the algebraic step needed to pass from the per-prime definition of c to closed-form expressions for costSpectrumValue. It therefore supports the complete-additivity theorems costSpectrumValue_mul and costSpectrumValue_pow that follow in the same module. Within the broader framework it links the arithmetic cost spectrum directly to the J-cost fixed point of the T5–T6 forcing chain.
scope and limits
- Does not hold when the base is composite.
- Does not extend to real or negative k.
- Does not address the summed cost over multiple distinct primes.
- Does not claim positivity or monotonicity of the left-hand side.
formal statement (Lean)
245private lemma summand_decomposition (p k : ℕ) (hp : Nat.Prime p) :
246 (k : ℝ) * primeCost p =
247 (1/2) * ((k : ℝ) * (p : ℝ))
248 + (1/2) * ((k : ℝ) / (p : ℝ)) - (k : ℝ) := by
proof body
Tactic-mode proof.
249 unfold primeCost Jcost
250 have hp_pos : (0 : ℝ) < (p : ℝ) := by exact_mod_cast hp.pos
251 have hp_ne : (p : ℝ) ≠ 0 := ne_of_gt hp_pos
252 field_simp
253
254/-! ## Power formula and Omega bound -/
255
256/-- For any positive integer `n` and any natural `k`,
257 `c(n^k) = k · c(n)`. This is the complete-additivity of `c`
258 extended to repeated multiplication. -/