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