shimmer_cert
plain-language theorem explainer
The canonical certificate bundles the arithmetic facts establishing the shimmer factor as exactly 360/37 from the Gap-45 periods. Workers on subjective time dilation cite this structure to reference the closed-form value and its supporting equalities without re-deriving the counts. Construction proceeds by direct assignment of the equality and verification of the component facts via unfolding and decision procedures.
Claim. The Shimmer certificate asserts that the factor equals $360/37$, obtained as the ratio of the least common multiple of the 8-tick body period and 45-tick consciousness period to their difference 37, together with the facts that this difference is prime, the periods are coprime, and the value lies between 9.72 and 9.73.
background
In the Gap-45 module the body period is defined as 8 (from the eight-tick octave) and the consciousness window as 45. Their least common multiple is 360 and difference 37. The shimmer factor is then their ratio. The upstream coprime_barrier theorem states that 8 and 45 are coprime, so no sub-period aligns both clocks. The time_dilation_factor theorem gives the loose bound 9 < 360/37 < 10. ShimmerCert is the structure that packages the closed-form value, the derivation from the gap primitives, the LCM and difference equalities, primality of 37, coprimality, and the tightened bounds 9.72 < factor < 9.73.
proof idea
The definition constructs the certificate by setting the value field to the pre-proved equality shimmerFactor_eq_360_div_37. The from_gap45 field is obtained by unfolding the definitions of shimmerFactor, gapLCM, gapDiff, bodyPeriod and gapPeriod then applying reflexivity. The LCM and difference equalities are settled by native_decide. Primality of 37 uses a show tactic with native_decide. Coprimality is imported from the barrier theorem. The lower and upper bounds come from separate inequalities proved elsewhere in the module.
why it matters
This definition supplies the canonical witness that the shimmer factor is pure Gap-45 arithmetic, allowing downstream modules to cite a single bundled fact rather than the individual counts. It supports the time dilation interpretation in RecognitionBarrier by tightening the numerical bounds. In the framework it connects the eight-tick octave and the Gap-45 structure to the subjective time factor without introducing new physical assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.