pith. machine review for the scientific record. sign in
def definition def or abbrev high

phi_rung_time

show as:
view Lean formalization →

phi_rung_time defines the timescale at rung N on the Recognition Science phi-ladder as tau0_SI multiplied by phi to the power N. Galactic dynamics researchers cite it when mapping observed periods such as stellar or rotation timescales to discrete phi-tiers. The definition is a direct algebraic scaling that inherits its SI calibration from the imported base tick tau0_SI.

claim$τ_N = τ_0 ⋅ φ^N$, where $τ_0$ is the fundamental Recognition Science tick in seconds.

background

In the GalacticTimescale module timescales sit on a phi-ladder whose successive rungs differ by exact factors of the golden ratio φ. The base value tau0_SI supplies the SI calibration at rung zero. Upstream results from PhiForcingDerived establish the convexity of the J-cost that forces self-similar scaling, while SpectralEmergence fixes the three spatial dimensions and eight-tick octave that underwrite the discrete ladder.

proof idea

The definition is a one-line wrapper that multiplies the imported constant tau0_SI by phi raised to the rung index N.

why it matters in Recognition Science

This definition supplies the explicit rung function used by the downstream theorem tau_star_is_phi_rung, which places the galactic characteristic time tau_star_s at rung 142. It thereby embeds galactic timescales inside the T7 eight-tick octave and the phi-forcing chain of the Recognition Science framework.

scope and limits

formal statement (Lean)

  24def phi_rung_time (N : ℝ) : ℝ := tau0_SI * phi ^ N

proof body

Definition body.

  25
  26/-- The log-base-φ of the timescale ratio: N = log_φ(τ★/τ₀) -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.