phi_pow_strictMono
plain-language theorem explainer
The lemma shows that powers of the golden ratio are strictly increasing on the natural numbers. Researchers proving J-cost growth along the phi-ladder in graph caching arguments cite it to compare costs at successive rungs. The proof is a direct one-line application of the library power monotonicity lemma once positivity of phi and one_lt_phi are supplied.
Claim. If $m,n$ are natural numbers with $m<n$, then $phi^m < phi^n$, where $phi$ is the golden ratio.
background
The Local Cache Forcing module proves that J-cost minimization on connected graphs forces hierarchical local caching, closing Gap G1. It relies on J being strictly increasing on [1,∞) and on the phi-ladder structure. The upstream lemma one_lt_phi (from Constants.lean, re-exported in PhiSupport) states 1 < phi and is proved via comparison of square roots: sqrt(1) < sqrt(5) and 2 < 1 + sqrt(5).
proof idea
The term proof first obtains 0 < phi from phi_pos, then applies the library lemma pow_lt_pow_right₀ directly to one_lt_phi and the hypothesis m < n.
why it matters
It is invoked by the downstream theorem Jcost_phi_pow_strictMono to obtain J(phi^m) < J(phi^n) for m < n, which contributes to the local_cache_forcing_certificate. This step supports the claim that collocated storage is cheaper than remote storage under the Recognition Composition Law and the self-similar fixed point property of phi (T6). It touches the question of how the eight-tick octave organizes cache hierarchies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.