fibonacciPhiCert
plain-language theorem explainer
The fibonacciPhiCert definition assembles the explicit phi-power identities up to exponent 8 together with the universal Fibonacci recurrence and monotonicity into one record structure. Cross-domain modules in cosmology and astrophysics cite it to invoke the full phi-ladder bounds without repeating individual lemmas. The construction is a direct record literal that references the pre-proved sibling definitions for each field.
Claim. Define the certificate $C$ by the equalities $phi^2 = phi + 1$, $phi^3 = 2 phi + 1$, $phi^4 = 3 phi + 2$, $phi^5 = 5 phi + 3$, $phi^8 = 21 phi + 13$, the universal relation $phi^{n+2} = F_{n+2} phi + F_{n+1}$ for every natural number $n$ (with $F_k$ the $k$th Fibonacci number), and the strict monotonicity $F_n < F_{n+1}$ whenever $n geq 2$.
background
The module states the Fibonacci-phi identity that reduces every integer power of the golden ratio to a linear combination of phi and 1 using Fibonacci coefficients: $phi^n = F(n) phi + F(n-1)$. This identity supplies the arithmetic engine behind per-domain bounds such as $phi^8 > 46$ for telomere halving and $phi^{44} > 10^8$ for baryon asymmetry. The certificate collects the low-order cases already proved in Constants together with the general recurrence phi_pow_fib and the monotonicity result fib_strict_mono.
proof idea
The definition is a one-line record constructor that populates each field of the FibonacciPhiCert structure by direct reference to the corresponding sibling: phi_sq supplies the square case, phi_cubed the cube case, and likewise for the fourth, fifth and eighth powers; the universal field is taken from phi_pow_fib and the monotonicity field from fib_strict_mono.
why it matters
This definition supplies the single cross-domain certificate for the Fibonacci-phi universality (C20) described in the module header, allowing any later proof to import the complete set of identities at once. It rests on the upstream phi_pow_fib theorem that establishes the general recurrence and on the explicit power lemmas already verified in Constants. No open questions are flagged, but the certificate remains available for future extensions to higher powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.