`constraintS`

definition

show as: view math explainer →

module: IndisputableMonolith.Gap45.SyncMinimization
domain: Gap45
line: 170 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.SyncMinimization on GitHub at line 170.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 167    syncPeriod 9 < syncPeriod 11
 168
 169/-- The verified constraint (S) certificate. -/
 170def constraintS : ConstraintS_Cert where
 171  phase_at_D3 := by native_decide
 172  sync_at_D3 := by native_decide
 173  coprime_at_D3 := by native_decide
 174  even_D_fails := even_D_not_coprime
 175  D3_minimizes := D3_unique_minimizer
 176  monotone_odd := sync_strictly_increasing_odd
 177
 178end SyncMinimization
 179end Gap45
 180end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.