gap_coprime_with_8
plain-language theorem explainer
The theorem shows that the gap number 45 shares no common prime factors with the eight-tick period 8. Workers on the Recognition Science derivation of spatial dimensions would cite this to confirm that the gap remains independent of the base period when forming the least common multiple. The proof reduces the claim by unfolding the definitions of gap, closure_factor, and fibonacci_factor, then applies a decision procedure to the resulting concrete equality.
Claim. $45 = (8 + 1) × 5$ and therefore $gcd(45, 8) = 1$, where the closure factor is one full eight-tick cycle plus return and the Fibonacci factor is the smallest Fibonacci number greater than 1 that is coprime to 8.
background
The module derives the gap 45 from the eight-tick structure forced by T8 together with the Fibonacci sequence tied to φ. The closure factor is defined as eight_tick_period + 1, supplying the fence-post increment that closes one cycle. The Fibonacci factor is fixed at 5, the smallest Fibonacci number greater than 1 coprime to 8. Their product yields the gap, which the module identifies with the ninth triangular number T(9) representing cumulative phase over a closed eight-tick cycle.
proof idea
The term proof is a one-line wrapper that applies simplification using the definitions of gap, closure_factor, and fibonacci_factor, then invokes the decide tactic on the resulting numerical statement.
why it matters
This result supplies the coprimeness needed to form lcm(8, 45) = 360, which the module links directly to the emergence of D = 3 spatial dimensions from the eight-tick octave. It closes the algebraic step showing that 45 is forced by T8, the closure principle, and cumulative phase rather than chosen arbitrarily. The declaration sits inside the Gap45.Derivation module whose main theorem equates the gap to 45.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.