phi_pow_bounded_by_fib
plain-language theorem explainer
The theorem shows that for every natural number n at least 2, phi to the power n is at most the nth Fibonacci number times phi plus the preceding Fibonacci number. Researchers converting the exact phi-Fibonacci recurrence into concrete numerical bounds for cosmology or biology applications would cite this corollary. The tactic proof rewrites the hypothesis 2 less than or equal to n as n equals k plus 2 and reduces the inequality to an equality supplied by the inductive identity.
Claim. For every natural number $n$ with $n$ at least 2, $phi^n$ is at most $F_n phi + F_{n-1}$, where $F_k$ denotes the $k$th Fibonacci number.
background
The module establishes the Fibonacci-phi identity as a cross-domain certificate. It records that any power satisfies the exact linear relation phi to the n equals F(n) times phi plus F(n minus 1), with the standard indexing F(0) equals 0 and F(1) equals 1. This identity is the mechanism that turns per-domain bounds such as phi to the 8 greater than 46 into arithmetic statements about the Fibonacci sequence together with the numerical bracket on phi itself.
proof idea
The tactic proof first applies Nat.exists_eq_add_of_le to the hypothesis 2 less than or equal to n, yielding n equals k plus 2. It then calls the inductive identity at k to obtain the exact equality phi to the (k plus 2) equals F(k plus 2) times phi plus F(k plus 1). Index arithmetic confirms that k plus 1 equals n minus 1, so the equality matches the target bound and le_of_eq finishes the argument.
why it matters
This corollary supplies the inequality version of the phi-Fibonacci identity for the C20 universality module. It supports the cross-domain certificate by converting the recurrence into a ready bound that per-domain modules can invoke directly. The module documentation notes that the same identity underlies the numerical claims for telomere halving and baryon asymmetry, connecting to the self-similar fixed-point property of phi in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.