No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
100theorem sync_3_lt_7 : syncPeriod 3 < syncPeriod 7 := by native_decide
proof body
Term-mode proof.
101
102/-- D = 3 has strictly smaller sync period than D = 9. -/
depends on (5)
Lean names referenced from this declaration's body.
-
period
in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS
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