phi_rung_complexity_unbounded
plain-language theorem explainer
The declaration shows that powers of the golden ratio phi grow without bound. Researchers classifying the computational complexity of Recognition Science models cite it to place high-rung state computation in EXPTIME. The proof is a one-line term application of the standard lemma establishing unboundedness of a^n for a > 1.
Claim. For any real number $M$, there exists a natural number $n$ such that $phi^n > M$.
background
The module Information.PhysicsComplexityStructure locates physics in the complexity zoo by analyzing J-cost minimization. J-cost is the function J(x) = (x + x^{-1})/2 - 1, which is strictly convex with unique minimum at x = 1. Local 8-tick dynamics are O(1) per step, ground-state verification is linear time, and the phi-hierarchy places high-rung states in EXPTIME because phi^n grows without bound.
proof idea
The proof is a term-mode one-liner that applies the lemma pow_unbounded_of_one_lt to the bound M together with the fact one_lt_phi that 1 < phi.
why it matters
This is THEOREM IC-005.15. It directly supports the module's complexity summary that phi-rung computation is EXPTIME, linking the phi-ladder in mass formulas to exponential resource requirements. It sits inside the forcing chain where phi is the self-similar fixed point (T6) and supplies the growth fact needed for the EXPTIME classification of high-rung RS states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.