shimmerFactor_approx
plain-language theorem explainer
The declaration establishes that the Shimmer subjective-time factor, defined as the ratio of the Gap-45 least common multiple to the period difference, satisfies 9.72 < factor < 9.73. Researchers auditing Gap-45 arithmetic in Recognition Science would cite it to confirm the numerical value of 360/37. The proof is a direct term-mode pairing of the separately established lower and upper bound theorems.
Claim. $9.72 < 360/37 < 9.73$
background
The module formalizes the Shimmer subjective-time factor from Gap-45 arithmetic. gapLCM is defined as lcm(8,45) = 360, the minimal window aligning the 8-tick body clock and 45-tick consciousness window; gapDiff is 45 - 8 = 37, the arithmetic beat between those periods. The factor itself is their ratio, reducing exactly to 360/37 as stated in the module documentation.
proof idea
The proof is a term-mode construction that directly supplies the pair of the lower-bound theorem shimmerFactor_gt_9_72 and the upper-bound theorem shimmerFactor_lt_9_73. Each bound reduces via the equality shimmerFactor_eq_360_div_37 to a norm_num call on the real arithmetic of 360/37.
why it matters
This result pins the approximate numerical value of the Shimmer factor inside the Gap-45 module. The module documentation states that the bounds follow from native_decide and norm_num with zero axioms, confirming that the factor is pure arithmetic on the primitives (8,45). It supports the broader claim that the ratio ~9.73 is forced by the Gap-45 structure rather than by external calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.