factorization_pow
plain-language theorem explainer
The theorem states that the prime factorization of a natural number raised to a power equals the exponent times the original factorization map. Number theorists building prime cost spectra or twisted L-series in Recognition Science cite it to scale exponents in J-cost calculations for powers. The proof is a one-line wrapper that invokes the matching Mathlib result on Nat.factorization.
Claim. For natural numbers $n$ and $k$, the prime factorization of $n^k$ satisfies $(n^k).factorization = k · n.factorization$, where the factorization is the Finsupp map sending each prime to its exponent.
background
The module supplies a thin, stable interface over Mathlib's Nat.factorization. It defines the local valuation vp(p, n) as the exponent of p in the prime factorization of n, written vp p n := n.factorization p. This supplies the reusable algebraic laws (vp_mul, vp_pow) needed for downstream work on squarefree numbers, Möbius inversion, and prime cost spectra. The local setting is a small collection of identities that keep all prime-exponent manipulations inside the Recognition Science number-theory layer without introducing new axioms.
proof idea
The proof is a one-line wrapper that applies the Mathlib theorem Nat.factorization_pow directly to the pair (n, k).
why it matters
This identity feeds the power rules for vp and the cost-spectrum theorems costSpectrumValue_pow and twistedCostSpectrumValue_pow, which reduce c(p^k) to k · J(p) and the corresponding twisted form. It supplies the algebraic step required to lift the basic vp definition to the phi-ladder mass formulas and the eight-tick octave structure in the Recognition framework. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.