phiRung_prime
plain-language theorem explainer
For every prime p the completely additive phi-rung index r(p) equals the base value floor(log_phi p). Researchers building the Recognition Theta sum cite the equality to justify extending the phi-ladder from primes to all natural numbers via valuations. The proof is a one-line term reduction that substitutes the prime factorization into the sum definition and simplifies.
Claim. Let $p$ be a prime number. Then the phi-rung index $r(p)$ satisfies $r(p) = r_p(p)$, where $r_p(p) = floor(log_φ p)$.
background
The Recognition Theta module constructs a candidate completion of the cost theta function that incorporates the eight-tick character and phi-ladder weights so that it inherits a modular identity under t to 1/t. The phi-rung function r(n) is defined completely additively: for n ≥ 1 it equals the sum over the prime factorization of n of v_p(n) times the prime rung r_p(p). The prime rung itself is given by r_p(p) = floor(log_φ p), the integer height on the phi-ladder. Upstream, the definition of r(n) is the sum over Nat.factorization and r_p is the floor-log expression; the theorem simply confirms that these two agree when n is prime.
proof idea
The proof is a term-mode reduction. It unfolds the sum definition of phiRung, rewrites the factorization map using the hypothesis that p is prime (so the map is the singleton sending p to 1), and applies simp to obtain equality with phiRungPrime p.
why it matters
This supplies the base case that legitimizes the valuation formula for the phi-rung on all natural numbers. It feeds directly into the downstream theorem phiRung_prime_pow establishing the corresponding statement for prime powers. In the Recognition framework it furnishes the arithmetic starting point for the Recognition Theta sum whose modular identity is stated as Sub-conjecture A.2; the construction rests on the self-similar fixed point phi (T6) and the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.