phi_powers_unbounded
plain-language theorem explainer
Powers of the golden ratio φ grow without bound above any real threshold M. Researchers on RS computation limits cite the result to show that φ-based costs become arbitrarily large at high rung numbers. The proof is a one-line wrapper applying the library lemma pow_unbounded_of_one_lt to the established fact that φ > 1.
Claim. For every real number $M$, there exists a natural number $n$ such that $φ^n > M$.
background
The module IC-002 derives computation limits from Recognition Science, listing temporal discreteness of the tick, irrationality of φ, Landauer erasure costs, and the Bremermann bound. φ enters as the self-similar fixed point forced by the J-uniqueness relation in the T0–T8 chain. The theorem sits among sibling results on tick atomicity and maximal computation rate.
proof idea
The proof is a one-line wrapper that applies pow_unbounded_of_one_lt to M and one_lt_phi, then packages the resulting witness pair.
why it matters
The declaration supplies IC-002.15 inside the computation-limits structure and is referenced by the status certificate ic002_certificate. It sharpens the claim that exact simulation of RS dynamics at high rungs is impossible with finite rational resources because φ-powers are unbounded. The result rests on the upstream lemma one_lt_phi and the irrationality facts established in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.