DriveSchedule
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not impose periodicity or neutrality constraints on any schedule.
- Does not assign physical units or dynamics to the pulse field.
- Does not reference mass ladders, J-cost, or Recognition constants.
formal statement (Lean)
28abbrev DriveSchedule := ℕ → Control
proof body
Definition body.
29
30/-- Re-export: 8-gate neutrality predicate. -/