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)
139def modal_nyquist_limit : ℕ := modal_period / 2
proof body
Definition body.
140
141/-- Two configs are **modally equivalent** if they differ by less than one tick. -/
depends on (7)
Lean names referenced from this declaration's body.
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
one
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
one
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
modal_period
in IndisputableMonolith.Modal.ModalGeometry
decl_use
-
one
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
one
in IndisputableMonolith.RecogSpec.Core
decl_use