shimmerFactor_gt_one
plain-language theorem explainer
The declaration proves the Shimmer subjective-time factor exceeds one. Researchers modeling Gap-45 arithmetic and subjective time scales in Recognition Science cite it to fix the factor's magnitude. The proof reduces the claim to an explicit fraction via an equality lemma then discharges the inequality by numerical normalization.
Claim. $1 < 360/37$, where the left-hand side is the shimmer subjective-time factor defined as the ratio of the least common multiple of the 8-tick and 45-tick periods to their arithmetic difference.
background
In the Gap-45 module the shimmer factor is obtained from two primitives: gapLCM equals the least common multiple of the 8-tick body clock and 45-tick consciousness window, hence 360, while gapDiff equals 45 minus 8, hence 37. The factor is their ratio, 360/37. The module states that once upstream structural facts on coprimality and window periods are in place, the numerical value follows by direct counting with no hidden physical input. The supporting equality theorem unfolds the definition and casts the natural-number identities to obtain the explicit fraction.
proof idea
The proof first rewrites the target inequality using the equality lemma that reduces the factor to 360/37, then applies the norm_num tactic to verify the resulting numerical comparison on the reals.
why it matters
The result supplies a basic numerical anchor for the Shimmer factor inside the Gap-45 arithmetic, confirming it lies strictly above unity. It aligns with the eight-tick octave of the forcing chain and supports the subjective-time interpretation noted in the module, although the module itself classifies the content as trivial arithmetic rather than a named physics theorem. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.