gap_coprime
plain-language theorem explainer
The declaration establishes that the body period of 8 and the gap period of 45 share no common divisors other than 1. Researchers formalizing the Gap-45 arithmetic in Recognition Science cite it to underwrite the definition of the shimmer factor as the ratio 360/37. The proof is a direct term application of the coprime_barrier lemma, which itself reduces to native_decide.
Claim. $8$ and $45$ are coprime, i.e., their greatest common divisor is $1$, where $8$ is the body-clock period from the eight-tick octave and $45$ is the consciousness-window period.
background
In the Gap-45 module, bodyPeriod is defined as $8$, the period forced by T6 as the self-similar fixed point yielding $2^D$ with $D=3$. gapPeriod is defined as $45$, the consciousness window. The RecognitionBarrier module supplies the upstream theorem coprime_barrier, whose doc-comment states: '8 and 45 are coprime: no sub-period aligns both.'
proof idea
This is a one-line term proof that directly invokes the coprime_barrier theorem from RecognitionBarrier.
why it matters
Coprimality of the two Gap-45 primitives is the hypothesis that generates the whole barrier, allowing the shimmer factor to be defined as lcm(8,45)/(45-8) = 360/37 with 37 prime. It supports the module claim that this numerical observation is pure arithmetic on the primitives and feeds the downstream definitions of shimmerFactor and its bounds. The result touches the T7 eight-tick octave and the Gap-45 structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.