phiLadderRung
plain-language theorem explainer
The phi-ladder rung assigns to each integer n the time scale tau0 multiplied by phi to the power of negative n. Researchers deriving discrete quantum gravity scales from Recognition Science principles cite this when connecting the base tick duration to the Planck regime at n approximately 34. The definition is a direct one-line expression relying on the imported constants tau0 and phi.
Claim. The time scale at rung $n$ of the $phi$-ladder is given by $tau_n = tau_0 phi^{-n}$.
background
In Recognition Science the fundamental time unit is the tick duration $tau_0$, defined as the base interval in RS-native units from the Constants module. The golden ratio $phi$ arises as the self-similar fixed point from the forcing chain in PhiForcing. The phi-ladder then generates a hierarchy of scales by successive multiplication by $phi^{-1}$, reaching the Planck time at rung 34 as stated in the declaration comment.
proof idea
This is a direct definition that multiplies the base tick tau0 by the appropriate power of phi. It applies the imported definitions of tau0 from Constants and phi from PhiForcing without further reduction or lemmas.
why it matters
This definition supplies the scale hierarchy used by sibling declarations such as planckTime and lengthHierarchy to express Planck quantities in terms of the base tick. It fills the QG-009 target of deriving Planck scale from phi, linking to the eight-tick octave (T7) and the self-similar fixed point (T6) in the forcing chain. It touches the open mapping from discrete rungs to continuous Planck regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.