five_eight_coprime
plain-language theorem explainer
The declaration proves that the greatest common divisor of 5 and 8 equals 1. Workers deriving the 45 gap in Recognition Science cite it to confirm the factorization 45 = 9 × 5 from the eight-tick cycle. The proof is a one-line decision procedure that computes the gcd on natural numbers directly.
Claim. $5$ and $8$ are consecutive Fibonacci numbers, hence coprime: $gcd(5,8)=1$.
background
The module derives the 45 gap from the eight-tick structure (T8) and the Fibonacci sequence tied to the golden ratio phi. Key result: 45 = (8 + 1) × 5, where the closure factor 9 = 8 + 1 accounts for one full cycle plus return, and the Fibonacci factor 5 is the smallest Fibonacci number greater than 1 that is coprime with 8. Physical motivation identifies 45 as the 9th triangular number T(9) = 1 + 2 + ... + 9, representing cumulative phase accumulation over a closed 8-tick cycle with linear cost per tick. This factorization is algebraically equivalent to T(9) = 9 × 5 and combines with lcm(8,45) = 360 to force D = 3 spatial dimensions.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic reduces the statement to a decidable equality on natural numbers and verifies the gcd computation by exhaustive evaluation.
why it matters
This result supports the module's derivation that 45 emerges from the eight-tick period (T8) combined with the Fibonacci sequence. It fills the algebraic step showing coprimality of 5 and 8, enabling the factorization that, together with the triangular-number interpretation, forces D = 3. The declaration touches the framework landmark T8 eight-tick octave and the closure principle that produces the 45 gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.