shimmer_is_gap45_arithmetic
plain-language theorem explainer
The declaration shows that the shimmer factor equals lcm(8,45) divided by (45-8), which reduces exactly to 360/37, satisfies the stated bounds, and inherits primality of 37 together with coprimality of the inputs. Researchers formalizing the Gap-45 structure cite it to record that the numerical value ~9.73 is forced by the two period primitives alone. The proof is a term-mode refine that unfolds the local definitions and dispatches the arithmetic facts by native_decide together with direct references to sibling lemmas.
Claim. Let $s$ be the shimmer factor. Then $s = (45-8)^{-1} · lcm(8,45)$, $s = 360/37$, lcm(8,45)=360, 45-8=37, 37 is prime, gcd(8,45)=1, and $9.72 < s < 9.73$.
background
The Gap-45 module defines bodyPeriod as the 8-tick body clock (from the eight-tick octave) and gapPeriod as the 45-tick consciousness window. Their difference gapDiff equals 37 and their least common multiple gapLCM equals 360; shimmerFactor is then the ratio gapLCM/gapDiff. The upstream coprime_barrier theorem records that 8 and 45 share no common divisors, which is invoked directly. The module document states that every identity here reduces to native_decide on ℕ or norm_num on ℝ with zero hidden physical input or calibration.
proof idea
The term proof opens with refine to split the eight-way conjunction. The first conjunct is discharged by unfolding shimmerFactor, gapLCM, gapDiff, bodyPeriod and gapPeriod followed by rfl. The equality to 360/37 is taken verbatim from the sibling shimmerFactor_eq_360_div_37. The remaining four arithmetic identities and the two bounds are settled by native_decide; coprimality is taken from coprime_barrier.
why it matters
This packages the entire Gap-45 arithmetic observation into a single citable statement so that any later module can invoke 'the shimmer factor is pure arithmetic on (8,45)' without rebuilding the reductions. It sits inside the Recognition Science forcing chain at the T7 eight-tick octave (bodyPeriod=8) and supplies the numerical content of the Gap-45 barrier whose coprimality is proved upstream. The module document explicitly positions it as the trivial arithmetic wrapper whose non-trivial content lives in RecognitionBarrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.