fibonacci_factor_coprime_with_8
plain-language theorem explainer
The declaration establishes that the Fibonacci factor 5 shares no common prime divisors with 8. Researchers deriving the 45-gap from the eight-tick structure cite it to confirm that the factorization 45 = 9 × 5 remains coprime and proceeds without adjustment. The proof reduces immediately by unfolding the definition of the Fibonacci factor.
Claim. $5$ denotes the Fibonacci factor (the fifth term in the sequence tied to the golden ratio). Then $gcd(5,8)=1$.
background
The module derives the 45-gap from the eight-tick octave (T8) and the Fibonacci sequence linked to φ. It states that 45 equals closure_factor times fibonacci_factor, where closure_factor is 9 (one full eight-tick cycle plus return) and fibonacci_factor is 5 (the smallest Fibonacci number greater than 1 that is coprime to 8). The physical motivation identifies 45 as the ninth triangular number T(9), representing cumulative phase accumulation over a closed 8-tick cycle with D=3 spatial dimensions.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the fibonacci_factor definition, reducing the gcd claim directly to the arithmetic fact that 5 and 8 share no common divisors.
why it matters
This result anchors the claim that 45 emerges from T8 combined with Fibonacci structure rather than appearing arbitrarily. It supports the further step that lcm(8,45)=360 forces D=3. The module connects the factorization to cumulative phase over closed cycles in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.