DriveSchedule
plain-language theorem explainer
A drive schedule is a function from natural-number ticks to a minimal control datum. Flight subtheory work cites this abbreviation when assembling trace schemas or status reports. The declaration is a direct type alias that re-exports the control stream for the 8-tick discipline.
Claim. A drive schedule is a map $f : {N} {to} C$, where $C$ is the structure whose sole field is a boolean pulse.
background
The Flight module sets up an 8-tick control discipline and re-exports neutrality predicates from SpiralField. Control is the minimal per-tick datum consisting of a single boolean pulse field; its doc-comment states that hardware-level specifications will refine this later. The local setting therefore treats schedules as pure tick-indexed streams that later structures can annotate with pressure or thrust data.
proof idea
This is a direct abbreviation that equates DriveSchedule to the function type from natural numbers to Control. No lemmas or tactics are invoked; the declaration simply introduces a type synonym.
why it matters
DriveSchedule supplies the schedule field required by the Trace structure in Falsifiers and by the FlightReport summary. It anchors the commanded control surface inside the 8-tick octave (T7) of the forcing chain, keeping all Flight objects inside RS-native terminology. The definition therefore closes the minimal interface between scheduling and downstream experimental reporting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.