fib_values
plain-language theorem explainer
The theorem confirms the initial segment of the Fibonacci sequence under the local recursive definition fib 0 = 0, fib 1 = 1, fib n+2 = fib n+1 + fib n. Researchers examining continued-fraction convergents to the golden ratio within Recognition Science's J-cost framework would cite these base cases to initialize arguments on the phi-ladder. The proof reduces immediately by simplification against the defining equations of fib.
Claim. Let $f:ℕ→ℕ$ be defined by $f(0)=0$, $f(1)=1$, and $f(n+2)=f(n+1)+f(n)$ for $n≥0$. Then $f(0)=0∧f(1)=1∧f(2)=1∧f(3)=2∧f(4)=3∧f(5)=5∧f(6)=8∧f(7)=13∧f(8)=21$.
background
The ContinuedFractionPhi module develops the link between continued fractions and φ through sequential J-cost minimization. The local fib definition sets fib 0 = 0, fib 1 = 1 and applies the standard recurrence thereafter; this generates the convergents to the self-similar fixed point φ = 1 + 1/φ that minimizes J(x) = (x + x^{-1})/2 - 1. The module doc states that infinite nesting converges because J is strictly convex and φ is the unique positive attractor of the recursion x ↦ 1 + 1/x.
proof idea
The proof is a one-line wrapper that applies the recursive definition of fib via the simp tactic with the fib lemma, directly computing each listed value from the base cases and recurrence.
why it matters
This supplies the concrete initial values required by the fib_values theorem in CrossDomain.FibonacciPhiUniversality, which matches Fibonacci coefficients up to F(11). It anchors the self-similar fixed point property of φ (T6) and the continued-fraction realization of the Recognition Composition Law inside the forcing chain. The result closes a small explicitness gap for downstream inductive arguments on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.