module module high

`IndisputableMonolith.Gap45.ShimmerFactor`

The Gap45.ShimmerFactor module defines the shimmer factor that quantifies the mismatch between the 8-tick body clock and the 45-fold phase structure under the coprimality condition gcd(8,45)=1. Researchers analyzing periodic constraints in Recognition Science would cite these definitions when examining finite-horizon decision incompatibilities. The module consists of a sequence of definitions for periods, their LCM and difference, plus the shimmer factor with its equality and positivity properties.

claimLet $P_b=8$ be the body-clock period and $P_g=45$ the gap period. Define the least common multiple $L=360$, the difference $d=37$, and the shimmer factor $s=360/37$. Then $s>1$ and $s$ is positive.

background

The module sits inside the Gap45 domain and imports the RecognitionBarrier result that gcd(8,45)=1 prevents any finite sub-period from aligning the 8-tick cycle with the 45-fold structure. The 8-tick period is the body clock fixed by T6 of the forcing chain as $2^D=8$ with $D=3$. Definitions introduced here include bodyPeriod for the 8-tick interval, gapPeriod for the 45-fold interval, gapLCM as their least common multiple, gapDiff as their absolute difference, and shimmerFactor as the ratio 360/37 together with its basic arithmetic properties.

proof idea

This is a definition module, no proofs. It supplies the period constants, their LCM and difference, the explicit equality shimmerFactor_eq_360_div_37, and the two inequalities shimmerFactor_pos and shimmerFactor_gt_one.

why it matters in Recognition Science

The shimmer factor supplies a concrete numerical measure of the Gap-45 mismatch and feeds the larger Recognition Science treatment of the barrier. It directly instantiates the eight-tick octave from T7 and the coprimality obstruction stated in the upstream RecognitionBarrier doc-comment. No downstream theorems are listed, yet the definitions close the basic arithmetic layer required for any further Gap45 analysis.

scope and limits

Does not derive the coprimality condition itself.
Does not prove any dynamical or decision-theoretic consequences of the barrier.
Does not extend to other gap sizes or higher-dimensional cases.
Does not supply numerical approximations or simulation code.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gap45.RecognitionBarrier module_import

declarations in this module (21)

def bodyPeriod L63
def gapPeriod L66
def gapLCM L69
def gapDiff L72
theorem gapLCM_eq L74
theorem gapDiff_eq L76
theorem gapDiff_prime L80
theorem gap_coprime L85
def shimmerFactor L91
theorem shimmerFactor_eq_360_div_37 L94
theorem shimmerFactor_pos L100
theorem shimmerFactor_gt_one L103
theorem shimmerFactor_gt_9_72 L112
theorem shimmerFactor_lt_9_73 L115
theorem shimmerFactor_approx L118
theorem shimmerFactor_three_decimal L124
theorem shimmerFactor_error_bound L131
theorem shimmer_is_gap45_arithmetic L160
structure ShimmerCert L184
def shimmer_cert L202
theorem tight_implies_loose L218