phi_pow_ge_one
plain-language theorem explainer
The lemma asserts that the golden ratio raised to any natural power meets or exceeds one. Researchers on phi-ladder stability and J-cost monotonicity in Recognition Science cite it to bound interaction costs from below. The proof proceeds by induction on the exponent, lifting the base case through multiplication by phi greater than one.
Claim. For every natural number $n$, $phi^n >= 1$, where $phi > 1$ is the golden ratio.
background
The phi-ladder stability module treats ladder positions as powers of phi for integer exponents. J-cost measures the interaction penalty between occupied rungs; adjacent rungs collapse under the golden recurrence phi^2 = phi + 1, while gaps of two minimize the cost. This lemma supplies the lower bound required for all subsequent monotonicity statements on the ladder.
proof idea
Induction on n. The zero case simplifies directly to the base inequality. The successor step rewrites 1 as 1 times 1, applies gcongr to reach 1 times phi^n, then multiplies by phi using gcongr and the upstream lemma one_lt_phi, finally rewriting the product to phi to the successor power.
why it matters
It is invoked by gapCost_mono and phi_pow_mono inside the module and by Jcost_phi_pow_strictMono in the GCIC LocalCacheForcing paper. The result closes the elementary inequality needed to prove that larger gaps carry strictly larger J-cost, which enforces the differ-by-at-least-two rule that recovers the Rogers-Ramanujan identities. It anchors the phi-ladder construction at the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.