fib4_eq_D
plain-language theorem explainer
The fourth Fibonacci number equals the spatial dimension D. Researchers tracing phi-ladder emergence and the eight-tick octave cite this when matching sequence values to D = 3. The proof evaluates the standard recurrence directly via the decide tactic on Nat.fib.
Claim. $F(4) = 3 = D$, where $F(n)$ denotes the Fibonacci sequence and $D$ is the spatial dimension fixed by the Recognition Science forcing chain.
background
The module shows the Fibonacci sequence arises intrinsically from the Recognition Science functional equation through the golden ratio phi, with the identity $F(n) phi + F(n-1) = phi^n$ and low-order values F(3) = 2, F(4) = 3, F(6) = 8 = 2^D. This declaration pins the case F(4) = 3 = D. The fib definition follows the recurrence with F(0) = 1, F(1) = 1, F(n+2) = F(n) + F(n+1), as given in Gap45.Derivation and aligned with RamanujanBridge variants.
proof idea
One-line wrapper that applies the decide tactic to reduce Nat.fib 4 = 3 via the standard recurrence definition.
why it matters
This anchors the fourth Fibonacci number to the spatial dimension D = 3 required by T8 in the forcing chain, where D emerges from the self-similar fixed point phi. It supports phi-ladder constructions and the eight-tick octave period 2^D = 8 at F(6). No downstream parents exist, so the result functions as a foundational identity rather than feeding a larger theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.