shimmerFactor_three_decimal
plain-language theorem explainer
The theorem establishes the strict numerical bound 9.729 < 360/37 < 9.730 for the shimmer factor arising from Gap-45 arithmetic. Researchers modeling subjective-time scales or consciousness windows in Recognition Science would cite it to confirm the two-decimal rounding to 9.73. The proof is a one-line wrapper that rewrites the factor via its defining equality and applies norm_num to verify both inequalities.
Claim. $9.729 < 360/37 < 9.730$, where the ratio is the shimmer factor obtained from the least common multiple of the 8-tick and 45-tick periods divided by their difference.
background
The module defines gapLCM as lcm(8,45)=360, the minimal window in which the 8-tick body clock and 45-tick consciousness window realign, and gapDiff as 45-8=37, the prime arithmetic beat between those periods. The shimmer factor is then their ratio 360/37. The module documentation states that every claim reduces to native_decide on natural-number facts or norm_num on real arithmetic, with zero hidden physical input or calibration. Upstream dependence includes the equality that reduces the factor exactly to this ratio, together with the structural facts on coprimality and window insufficiency proved in the RecognitionBarrier module.
proof idea
The proof rewrites the factor using the equality to 360/37, then splits the conjunction and applies norm_num to each side to confirm the decimal bounds.
why it matters
This bound supplies the concrete numerical precision for the shimmer subjective-time factor that the Gap-45 module extracts from the eight-tick octave and the 45-tick consciousness window. It directly supports the module claim that the factor is pure arithmetic on the pair (8,45) rather than an empirical constant, and it closes the three-decimal verification step referenced in the module documentation. No downstream theorems are listed, but the result supplies the rounding justification needed for any later calculation that treats the factor as approximately 9.73.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.