fib_recurrence_at_6
plain-language theorem explainer
The theorem confirms the Fibonacci recurrence holds at index 6, establishing F6 equals F5 plus F4. Researchers deriving the coherence energy exponent in Recognition Science cite this identity when linking D equals 3 to the exponent minus 5 via the octave relation. The proof is a direct algebraic reduction that substitutes the precomputed values for fib 4, fib 5, and fib 6.
Claim. $F_6 = F_5 + F_4$, where the Fibonacci sequence is defined by $F_0 = 1$, $F_1 = 1$, and $F_{n+2} = F_{n+1} + F_n$ for $ngeq 0$.
background
Recognition Science derives the coherence energy exponent from the requirement that both the spatial dimension D and the octave 2^D are Fibonacci numbers. The sequence is defined by fib(0) equals 1, fib(1) equals 1, and fib(n+2) equals fib(n+1) plus fib(n). Prior results in the module establish fib(4) equals 3 (corresponding to D), fib(5) equals 5, and fib(6) equals 8 (corresponding to 2^D).
proof idea
The proof is a one-line wrapper that applies the rewrite tactic to substitute the pre-proved equalities fib_4_eq, fib_5_eq, and fib_6_eq into the target statement.
why it matters
This identity closes the arithmetic step in the derivation of the coherence energy E_coh equals phi to the minus 5 from the Fibonacci constraint on dimension. It supports the main theorem that the exponent is structurally fixed by D equals F4 and 2^D equals F6. The result aligns with the eight-tick octave in the forcing chain and the selection of D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.