fib_5_eq
The declaration fixes the fifth Fibonacci number at 5 and identifies it as the coherence exponent in the Recognition Science mass ladder. Researchers deriving the phi-ladder spectrum or the coherence energy E_coh = phi^{-5} would cite this result to anchor the exponent. The proof is a direct evaluation of the recursive Fibonacci definition via native decision procedure.
claim$F_5 = 5$, where the Fibonacci sequence satisfies $F_0 = 1$, $F_1 = 1$, and $F_{n+2} = F_n + F_{n+1}$.
background
The module derives the coherence energy exponent from the Fibonacci constraint on spatial dimension D. The Fibonacci sequence is defined recursively as fib 0 = 1, fib 1 = 1, fib (n+2) = fib n + fib (n+1). The octave is defined locally as 2^D, which equals 8 when D = 3. Upstream results supply the octave definition from Constants as 8 * tick and the fib definition from Gap45.Derivation.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the Fibonacci recurrence directly at index 5.
why it matters in Recognition Science
This result feeds the parent theorems coherence_exponent_is_fib_5 and fibonacci_deficit, which establish that the coherence exponent equals F_5 and that F_6 - F_4 = F_5. It fills the chain step showing E_coh = phi^{-5} is determined by the Fibonacci-phi framework, linking to T8 dimension forcing where D = 3 and the eight-tick octave.
scope and limits
- Does not establish the value of the spatial dimension D.
- Does not derive the golden ratio connection to the Fibonacci sequence.
- Does not compute the coherence energy itself.
Lean usage
rw [fib_5_eq]formal statement (Lean)
35theorem fib_5_eq : fib 5 = 5 := by native_decide
proof body
Term-mode proof.
36
37/-- F₆ = 8 (the octave = 2^D) -/