def definition def or abbrev

`octavePeriod`

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

formal statement (Lean)

 183@[simp] def octavePeriod : Time := 8 * tick

Definition body.

 184
 185/-- The breath cycle: 1024 ticks (8 × 128 = 8 × 2⁷). -/

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

status in IndisputableMonolith.Constants.RSNativeUnits decl_use
impulse_per_octave in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
impulse_per_octave_nonneg in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
impulse_per_octave_pos_of_ne_sat in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_eq_eight in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_is_minimal_cover in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_pos in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
VolcanicForcingAsJCostImpulseCert in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
volcanic_forcing_one_statement in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
Time in IndisputableMonolith.Constants.RSNativeUnits decl_use
octavePeriod in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use