phi_pow_ge_one
phi^n is bounded below by one for every natural number n. Researchers on phi-ladder stability and J-cost monotonicity cite this to anchor cost comparisons along the hierarchy. The proof proceeds by induction on n, rewriting the successor case as a product and applying mul_le_mul with the inductive hypothesis together with one_lt_phi.
claimFor every natural number $n$, the golden ratio satisfies $1 ≤ φ^n$.
background
The module proves local cache forcing from J-cost minimization on connected graphs, closing Gap G1 in the brain holography argument. J-cost is the function J(x) = (x + x^{-1})/2 - 1, strictly increasing on [1, ∞). phi is the golden ratio, the self-similar fixed point of the Recognition Composition Law with phi > 1. This lemma supplies the base inequality 1 ≤ phi^n required for all subsequent monotonicity statements on the phi-ladder. It depends directly on one_lt_phi, which states 1 < phi and is established in Constants by comparing the quadratic root to 1.
proof idea
Proof by induction on n. The zero case reduces to phi^0 = 1 by simp. In the successor case, rewrite phi^(k+1) = phi^k * phi via pow_succ, then compare 1*1 to phi^k * phi by mul_le_mul applied to the inductive hypothesis phi^k ≥ 1 and le_of_lt one_lt_phi, with nonnegativity and positivity side conditions.
why it matters in Recognition Science
This bound is invoked in gapCost_mono to prove that larger gaps carry strictly higher J-cost, and in Jcost_phi_pow_strictMono to obtain J(phi^m) < J(phi^n) for m < n. It therefore supports the main local_cache_forcing_certificate by ensuring costs increase with distance on the phi-ladder. In the Recognition framework it underpins T6 (phi as self-similar fixed point) and the eight-tick octave structure used for hierarchical caching.
scope and limits
- Does not address real or negative exponents.
- Does not quantify the rate of growth of phi^n.
- Assumes the standard definition of phi as the golden ratio >1.
- Limited to the natural-number phi-ladder; does not treat continuous extensions.
Lean usage
have hj1 : 1 ≤ phi ^ j := phi_pow_ge_one jformal statement (Lean)
54lemma phi_pow_ge_one (n : ℕ) : 1 ≤ phi ^ n := by
proof body
Tactic-mode proof.
55 induction n with
56 | zero => simp
57 | succ k ih =>
58 have : phi ^ (k + 1) = phi ^ k * phi := pow_succ phi k
59 rw [this]
60 calc 1 = 1 * 1 := by ring
61 _ ≤ phi ^ k * phi := by
62 exact mul_le_mul ih (le_of_lt one_lt_phi) (by norm_num) (by positivity)
63
64/-- φ^m < φ^n when m < n. -/