fib_values
The fib_values theorem records the explicit values of the first eleven Fibonacci numbers under the standard Nat.fib definition. Cross-domain proofs in Recognition Science cite these base cases when reducing powers of phi via the identity phi^n = F(n) phi + F(n-1). The proof is a single term that applies reflexivity to each of the eleven conjuncts.
claimLet $F_n$ denote the $n$th Fibonacci number with $F_1 = 1$, $F_2 = 1$, and $F_n = F_{n-1} + F_{n-2}$ for $n > 2$. Then $F_1 = 1$, $F_2 = 1$, $F_3 = 2$, $F_4 = 3$, $F_5 = 5$, $F_6 = 8$, $F_7 = 13$, $F_8 = 21$, $F_9 = 34$, $F_{10} = 55$, and $F_{11} = 89$.
background
The Fibonacci-Phi Identity Universality module states that any power of the golden ratio satisfies phi^n = F(n) phi + F(n-1), where F is the Fibonacci sequence. This identity reduces bounds on high powers of phi, such as those used for telomere halving or baryon asymmetry, to arithmetic facts about the coefficients F(n) and F(n-1). The module supplies these base values as a cross-domain certificate, drawing on the fib definitions from Gap45.Derivation and RamanujanBridge.ContinuedFractionPhi together with identity events from ObserverForcing and VantageCategory.
proof idea
The proof is a term-mode one-liner that constructs the eleven-fold conjunction by applying reflexivity to each equality after the definition of Nat.fib is unfolded.
why it matters in Recognition Science
This supplies the concrete base cases required by the universal Fibonacci-phi identity in the C20 wave of the Recognition framework. It is referenced by the fib_values theorem in RamanujanBridge.ContinuedFractionPhi, which supports continued-fraction and Zeckendorf representations tied to J-cost. Within the larger structure the values anchor the phi-ladder used for mass formulas and the eight-tick octave.
scope and limits
- Does not establish the general Binet closed form.
- Does not prove the Fibonacci recurrence relation.
- Does not extend the explicit values past the eleventh term.
- Does not address generalizations to Lucas numbers or other sequences.
formal statement (Lean)
44theorem fib_values :
45 Nat.fib 1 = 1 ∧ Nat.fib 2 = 1 ∧ Nat.fib 3 = 2 ∧ Nat.fib 4 = 3 ∧
46 Nat.fib 5 = 5 ∧ Nat.fib 6 = 8 ∧ Nat.fib 7 = 13 ∧ Nat.fib 8 = 21 ∧
47 Nat.fib 9 = 34 ∧ Nat.fib 10 = 55 ∧ Nat.fib 11 = 89 := by
proof body
Term-mode proof.
48 refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
49
50/-- Universal Fibonacci-phi identity by induction. -/