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

N_galactic

show as:
view Lean formalization →

N_galactic gives the phi-ladder rung count separating the fundamental RS tick from the galactic memory timescale. Galaxy dynamics modelers using Recognition Science to predict the acceleration scale a0 would cite this when calibrating the forcing chain. The definition is a direct application of the logarithm base phi to the ratio of the two timescales.

claim$N = log_φ(τ★ / τ₀)$ where τ★ is the galactic memory timescale in seconds and τ₀ is the fundamental RS tick in seconds.

background

The module GalacticTimescale sets tau_star_s to 133 million years converted to seconds and tau0_SI to the SI value 7.3e-15 seconds. Phi is the self-similar fixed point imported from PhiForcing. The definition extracts the continuous rung count on the phi-ladder between these two calibrated timescales.

proof idea

One-line definition that applies the change-of-base formula for logarithms to the ratio tau_star_s / tau0_SI.

why it matters in Recognition Science

N_galactic supplies the exact rung count used by the downstream theorem N_galactic_approx to establish the integer bounds 140 < N < 145. It also feeds galactic_status and the amplitude bounds in GravityParameters. This realizes the timescale constraint linking a0 and r0, consistent with the phi-forcing chain.

scope and limits

formal statement (Lean)

  27def N_galactic : ℝ := Real.log (tau_star_s / tau0_SI) / Real.log phi

proof body

Definition body.

  28
  29/-- **THEOREM: N_galactic Approximation** -/

used by (4)

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

depends on (3)

Lean names referenced from this declaration's body.