fib_strict_mono
plain-language theorem explainer
Strict monotonicity holds for the Fibonacci sequence at all indices n at least 2. Researchers deriving phi-power bounds across Recognition Science domains cite this to guarantee strict inequalities when reducing exponential expressions via Fibonacci coefficients. The argument is a direct one-line application of the standard library fact on successive Fibonacci numbers.
Claim. For every natural number $n$ with $n$ at least 2, the $n$-th Fibonacci number is strictly less than the $(n+1)$-th Fibonacci number, where the sequence satisfies $F_0=0$, $F_1=1$, and $F_k=F_{k-1}+F_{k-2}$ for $k$ at least 2.
background
The module collects the Fibonacci-phi identity that reduces any power of the golden ratio to a linear combination: phi to the n equals F(n) times phi plus F(n-1). This identity converts domain-specific bounds on phi powers into arithmetic statements about the integer sequence F. The local setting is the cross-domain certificate that assembles these facts with zero axioms or sorrys, supporting calculations such as phi^8 greater than 46 and phi^44 greater than 10^8.
proof idea
The proof is a one-line wrapper that applies the standard library lemma on strict increase of successive Fibonacci numbers to the hypothesis that n is at least 2.
why it matters
This result is invoked inside the fibonacciPhiCert definition to complete the universal set of phi-power identities. It supplies the strict growth needed for the corollary that bounds any phi^n by a linear expression in phi with Fibonacci coefficients. In the framework it anchors the phi fixed-point step and the phi-ladder used for mass formulas and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.