phi_pow54_eq
plain-language theorem explainer
The identity φ^54 = φ^51 ⋅ φ^3 holds for the golden ratio φ. Numerics researchers building interval estimates in Recognition Science cite this to chain bounds across high powers of φ. The proof is a one-line ring normalization that reduces the exponent equality via ring axioms.
Claim. $φ^{54} = φ^{51} ⋅ φ^3$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous algebraic bounds on φ by sandwiching √5 between 2.236 and 2.237 to obtain 1.618 < φ < 1.6185, with tighter decimal refinements. This theorem supplies the multiplicative exponent identity required to relate distant powers of φ. It depends on the and theorem from CirclePhaseLift, which supplies an explicit log-derivative bound M that becomes the angular Lipschitz constant on a circle of radius r.
proof idea
The proof applies the ring_nf tactic, which normalizes the power expression using ring axioms and the rule a^{m+n} = a^m ⋅ a^n to confirm the equality in one step.
why it matters
This equality is invoked by phi_pow54_gt and phi_pow54_lt to derive the concrete bounds 192894126000 < φ^54 < 192983018016. It serves as the algebraic stepping stone in the module's strategy for rigorous φ bounds, supporting phi-ladder mass formulas and the self-similar fixed-point role of φ in the Recognition Science forcing chain (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.