fib_4_eq
The declaration establishes that the fourth Fibonacci number equals 3, anchoring the spatial dimension in the Recognition Science framework. Researchers deriving the coherence energy exponent from the Fibonacci constraint on dimension would cite this when showing that the difference between the sixth and fourth terms yields the exponent 5. The proof proceeds by native decision on the recursive definition.
claimThe fourth Fibonacci number satisfies $F_4 = 3$.
background
The Fibonacci sequence is defined recursively in upstream modules as fib 0 = 1, fib 1 = 1, fib (n+2) = fib n + fib (n+1), producing the terms 1, 1, 2, 3, 5, 8, .... The Coherence Exponent module uses this sequence to constrain dimension such that both D and 2^D must be Fibonacci numbers. The module doc states: 'This proves that E_coh = φ^{-5} is not a free parameter but is structurally determined by the Fibonacci-φ framework.'
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the Fibonacci recursion at argument 4.
why it matters in Recognition Science
This identity is invoked in D_is_fib_4 to conclude D equals the fourth Fibonacci number and in fibonacci_deficit to obtain the identity 8 - 3 = 5. It thereby supports the module's main theorem linking dimension forcing (T8) to the coherence exponent phi^{-5}. In the framework it anchors the eight-tick octave (T7) and the phi-ladder mass formulas.
scope and limits
- Does not derive the Fibonacci recurrence from first principles.
- Does not prove uniqueness of the dimension D = 3.
- Does not compute higher Fibonacci numbers or phi powers.
- Does not address J-uniqueness or the Recognition Composition Law.
Lean usage
rw [fib_4_eq]formal statement (Lean)
32theorem fib_4_eq : fib 4 = 3 := by native_decide
proof body
Term-mode proof.
33
34/-- F₅ = 5 (the coherence exponent) -/