phiRung

Recognition Science places scales on a discrete φ-ladder: successive rungs multiply by the golden ratio φ forced at T6 as the self-similar fixed point of the cost functional. The integer form in RS-native units is the forward map $n \mapsto \varphi^n$. The present definition is the continuous inverse: given a positive real scale, return its (possibly non-integer) rung coordinate.

This module stages honest targets for the Steve baryogenesis loop. The lead invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus sphaleron equilibration forces vanishing final baryon number. Scale ratios that enter washout exponents, freeze-out windows, and seesaw cutoffs are naturally written as φ-rungs once masses and temperatures sit on the ladder.

Upstream, Constants.phi is the same φ used for coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and the gap-45 synchronization rung. Mathlib supplies Real.logb.

Pure definitional abbreviation: expand to Mathlib Real.logb applied at base Constants.phi. No lemmas, no tactics, no sorry. Noncomputable only because real logarithm is noncomputable in Lean.

Gives the continuous rung coordinate used whenever a baryogenesis or mass-ladder argument must turn a ratio of scales into a φ-exponent. Downstream RS-native units package the dual integer map $\varphi^n$ and identities such as additivity and negation of rungs; coherence energy is the rung $-5$ instance, and gap-45 is the rung $45$ instance tied to the lcm$(8,45)=360$ synchronization period with the eight-tick octave (T7).

In the baryogenesis staging lane the definition keeps scale language honest: washout exponents, freeze-out windows, and the seesaw cutoff $\Lambda=f_\chi$ after EWSB can be stated as rung differences rather than ad-hoc logarithms. It does not itself prove any Sakharov condition; it is the unit conversion that later obstruction and relic-charge lemmas rely on when they compare ladder heights.