shimmerFactor_pos
plain-language theorem explainer
The theorem establishes that the Shimmer subjective-time factor is strictly positive. Researchers working on Gap-45 arithmetic would cite it when confirming the sign of the ratio derived from the 8-tick and 45-tick periods. The proof is a one-line wrapper that rewrites the factor to 360/37 and applies norm_num.
Claim. $0 < 360/37$, where the left-hand side is the Shimmer factor obtained as the ratio of lcm(8,45) to the difference 45 minus 8.
background
The Shimmer factor is defined directly from the Gap-45 primitives as (gapLCM : ℝ) / (gapDiff : ℝ), with gapLCM equal to lcm(8,45) and gapDiff equal to 45 minus 8. The module states that this ratio is pure arithmetic on the pair (8,45) arising from the eight-tick body clock and 45-tick consciousness window, with no hidden physical input. The upstream theorem shimmerFactor_eq_360_div_37 states that the factor reduces to the bare arithmetic ratio 360/37.
proof idea
The proof is a one-line wrapper that applies the rewrite from shimmerFactor_eq_360_div_37 to express the factor as 360/37, then uses norm_num to confirm positivity of the resulting rational.
why it matters
This theorem confirms the positivity of the Shimmer factor inside the Gap-45 arithmetic structure that follows from alignment of the 8-tick octave and 45-tick window. It supports the module claim that the approximate value near 9.73 follows by counting once the structural facts from RecognitionBarrier are in place. The result touches the T7 eight-tick octave landmark but adds no new physics content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.