phiRungPrime
plain-language theorem explainer
The prime case of the phi-rung index is the floor of the base-phi logarithm. Researchers extending the rung function to all naturals cite this when establishing additivity for the Recognition Theta sum. The body is a direct one-line definition using the floor function on the log ratio.
Claim. $ r(p) = ⌊ log_φ p ⌋ $ for a prime number $ p $.
background
The Recognition Theta module constructs a candidate completion of the cost theta function incorporating the 8-tick character (T7) and phi-ladder weight (T6) to inherit a modular identity under t ↦ 1/t. The phi-rung index r(n) is defined completely additively for n ≥ 1 as the sum over primes of v_p(n) times the prime rung value, with the prime case given here. The module states: 'phiRung n : the phi-rung index r(n), completely additive with r(p) = ⌊log_φ p⌋ for primes.'
proof idea
Direct definition: the body evaluates Int.floor of the ratio of real logarithms with base phi.
why it matters
This base case supplies the prime values for the phiRung definition and feeds the theorems phiRung_prime, phiRung_mul, and phiRung_prime_pow. It realizes the phi-ladder weight (T6) inside the Recognition Theta construction, which targets a modular identity. The downstream results establish the complete additivity required for the theta sum terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.