ratio_0_7_lt_phi_pow_142
plain-language theorem explainer
This theorem shows that 0.7 times the rational galactic ratio is strictly below the lower bound of the interval enclosure for phi to the 142. Researchers verifying numerical consistency of the phi-ladder against galactic timescales in Recognition Science numerics would cite it. The proof is a term-mode reduction that unfolds the successive positive interval multiplications for the phi powers and applies norm_num to the resulting rational comparison.
Claim. $ (7/10) r < l $ where $ r $ is the rational approximation to the galactic ratio $ tau^star / tau_0 $ and $ l $ is the lower endpoint of the interval enclosure for $ phi^{142} $ obtained by positive multiplications of lower-power phi intervals.
background
The module computes rational interval enclosures for high powers of phi to bound the galactic timescale ratio $ tau^star / tau_0 approx 5.75e29 $. An Interval is a structure with rational endpoints lo and hi satisfying lo <= hi. Positive interval multiplication mulPos(I, J, hI, hJ) returns the product interval whose lo is I.lo * J.lo and hi is I.hi * J.hi, given proofs that both lower bounds are positive. The galactic_ratio_rational is the concrete rational 41971608 * 10^24 / 73. The phi_pow_142_interval is assembled via mulPos from phi_pow_140_interval and phi_pow_2_interval; phi_pow_140_interval is itself mulPos of phi_pow_102_interval and phi_pow_38_interval, with phi_pow_102_interval defined as the square of phi_pow_51_interval.
proof idea
The proof is a term-mode script. It unfolds the definitions of phi_pow_142_interval, phi_pow_2_interval, 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 together with mulPos, Interval.add and Interval.point. norm_num then reduces the concrete rational inequality to a decidable numerical fact.
why it matters
This declaration supplies a verified numerical check confirming that the phi^142 lower bound exceeds 0.7 times the galactic ratio, supporting interval-based consistency arguments for the phi-ladder in Recognition Science. It rests on the interval primitives from Basic and the power-construction chain inside GalacticBounds. No downstream theorems are recorded, so the result functions as a standalone verification step rather than an intermediate lemma. It aligns with the framework's use of successive phi powers to bound physical ratios, consistent with the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.