gapLCM_eq
Recognition Science researchers cite the equality of the joint realignment window to 360 when deriving the shimmer factor as 360 divided by 37 from Gap-45 primitives. This anchors the numerical value of the subjective-time factor without external input. The proof is a one-line native_decide tactic that evaluates the LCM definition on natural numbers.
claim$lcm(8,45)=360$, where 8 is the body clock period and 45 is the consciousness window period.
background
The Gap45.ShimmerFactor module constructs the shimmer subjective-time factor from two primitives: the body period of 8 (eight-tick octave) and gap period of 45. gapLCM is defined as Nat.lcm bodyPeriod gapPeriod, described in the upstream doc-comment as the minimal joint realignment window. The module doc states that gapLCM equals 360 and gapDiff equals 37, with the factor their ratio. This theorem confirms the LCM value so that downstream arithmetic can proceed by exact_mod_cast.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic directly to the definition of gapLCM. It computes lcm(8,45) on natural numbers and confirms equality to 360.
why it matters in Recognition Science
This result is invoked by the downstream theorem shimmerFactor_eq_360_div_37, which unfolds shimmerFactor and substitutes the cast values to obtain 360/37. It supplies the arithmetic step inside the Gap-45 structure, linking to the eight-tick octave (T7) in the forcing chain. The module doc notes that non-trivial content resides in RecognitionBarrier while this file records the forced numerical consequence.
scope and limits
- Does not derive the periods 8 and 45 from any physical principle.
- Does not establish coprimality or primality of 37.
- Does not address physical interpretation of the shimmer factor.
- Applies only to the specific Gap-45 periods in natural numbers.
Lean usage
have h1 : (gapLCM : ℝ) = 360 := by exact_mod_cast gapLCM_eqformal statement (Lean)
74theorem gapLCM_eq : gapLCM = 360 := by native_decide
proof body
75