theorem proved term proof

`syncPeriod_11`

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

formal statement (Lean)

  92@[simp] theorem syncPeriod_11 : syncPeriod 11 = 15116288 := by native_decide

Term-mode proof.

  93
  94/-! ## The Minimization Theorem (Constraint S) -/
  95
  96/-- D = 3 has strictly smaller sync period than D = 5. -/

Lean names referenced from this declaration's body.

period in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS decl_use
Constraint in IndisputableMonolith.Complexity.SAT.PC decl_use
syncPeriod in IndisputableMonolith.Constants.RSNativeUnits decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
syncPeriod in IndisputableMonolith.Gap45.SyncMinimization decl_use
syncPeriod in IndisputableMonolith.Papers.DraftV1 decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use