phi_pow54_gt
plain-language theorem explainer
Lower bounds on high powers of the golden ratio are established for interval arithmetic in Recognition Science numerics. Researchers computing precise constants for mass ladders or inverse-power thresholds would cite this result. The proof rewrites the target as a product of two prior lower bounds and chains them via positivity and linear arithmetic to reach the stated constant.
Claim. $192894126000 < phi^{54}$, where $phi = (1 + sqrt(5))/2$.
background
The module supplies rigorous numerical bounds on powers of the golden ratio by propagating tight quadratic approximations to sqrt(5) through algebraic identities. Upstream lemmas establish the decomposition phi^54 = phi^51 * phi^3 together with the concrete lower bounds phi^51 > 45536856942 and phi^3 > 4.236; these rest on the base inequality phi > 1.618 obtained from 2.236 < sqrt(5) < 2.237. The local setting is interval arithmetic that avoids floating-point rounding while remaining inside the Recognition Science phi-ladder.
proof idea
The tactic proof rewrites the exponent via the equality phi^54 = phi^51 * phi^3. It invokes the two prior lower-bound theorems, adds positivity statements for both factors, and executes a calc block that first compares the numerical product 45536856942 * 4.236 against the target constant by norm_num, then lifts the inequality to the golden-ratio terms by two applications of nlinarith.
why it matters
This bound is invoked by the downstream results phi_neg54_lt, phi_pow58_gt and phi_pow70_gt to control negative and higher positive powers. It supplies one rung on the phi-ladder used for mass formulas and for placing constants inside the alpha band (137.030, 137.039). The step closes a segment of the T6 self-similar fixed-point construction by furnishing concrete numerical anchors for the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.