fib_mono
plain-language theorem explainer
Fibonacci numbers are non-decreasing for indices at least 1. This fact is invoked in the Recognition Science treatment of Zeckendorf representations as J-cost-stable decompositions on the phi-ladder. The proof is a one-line wrapper that applies the standard-library monotonicity result for the Fibonacci sequence.
Claim. Let $F_k$ denote the $k$-th Fibonacci number. For all natural numbers $m,n$ with $1leq mleq n$, one has $F_mleq F_n$.
background
The module treats Zeckendorf representations as J-cost-stable configurations on the phi-ladder. Fibonacci numbers occupy the discrete rungs $F_napprox phi^n/sqrt{5}$, and the non-consecutive (gap at least 2) condition prevents adjacent occupation that would collapse under the J functional equation. Upstream results supply the structure of J-cost and the phi-forcing that calibrates these positions.
proof idea
The proof is a one-line wrapper that applies the monotonicity of the Fibonacci sequence as recorded in Mathlib.
why it matters
This monotonicity supports the greedy algorithm for Zeckendorf representations, identified with J-cost gradient descent. It supplies the classical fact needed for the module claim that every positive integer admits a unique J-cost-stable representation on the phi-ladder. No downstream theorems are recorded; the result closes a supporting step in the Zeckendorf-J-cost identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.