shimmerFactor_lt_9_73
plain-language theorem explainer
The inequality establishes that the Gap-45 ratio 360/37 lies strictly below 9.73. Researchers modeling subjective time scales via the Recognition Composition Law cite this bound when anchoring the Shimmer factor inside its arithmetic window. The proof is a one-line rewrite to the exact fraction followed by norm_num.
Claim. $S < 9.73$ where $S = 360/37$ and $S$ is the Shimmer factor obtained as the ratio of the least common multiple of the body period 8 and consciousness window 45 to their difference 37.
background
The Gap45.ShimmerFactor module fixes the body period at 8 ticks and the consciousness window at 45 ticks. Their least common multiple equals 360 while their difference equals 37, so the Shimmer factor is defined directly as the real division of these two quantities. This construction encodes the minimal realignment window forced by the eight-tick octave in the UnifiedForcingChain together with the RecognitionBarrier that enforces the 45-tick window.
proof idea
The proof is a one-line wrapper. It applies the rewrite rule from shimmerFactor_eq_360_div_37 to replace the factor by the concrete fraction 360/37, after which norm_num discharges the numerical comparison against 9.73.
why it matters
This upper bound supplies the missing half of the tight interval used by shimmerFactor_approx and is invoked inside tight_implies_loose to obtain the looser 9 < factor < 10 statement required by RecognitionBarrier. It therefore certifies that the subjective-time factor approximately 9.73 is forced solely by the Gap-45 primitives, consistent with the T7 eight-tick octave. The arithmetic layer is closed; physical interpretation is deferred to the barrier theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.