phi_pow_strictMono
The lemma establishes that powers of the golden ratio phi are strictly increasing for natural number exponents. Researchers proving J-cost growth along the phi-ladder in graph caching arguments cite it to chain inequalities. The term proof first secures positivity of phi then applies the standard power monotonicity lemma for bases exceeding one.
claimFor the golden ratio $phi > 1$ and natural numbers $m < n$, $phi^m < phi^n$.
background
The module proves local cache forcing from J-cost minimization on connected graphs, showing that cost minimization forces hierarchical caching and closes Gap G1 in the brain holography argument. The golden ratio phi satisfies its defining equation and exceeds 1, as established by the upstream lemma one_lt_phi via comparison of square roots: Real.sqrt 1 < Real.sqrt 5 and algebraic rearrangement to 2 < 1 + Real.sqrt 5. J-cost is the recognition cost function shown strictly monotone on [1, infinity) in sibling results such as Jcost_strictMono_on_Ici_one.
proof idea
The term proof obtains 0 < phi from phi_pos, then applies pow_lt_pow_right₀ to one_lt_phi and the hypothesis m < n.
why it matters in Recognition Science
It is invoked directly by Jcost_phi_pow_strictMono to obtain J(phi^m) < J(phi^n) for m < n. That theorem feeds the local_cache_forcing_certificate, which demonstrates forced local caching. The result supports the phi-ladder structure in the Recognition Science forcing chain, where phi is the self-similar fixed point and powers index the mass formula.
scope and limits
- Does not extend the inequality to real exponents.
- Does not apply when the base is at most one.
- Does not supply explicit growth rates or bounds.
- Assumes the standard ordering on real numbers.
Lean usage
example {m n : ℕ} (hmn : m < n) : phi ^ m < phi ^ n := phi_pow_strictMono hmnformal statement (Lean)
65lemma phi_pow_strictMono {m n : ℕ} (hmn : m < n) : phi ^ m < phi ^ n := by
proof body
Term-mode proof.
66 have hphi_pos : 0 < phi := phi_pos
67 exact pow_lt_pow_right₀ one_lt_phi hmn
68
69/-- **J(φ^m) < J(φ^n) FOR m < n**. -/