fib_6_eq
plain-language theorem explainer
The declaration states that the sixth Fibonacci number equals 8, which identifies the octave period 2^D with F_6 under the dimension constraint D=3. Researchers deriving the coherence energy exponent from the Fibonacci-phi framework would cite this to anchor the structural identity 8-3=5. The proof is a direct evaluation via native decision on the recursive definition of fib.
Claim. $F_6 = 8$, where $F_n$ denotes the Fibonacci sequence with $F_0=1$, $F_1=1$ and the recurrence $F_{n+2}=F_{n+1}+F_n$. This equates the octave period $2^D$ to the sixth Fibonacci number when $D=3$.
background
The Coherence Exponent module derives the exponent -5 from the requirement that both D and 2^D are Fibonacci numbers. The local Fibonacci definition is the recurrence fib 0 = 1, fib 1 = 1, fib (n+2) = fib n + fib (n+1). This matches the upstream fib definitions in Gap45.Derivation and the RamanujanBridge modules, which supply the sequence used for the dimension-forcing argument. The Identity definition from LogicAsFunctionalEquation supplies the zero-cost comparison baseline that underpins the entire Recognition functional equation.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the recursive Fibonacci definition directly at argument 6.
why it matters
This result feeds the parent theorems fibonacci_deficit (which extracts the identity 8-3=5) and octave_is_fib_6 (which equates the octave to F_6). It fills the Fibonacci-constraint step in the module's main theorem, confirming that the coherence energy E_coh = phi^{-5} follows from T8 dimension forcing and the eight-tick octave. The declaration closes the structural link between D=3 and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.