fib_4_eq
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.