module module

`IndisputableMonolith.Gap45.SyncMinimization`

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

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cosmology.PerpetualComplexity module_import
IndisputableMonolith.Gap45.RecognitionBarrier module_import

declarations in this module (47)

def T L38
theorem T_0 L40
theorem T_1 L41
theorem T_9 L42
theorem T_25 L43
theorem T_49 L44
theorem T_81 L45
theorem T_121 L46
theorem T_4 L47
theorem T_16 L48
def phasePeriod L53
theorem phasePeriod_3 L55
theorem phasePeriod_5 L56
theorem phasePeriod_7 L57
theorem phasePeriod_9 L58
theorem phasePeriod_11 L59
theorem phasePeriod_even_2 L62
theorem phasePeriod_even_4 L63
theorem phasePeriod_even_6 L64
theorem phasePeriod_even_8 L65
theorem phasePeriod_even_10 L66
theorem phasePeriod_odd_3 L69
theorem phasePeriod_odd_5 L70
theorem phasePeriod_odd_7 L71
theorem phasePeriod_odd_9 L72
theorem phasePeriod_odd_11 L73
theorem coprime_3 L77
theorem coprime_5 L78
theorem coprime_7 L79
theorem coprime_9 L80
theorem coprime_11 L81
def syncPeriod L86
theorem syncPeriod_3 L88
theorem syncPeriod_5 L89
theorem syncPeriod_7 L90
theorem syncPeriod_9 L91
theorem syncPeriod_11 L92
theorem sync_3_lt_5 L97
theorem sync_3_lt_7 L100
theorem sync_3_lt_9 L103
theorem sync_3_lt_11 L106
theorem constraint_S_minimization L122
theorem D3_unique_minimizer L129
theorem even_D_not_coprime L137
theorem sync_strictly_increasing_odd L146
structure ConstraintS_Cert L156
def constraintS L170