module module

`IndisputableMonolith.Gap45.ShimmerFactor`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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