phi_powers_unbounded
plain-language theorem explainer
The theorem shows that powers of the golden ratio exceed any prescribed real bound M. Researchers deriving computation limits in Recognition Science cite it to establish that φ-dependent costs become arbitrarily large at high rungs. The proof is a one-line term wrapper that instantiates the standard real-analysis fact on unbounded powers for bases strictly greater than one.
Claim. For every real number $M$, there exists a natural number $n$ such that $φ^n > M$, where $φ$ is the golden ratio satisfying $φ > 1$.
background
The module IC-002 derives fundamental computation limits from temporal discreteness (tick τ₀), irrationality of φ, and Landauer erasure costs. φ enters as the self-similar fixed point forced by the Recognition Composition Law and appears in J-cost and φ-ladder constructions. Upstream results supply one_lt_phi (1 < φ from the quadratic definition) together with structures for J-cost, ledger factorization, and spectral emergence that place φ-powers in cost and precision arguments.
proof idea
The proof is a term-mode one-liner. It calls pow_unbounded_of_one_lt on the bound M and the fact one_lt_phi, obtains the witness pair, and returns it directly as the existential.
why it matters
The result closes the irrationality leg of IC-002 by confirming unbounded φ-cost growth, which the downstream certificate ic002_certificate records as part of the derived limits summary. It aligns with the forcing chain where φ is fixed in T6 and enters mass and alpha-band formulas. The certificate lists this unboundedness alongside tick positivity and maximum rate bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.