gapLCM
plain-language theorem explainer
gapLCM defines the least common multiple of the 8-tick body period and the 45-tick gap period, yielding 360 as the shortest realignment interval. Researchers working on Gap-45 arithmetic in Recognition Science cite this definition when building the Shimmer factor and its certificates. The definition is a direct application of Nat.lcm to the two primitive periods with no further reduction.
Claim. Define the minimal joint realignment window as the least common multiple of the body-clock period 8 and the consciousness-window period 45, so that the window equals 360.
background
The module formalizes the Shimmer subjective-time factor as pure arithmetic on the Gap-45 primitives. bodyPeriod is the 8-tick body-clock period obtained from T6 as 2^D with D=3. gapPeriod is the 45-tick consciousness window whose difference from 8 produces the prime beat 37. The module states that every subsequent claim reduces to native_decide on natural-number facts or norm_num on real arithmetic, with no hidden physical input.
proof idea
This is a direct definition that applies Nat.lcm to bodyPeriod and gapPeriod. No tactics or lemmas are invoked beyond the standard library operation.
why it matters
The definition supplies the numerator for shimmerFactor and the lcm_eq certificate used in shimmer_cert and shimmer_is_gap45_arithmetic. It realizes the eight-tick octave (T7) together with the Gap-45 barrier inside the Recognition framework, allowing the ratio 360/37 to be treated as forced arithmetic rather than an empirical constant. Downstream results quote this value when they assert that the Shimmer factor is irreducible because 37 is prime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.