phi_pow_140_lt_ratio
plain-language theorem explainer
φ^140 is strictly less than the rational galactic_ratio_rational that approximates the galactic-to-base timescale ratio at 5.75e29. Recognition Science numerics researchers cite the bound to fix the galactic rung N_galactic between 140 and 145. The tactic proof obtains containment of φ^140 inside a precomputed positive interval, then verifies the interval upper endpoint lies below the target rational by unfolding the mulPos constructions and applying norm_num.
Claim. $φ^{140} < r$ where $φ$ is the golden ratio and $r = 41971608 × 10^{24}/73$ is the rational approximation to the galactic timescale ratio τ★/τ₀.
background
The module supplies interval bounds on successive powers of the golden ratio φ to compare against the galactic ratio τ★/τ₀ ≈ 5.75e29, represented exactly by the rational galactic_ratio_rational := 41971608 * 10^24 / 73. Interval multiplication is performed by mulPos, which for positive intervals I and J returns the interval whose lo is I.lo * J.lo and hi is I.hi * J.hi. Upstream theorems construct phi_pow_140_interval as mulPos of phi_pow_102_interval and phi_pow_38_interval, with phi_pow_102_interval itself mulPos of two copies of phi_pow_51_interval; phi_pow_140_in_interval proves that φ^140 lies inside this interval.
proof idea
The tactic proof first obtains h_in_140 from phi_pow_140_in_interval. It then proves the upper endpoint of phi_pow_140_interval is less than galactic_ratio_rational by unfolding the chain of mulPos definitions for phi_pow_140_interval, phi_pow_102_interval, phi_pow_38_interval, phi_pow_37_interval, phi_pow_32_interval and the lower-power intervals, followed by norm_num. The final step applies lt_of_le_of_lt to the containment upper bound and the verified strict inequality, using exact_mod_cast to align the rational.
why it matters
The result is invoked in N_galactic_approx to conclude 140 < N_galactic < 145, which fixes the integer rung on the φ-ladder for galactic timescales. Within the Recognition framework this supplies a concrete numerical anchor for the mass formula yardstick * φ^(rung - 8 + gap(Z)) and supports the eight-tick octave structure (T7) that precedes the derivation of D = 3 (T8). It closes a verification gap between the J-uniqueness fixed point (T5) and the galactic ratio approximation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.