phiRung_prime_pow
plain-language theorem explainer
The theorem states that the phi-rung index of a prime power equals k times the rung of the prime. Researchers building the Recognition Theta sum would cite it to decompose terms over prime factorizations. The proof is by induction on k, applying the multiplicative rung property at the successor step followed by integer arithmetic.
Claim. Let $p$ be prime and $k$ a nonnegative integer. Then the phi-rung index of $p^k$ equals $k$ times the phi-rung index of $p$.
background
The Recognition Theta function augments the cost theta sum with the 8-tick character and phi-ladder weights to support a modular identity under $t$ to $1/t$. The phi-rung index $r(n)$ is the completely additive function on natural numbers with $r(p)$ given by the floor of the base-phi logarithm for primes; the sibling theorem phiRung_mul supplies $r(mn)=r(m)+r(n)$ under the stated conditions, while phiRung_prime fixes the base value at primes. The local setting is the elementary arithmetic layer of the Recognition Theta module, which precedes the hypothesis structures for convergence and modularity.
proof idea
Proof by induction on $k$. The zero case reduces immediately by simplification. The successor step rewrites the power via the successor rule, invokes the multiplicative property phiRung_mul on the nonzero factors, substitutes the inductive hypothesis, inserts the prime case phiRung_prime, then applies casting and ring to equate the integers.
why it matters
The result extends the prime rung to arbitrary powers, enabling the full additive decomposition of the Recognition Theta sum over the natural numbers. It feeds the module's main theorems on term positivity and evaluation at one, and supports the hypothesis structures RecognitionThetaConvergence and RecognitionThetaModularIdentity. In the framework it supplies the discrete rung arithmetic required by the phi-ladder fixed point (T6) and the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.