tau_star_is_phi_rung
plain-language theorem explainer
The theorem shows that the galactic memory timescale τ★ lies within 10% of the φ-ladder rung at N=142, i.e., |τ★ − τ₀ φ^{142}| < 0.1 τ★. Astrophysicists working with Recognition Science galactic models cite it to anchor observed periods to the self-similar structure. The proof is a direct verification that selects N=142, equates the ratio τ★/τ₀ to a precomputed rational, invokes interval bounds on φ^{142}, and discharges the split absolute-value inequalities by linear arithmetic.
Claim. There exists an integer $N$ such that $|τ_★ - τ_0 φ^N| < 0.1 τ_★$, where $τ_★$ is the galactic memory timescale in seconds and $τ_0$ is the fundamental RS tick duration.
background
In the GalacticTimescale module, τ★ (tau_star_s) is defined as the characteristic galactic memory timescale, set to 133 million years converted to seconds. The auxiliary function phi_rung_time N returns τ₀_SI ⋅ φ^N, with τ₀_SI the SI-calibrated RS tick of 7.3 × 10^{-15} s. Upstream results supply the native tick τ₀ (from Constants and its Derivation) together with the interval lemma phi_pow_142_in_interval and the rational ratio galactic_ratio_rational from GalacticBounds.
proof idea
The proof selects N=142 explicitly. It unfolds phi_rung_time, computes the ratio τ★/τ₀ and confirms it equals galactic_ratio_rational by norm_num. It invokes phi_pow_142_in_interval to obtain bounds on φ^{142}. The absolute-value goal is rewritten via abs_lt; each side is transformed by division lemmas and discharged by linarith after casting the interval inequalities.
why it matters
This places the galactic memory timescale on the φ-ladder, connecting observed galactic periods to the self-similar fixed point φ forced at T6 of the UnifiedForcingChain and the eight-tick octave at T7. It supplies a concrete numerical check inside the Gravity domain that can feed later mass-ladder or Berry-threshold arguments, even though no downstream use is recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.