phiRung
plain-language theorem explainer
The phi-rung function r(n) for positive integers n is the completely additive extension of floor(log base phi of p) over the prime factorization of n. Number theorists and physicists building mass spectra or coherence energies cite it when decomposing integers onto the phi-ladder. The definition is a direct sum over Nat.factorization that multiplies each valuation by the prime rung.
Claim. For each positive integer $n$, the phi-rung index $r(n)$ equals $r(n) = sum_p v_p(n) floor(log_phi p)$, where the sum runs over primes p dividing n and $v_p(n)$ denotes the p-adic valuation.
background
In the Recognition Theta module the phi-rung index is defined as a completely additive arithmetic function on positive integers. It rests on phiRungPrime, which sets the value at each prime p to floor(log base phi of p). The module places this construction inside the candidate Recognition Theta function that augments the cost theta sum with the 8-tick character and phi-ladder weights to support a modular identity under t to 1/t.
proof idea
One-line definition that applies the sum operation to the prime factorization of n, scaling each exponent by the corresponding phiRungPrime value.
why it matters
This supplies the integer rung index consumed by RSNativeUnits for E_coh_rs = phiRung(-5), gap45 = phiRung(45), and the family of phiRung lemmas. It realizes the phi-ladder weight (T6) in the forcing chain and supplies the exponent in the mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)). The definition therefore anchors the arithmetic layer that feeds coherence scaling and the synchronization period before the modular-identity hypothesis is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.