phi_pow32_lt
plain-language theorem explainer
The result shows that the golden ratio raised to the 32nd power lies strictly below 4,873,100. Researchers verifying numerical consistency of the phi-ladder mass formula in Recognition Science numerics would cite this when chaining bounds to exponent 43 for proton-mass checks. The proof reduces the 32nd power to the square of the 16th power via ring_nf, invokes the predecessor bound on phi^16, and closes the inequality with nlinarith and norm_num.
Claim. The golden ratio satisfies $phi^{32} < 4873100$.
background
The module supplies rigorous upper bounds on powers of the golden ratio phi = (1 + sqrt(5))/2 by lifting rational approximations to sqrt(5). It begins from the elementary inequalities 2.236^2 < 5 < 2.237^2, which immediately give 1.618 < phi < 1.6185, and then propagates these bounds to higher exponents through algebraic identities such as phi_pow16_eq.
proof idea
The tactic proof first rewrites phi^32 as (phi^16)^2 by ring_nf. It then applies the upstream theorem phi_pow16_lt to replace each factor by the constant 2207.5. Positivity of the power is recorded, after which a calc block uses nlinarith to bound the product by 2207.5 squared and finally norm_num to reach 4873100.
why it matters
This intermediate bound feeds directly into the downstream theorem phi_pow43_lt, which establishes phi^43 < 970320000 for proton-mass verification on the phi-ladder. Within the Recognition Science framework it supports numerical checks of the mass formula (yardstick times phi to a rung offset) and the eight-tick octave structure. The result is fully proved and closes no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.