ratio_lt_phi_pow_145
plain-language theorem explainer
The rational approximation r to the galactic timescale ratio τ★/τ₀ satisfies r < φ^{145}. Researchers deriving the galactic step count N_galactic in Recognition Science numerics cite this bound to close the interval for the phi-ladder exponent. The tactic proof first unfolds the recursive mulPos interval definitions for φ^{145} and applies norm_num to place r below the lower endpoint, then chains the inequality via lt_of_lt_of_le after casting.
Claim. Let r be the rational 41971608 × 10^{24}/73 that approximates the galactic timescale ratio τ★/τ₀. Then r < φ^{145}, where φ denotes the golden ratio.
background
The module Numerics.Interval.GalacticBounds builds closed rational intervals for powers of φ via the mulPos operation on positive intervals. galactic_ratio_rational is defined as the specific fraction 41971608 * 10^24 / 73, which the module documentation states approximates τ★/τ₀ ≈ 5.75e29. Upstream results include phi_pow_145_in_interval, which places φ^{145} inside its interval, together with the recursive constructions phi_pow_140_interval := mulPos phi_pow_102_interval phi_pow_38_interval and the lower-power intervals down to phi_pow_5_interval.
proof idea
The proof invokes phi_pow_145_in_interval to obtain the containment for φ^{145}. It unfolds the full chain of interval definitions (phi_pow_145_interval through phi_pow_140_interval, phi_pow_102_interval, phi_pow_38_interval, phi_pow_37_interval, phi_pow_32_interval, phi_pow_51_interval, phi_pow_16_interval, phi_pow_5_interval) and mulPos, then applies norm_num to verify galactic_ratio_rational < phi_pow_145_interval.lo. The final step applies lt_of_lt_of_le after exact_mod_cast to reach the strict inequality.
why it matters
N_galactic_approx directly applies this bound to conclude 140 < N_galactic < 145. The result supplies the concrete numerical anchor needed for galactic timescale approximations inside the Recognition Science phi-ladder and eight-tick octave structure. It closes a gap in the forcing chain by converting the module's interval arithmetic into a usable strict inequality without requiring exact evaluation of φ^{145}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.