structure definition def or abbrev

`Schedule`

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

formal statement (Lean)

 202structure Schedule (E : Type _) where
 203  order : List E
 204  nodup : order.Pairwise (· ≠ ·)
 205
 206namespace Schedule
 207
 208variable [DecidableEq E]
 209
 210/-- Event at a given tick (index into the order), if any. -/

used by (15)

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

Trace in IndisputableMonolith.Flight.Falsifiers decl_use
mkLabPrediction in IndisputableMonolith.Flight.GravityBridge decl_use
FlightReport in IndisputableMonolith.Flight.Report decl_use
eightGateNeutral_shift_invariance in IndisputableMonolith.Flight.Schedule decl_use
PulseCoherence in IndisputableMonolith.Flight.SolidState.VirtualRotor decl_use
atomic_tick in IndisputableMonolith.Foundation.Atomicity decl_use
exists_sequential_schedule in IndisputableMonolith.Foundation.Atomicity decl_use
postAtTick in IndisputableMonolith.Foundation.Atomicity decl_use
sequential_preserves_conservation in IndisputableMonolith.Foundation.Atomicity decl_use
WaveformCompliance in IndisputableMonolith.Gravity.Candidates.Searl decl_use
balancedSchedule in IndisputableMonolith.Superhuman.TechnologicalAccess decl_use
Schedule in IndisputableMonolith.Superhuman.TechnologicalAccess decl_use
scheduleNeutral in IndisputableMonolith.Superhuman.TechnologicalAccess decl_use
schedule_neutrality_report in IndisputableMonolith.URCAdapters.LNALReports decl_use
OpcodeSoundnessCert in IndisputableMonolith.URCGenerators.LNALCerts decl_use

depends on (4)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Schedule in IndisputableMonolith.Superhuman.TechnologicalAccess decl_use