structure definition def or abbrev

`Control`

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

formal statement (Lean)

  23structure Control where
  24  pulse : Bool
  25  deriving Repr
  26
  27/-- A drive schedule is a tick-indexed control stream. -/

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

DriveSchedule in IndisputableMonolith.Flight.Schedule decl_use
global_only_policy in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
re_two_mul_nonneg_of_attachmentWithMargin in IndisputableMonolith.NumberTheory.RiemannHypothesis.AttachmentWithMargin decl_use

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use