N_galactic_approx
plain-language theorem explainer
Galactic dynamics models in Recognition Science rely on the rung number N_galactic = log_φ(τ★/τ₀) for the memory timescale. This theorem shows 140 < N_galactic < 145, confirming the integer approximation 142 used in acceleration derivations. The proof substitutes the explicit ratio τ★/τ₀, converts the bounds via log properties, and applies pre-established inequalities on powers of phi.
Claim. $140 < N < 145$ where $N = log_φ(τ★/τ₀)$, τ★ is the galactic memory timescale in seconds, and τ₀ is the fundamental RS tick.
background
The module defines τ★ as the characteristic galactic memory timescale (133 million years in SI units) and τ₀ as the base RS tick 7.3e-15 s. N_galactic is the base-φ logarithm of their ratio: N = log(τ★/τ₀) / log φ. Upstream lemma one_lt_phi supplies 1 < φ so that log φ is positive. Bounds phi_pow_140_lt_ratio and ratio_lt_phi_pow_145 from GalacticBounds supply the concrete power comparisons needed for the log inequalities.
proof idea
The tactic proof first equates the ratio to its rational value by unfolding and norm_num. It obtains 0 < log φ from one_lt_phi. The lower bound rewrites via lt_div_iff₀ and log_rpow, reducing to log(ratio) > log(φ^140) which is discharged by phi_pow_140_lt_ratio. The upper bound applies div_lt_iff₀ and reduces to log(ratio) < log(φ^145) using ratio_lt_phi_pow_145.
why it matters
This result justifies the integer rung 142 adopted in GravityParameters.N_galactic for deriving the galactic acceleration scale from r₀. It closes the approximation step on the φ-ladder for galactic memory, consistent with the eight-tick octave. The bound is tight enough to support the integer claim without further scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.