phi_pow_mono
plain-language theorem explainer
The lemma shows that natural-number powers of the golden ratio are non-decreasing: if j ≤ k then phi^j ≤ phi^k. Workers on phi-ladder stability in Recognition Science cite it when establishing monotonic growth of gap costs under the J-cost function. The tactic proof reduces the claim to multiplication by a power at least one after rewriting the difference k - j as a natural number d.
Claim. Let phi > 1 be the golden ratio. For all natural numbers j, k with j ≤ k, phi^j ≤ phi^k.
background
The phi-ladder places positions at phi^n for integer n. The module shows that Rogers-Ramanujan identities arise because the J-cost (defined from the Recognition Composition Law) forbids adjacent occupations: phi^n + phi^{n+1} collapses to phi^{n+2} by the golden recurrence. J-cost is positive for ratio phi and reaches its first minimum at ratio phi^2, enforcing gaps of at least 2. Upstream results include the fact that phi^d ≥ 1 for every natural d, which supplies the multiplier needed for the inequality.
proof idea
Case analysis via Nat.exists_eq_add_of_le rewrites k = j + d. Non-negativity of phi^j follows from pow_nonneg. Multiplication by the non-negative term phi^j then yields phi^j * 1 ≤ phi^j * phi^d once phi_pow_ge_one supplies phi^d ≥ 1. The final step rewrites the right-hand side as phi^{j+d} by the power-addition rule.
why it matters
The result feeds directly into gapCost_mono, which proves that larger gaps carry strictly larger J-cost and thereby closes the admissibility argument for the phi-ladder. It supplies the elementary monotonicity step required by the Recognition Science reading of Rogers-Ramanujan, where the eight-tick octave and self-similar fixed point of phi (T6) already fix the ladder geometry. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.