phi_pow_51_in_interval
plain-language theorem explainer
Golden ratio to the 51st power lies inside the closed rational interval with endpoints 45537548334 and 45537549354. Numerics and cosmology modules cite the bound when scaling the phi-ladder for mass and spectrum calculations. The tactic proof rewrites the base to goldenRatio, converts the real exponent to a natural number via rpow_natCast, then delegates to the pre-proven containment phi_pow51_in_interval_proven.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $phi^{51}$ belongs to the closed interval whose lower endpoint is the rational 45537548334 and upper endpoint is the rational 45537549354.
background
The module supplies interval arithmetic for the power function, preferring direct natural-number evaluation for precision over the general exp(log) route. An Interval is a structure with rational lo and hi fields together with a proof that lo ≤ hi. The predicate contains holds precisely when lo ≤ x ≤ hi for a real number x.
proof idea
The tactic proof first simplifies the contains predicate and the target interval. It rewrites the base (1 + sqrt 5)/2 to goldenRatio by reflexivity. It then converts the real power to the natural power goldenRatio^51 using Real.rpow_natCast. Finally it invokes the upstream theorem phi_pow51_in_interval_proven and transfers the containment by simplification.
why it matters
The result is invoked directly by phi_pow_140_in_interval in GalacticBounds to build higher phi-powers. It supplies a concrete numerical anchor for the phi-ladder used in mass formulas of the form yardstick * phi^(rung-8+gap(Z)). The bound closes a step inside the eight-tick octave numerics that supports T7 and the alpha band constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.