fib_coprime_4_5
plain-language theorem explainer
Consecutive terms in the Fibonacci sequence with F_0=1, F_1=1 and the standard recurrence are coprime. This instance for the fourth and fifth terms supplies the coprimality needed to factor 45 as 9 times 5 in the eight-tick derivation. The proof is a direct computational verification that evaluates the concrete values.
Claim. Let $F_n$ be the sequence defined by $F_0=1$, $F_1=1$, $F_{n+2}=F_n+F_{n+1}$. Then $F_4=5$, $F_5=8$ and $gcd(5,8)=1$.
background
The local Fibonacci definition is the recurrence $F_0=1$, $F_1=1$, $F_{n+2}=F_n+F_{n+1}$. The module derives the 45-gap from the eight-tick structure (T8) by writing 45 as the product of the closure factor 9 and the Fibonacci factor 5, noting that 5 is the smallest Fibonacci number greater than 1 that is coprime to 8. Upstream results supply the same recurrence in three other modules, confirming the sequence values used here.
proof idea
One-line wrapper that applies the decide tactic to compute the gcd on the concrete integers obtained from the recurrence.
why it matters
The result closes the algebraic step that isolates the Fibonacci factor 5 in the identity 45=(8+1)×5, which the module links to the triangular number T(9) and the cumulative phase over one eight-tick cycle. It therefore feeds the claim that lcm(8,45)=360 forces D=3. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.