FibonacciPhiCert
plain-language theorem explainer
Cross-domain modules invoke the FibonacciPhiCert structure to reduce any bound on a high power of the golden ratio to an arithmetic comparison of Fibonacci numbers. The structure collects the base identities φ² = φ + 1 through φ⁸ = 21φ + 13, the general recurrence φ^{n+2} = F_{n+2} φ + F_{n+1}, and the monotonicity of the Fibonacci sequence. It is defined by direct assembly of theorems already proved in Constants and the present module.
Claim. Let φ be the golden ratio. A FibonacciPhiCert is a record containing the identities φ² = φ + 1, φ³ = 2φ + 1, φ⁴ = 3φ + 2, φ⁵ = 5φ + 3, φ⁸ = 21φ + 13, the universal relation φ^{n+2} = F_{n+2} φ + F_{n+1} for all natural numbers n (with F the Fibonacci sequence), and the strict increase F_n < F_{n+1} for n ≥ 2.
background
The module CrossDomain.FibonacciPhiUniversality collects the Fibonacci-phi identities that reduce high powers of the golden ratio to linear expressions in φ itself. The defining relation is φ^n = F_n φ + F_{n-1}, where F is the Fibonacci sequence. This identity serves as the bridge that converts per-domain exponential bounds into statements about integer sequences. Upstream, the individual power identities are established by iterated application of the base equation φ² = φ + 1, as recorded in the theorems phi_cubed, phi_fourth, phi_fifth and phi_eighth. The universal form and the monotonicity of F are likewise already available in the module. The local setting is the cross-domain certificate that unifies these facts for use across astrophysics, gap derivations and Ramanujan-bridge arguments.
proof idea
The definition constructs the structure by supplying the fields phi_sq, phi_cubed, phi_fourth, phi_fifth, phi_eighth directly from the corresponding theorems in the module, together with the already-proved universal recurrence and fib_monotone statements.
why it matters
FibonacciPhiCert supplies the shared certificate that every cross-domain bound on powers of φ ultimately rests upon. It is instantiated by the definition fibonacciPhiCert and thereby supports the reduction of claims such as φ^8 > 46 or φ^{44} > 10^8 to arithmetic facts about Fibonacci numbers. Within the Recognition framework it realizes the concrete content of the phi-ladder fixed point by linking it to the integer sequence that appears in the mass formula and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.