tight_implies_loose
plain-language theorem explainer
The declaration shows that the shimmer factor equals exactly 360/37 and lies strictly between 9 and 10. Gap-45 researchers cite it to obtain the factor's order of magnitude from the arithmetic ratio of lcm(8,45) to the period difference 37. The proof is a term-mode wrapper that packages the exact equality with two pre-proved norm_num bounds via refine and linarith.
Claim. Let $s$ be the shimmer factor defined by $s = 360/37$. Then $s = 360/37$ and $9 < s < 10$.
background
The module treats the shimmer factor as pure Gap-45 arithmetic. gapLCM is defined as lcm(8,45) = 360, the smallest window in which the 8-tick body clock and 45-tick consciousness window realign; gapDiff is 45-8 = 37, the prime beat between the periods. The factor is their ratio: shimmerFactor := (gapLCM : ℝ) / (gapDiff : ℝ).
proof idea
The proof is a term-mode wrapper. It applies refine to the exact equality shimmerFactor_eq_360_div_37 together with two subgoals, then discharges each subgoal by linarith on the sibling theorems shimmerFactor_gt_9_72 and shimmerFactor_lt_9_73.
why it matters
This packages the numerical value of the shimmer factor for downstream use in RecognitionBarrier, where the loose interval 9 < factor < 10 may suffice for window arguments. It completes the Gap-45 arithmetic observation that the factor ~9.73 follows directly from lcm(8,45) and 45-8, with no empirical input. The module states that the non-trivial structural content resides in RecognitionBarrier while this file records the forced numerical consequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.