phi_pow58_eq
plain-language theorem explainer
The algebraic identity φ^58 = φ^54 ⋅ φ^4 holds by the exponent addition rule. Numerics code in Recognition Science cites it to split high-power bounds into products of lower-power estimates such as those on φ^54 and φ^4. The proof is a one-line algebraic reduction via ring normalization.
Claim. $φ^{58} = φ^{54} ⋅ φ^{4}$
background
The module supplies rigorous bounds on the golden ratio φ = (1 + √5)/2 by establishing tight inequalities such as 1.618 < φ < 1.6185 and then refining them with more decimal places. It relies on algebraic properties of φ and the fact that φ satisfies φ² = φ + 1. This theorem records the elementary power rule φ^{m+n} = φ^m ⋅ φ^n for the specific exponents 58, 54 and 4.
proof idea
The proof is a one-line wrapper that applies the ring_nf tactic to reduce the equality to a trivial identity under the ring axioms.
why it matters
This equality is invoked by the companion theorems phi_pow58_gt and phi_pow58_lt to convert separate bounds on φ^54 and φ^4 into a bound on φ^58. It fills the algebraic step needed to obtain the numerical interval 1.3219e12 < φ^58 < 1.324e12, which supports the phi-ladder mass formulas and the eight-tick octave structure in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.