shimmerFactor_error_bound
plain-language theorem explainer
The theorem bounds the shimmer factor, obtained as lcm(8,45) divided by the difference 45-8, to within 0.001 of the decimal 9.73. Workers on subjective-time scales or Gap-45 arithmetic in Recognition Science cite the bound when treating the observed ratio as a fixed numerical input. The proof rewrites the factor to its exact rational form 360/37 then invokes abs_lt and norm_num to confirm the inequality holds.
Claim. $|360/37 - 9.73| < 0.001$
background
The module defines gapLCM as lcm(8,45) = 360 and gapDiff as 45-8 = 37, with the shimmer factor their ratio 360/37. These arise from the eight-tick body clock and the 45-tick consciousness window whose realignment period is the least common multiple; the difference 37 is prime and coprime to 360. The local setting is pure Gap-45 arithmetic: every identity reduces to native_decide on natural-number facts or norm_num on real arithmetic, with no empirical calibration or hidden physical input. Upstream results supply the structural facts (coprime gap, primality of 37) from RecognitionBarrier; the present bound merely observes the numerical consequence once those facts are in place.
proof idea
The term proof first rewrites shimmerFactor via the already-proved equality shimmerFactor_eq_360_div_37, converting the expression to the concrete rational 360/37. It then applies abs_lt to split the absolute-value inequality into two one-sided bounds and finishes with norm_num on both sides.
why it matters
The declaration supplies the concrete numerical error control required whenever the meta-claim (shimmer factor equals 360/37 with no extra physics) is invoked downstream. It closes the Gap-45 arithmetic package by confirming that the displayed precision 9.73 is accurate to three decimal places, consistent with the eight-tick octave and the coprimality already established in the barrier module. No parent theorem is listed among the used-by edges; the result therefore functions as a terminal numerical witness rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.