fib7_eq_13
plain-language theorem explainer
The equality states that the seventh term of the Fibonacci sequence equals 13. Researchers verifying the phi-ladder steps or Zeckendorf representations in Recognition Science would cite it when checking low-order values against the eight-tick octave. The proof reduces to a direct computation via the decide tactic on the standard recurrence.
Claim. The seventh Fibonacci number satisfies $F_7 = 13$, where the sequence obeys the recurrence $F_n = F_{n-1} + F_{n-2}$ with $F_0 = 0$, $F_1 = 1$.
background
The module shows that the Fibonacci sequence arises intrinsically in Recognition Science through the golden ratio φ, with the identity $F(n)φ + F(n-1) = φ^n$ and concrete ties to physical constants: $F(3) = 2 = D$, $F(4) = 3 = D$, and $F(6) = 8 = 2^D$ (the ledger period). This declaration supplies the next term in that sequence. It rests on three imported definitions of the Fibonacci function: the inductive version in Gap45.Derivation (starting 1, 1, 2, ...), the standard version in ContinuedFractionPhi (starting 0, 1, 1, ...), and the alias to Nat.fib in ZeckendorfJCost.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the recursive definition of Nat.fib at argument 7.
why it matters
This equality fills the next slot in the initial Fibonacci segment required for the phi-ladder. It aligns with framework steps T6 (phi as self-similar fixed point) and T7 (eight-tick octave at period 8 = F(6)), preparing rungs where F(7) = 13 enters Zeckendorf J-cost calculations and the mass formula. No downstream theorem currently depends on it, yet it closes one of the canonical identities listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.