gapPeriod
plain-language theorem explainer
gapPeriod defines the natural number 45 as the consciousness window period in Gap-45 arithmetic. Researchers on the Shimmer subjective-time factor cite it as one of the two fixed inputs that force the ratio 360/37. The definition is a direct constant assignment with no lemmas or computation steps.
Claim. Let $g = 45$ denote the period, in ticks, of the Gap-45 consciousness window.
background
The Gap45.ShimmerFactor module builds the Shimmer factor from two primitives: the 8-tick body clock and the 45-tick consciousness window supplied by gapPeriod. The module document states that gapLCM is defined as the least common multiple of the two periods and equals 360, while gapDiff is their difference and equals 37. These arithmetic relations generate the coprimality hypothesis used in downstream statements such as gap_coprime.
proof idea
The declaration is a direct definition that binds the name to the constant 45. No tactics or lemmas are applied.
why it matters
This definition supplies one of the two Gap-45 primitives that enter the master theorem shimmer_is_gap45_arithmetic, which asserts the factor equals 360/37, is bounded by 9.72 and 9.73, and is irreducible because the denominator 37 is prime. It also feeds gap_coprime, whose documentation states that coprimality of the periods generates the whole barrier. In the Recognition framework the choice of 45 instantiates the eight-tick octave with a consciousness window whose difference from 8 produces the subjective-time factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.