ShimmerCert
plain-language theorem explainer
The ShimmerCert structure packages the identity that the subjective-time factor equals 360/37 together with its derivation as the ratio of lcm(8,45) to the difference 45-8. Modules working on Gap-45 models cite the certificate to invoke the numerical value and its bounds without repeating the arithmetic reductions. The structure is assembled by unfolding the period definitions and discharging the natural-number facts via native decision procedures.
Claim. Let $s = 360/37$. Then $s = (8,45)/ (45-8)$, where lcm$(8,45)=360$, $45-8=37$, 37 is prime, 8 and 45 are coprime, and $9.72 < s < 9.73$.
background
The module defines the shimmer factor from two Gap-45 primitives: the least common multiple of the 8-tick body period and the 45-tick gap period, together with their arithmetic difference. gapLCM is the minimal window in which the two clocks realign, while gapDiff is the beat between them. The factor is their ratio, which the module shows equals 360/37 by direct counting. MODULE_DOC states that every claim reduces to native_decide on natural numbers or norm_num on reals, with no hidden physical input or calibration step. Upstream results supply the canonical arithmetic object and the Gap-45 beat construction that fix the periods 8 and 45.
proof idea
The structure is a definition with no proof body. Each field is discharged in the canonical instance by unfolding the period definitions to expose the natural-number identities, then applying native_decide to the lcm, difference, primality, and coprimality statements together with norm_num on the real bounds.
why it matters
The certificate lets any downstream module cite the numerical value as pure Gap-45 arithmetic without rebuilding the reductions. It directly supports the module claim that the factor follows by counting once the structural facts (coprimality, primality) are established in RecognitionBarrier. The construction touches the eight-tick octave and the 45-tick window that appear in the Gap-45 forcing chain. It feeds the canonical instance shimmer_cert, which packages the entire arithmetic observation for later use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.