phi_powers_unbounded
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not supply an explicit growth rate or minimal n for given M.
- Does not address rational approximations to φ-powers.
- Does not derive concrete operation counts or energy bounds.
- Does not engage quantum or thermodynamic limits beyond the irrationality remark.
formal statement (Lean)
172theorem phi_powers_unbounded (M : ℝ) : ∃ n : ℕ, phi ^ n > M := by
proof body
Term-mode proof.
173 obtain ⟨n, hn⟩ := pow_unbounded_of_one_lt M one_lt_phi
174 exact ⟨n, hn⟩
175
176/-! ## Summary: Computation Limits from RS -/
177
178/-- Summary of computation limits derived in RS. -/