Schedule
plain-language theorem explainer
An 8-tick schedule is a map assigning a signed integer contribution to each of the eight fundamental time quanta. Researchers modeling Nautilus-class propulsion tiers or flight falsifiers cite it when specifying periodic pulse sequences. The declaration is introduced as a direct type abbreviation that encodes the eight-tick periodicity from the forcing chain.
Claim. An 8-tick schedule is a function $s :$ Fin $8$ $→$ $ℤ$ that assigns a signed contribution to each tick index.
background
The tick is the fundamental RS time quantum, set to τ₀ = 1 in native units, with one octave defined as exactly eight ticks forming the basic evolution period. In the Superhuman module this type supports power-tier definitions for Class C technological access paths, where schedules encode signed contributions under the neutrality constraint. Upstream results include the general Schedule structure from Atomicity for finite histories and the tick definition from Constants, which together specialize the eight-tick case here.
proof idea
This is a direct abbreviation that defines the type as functions from Fin 8 to the integers.
why it matters
The definition supplies the schedule type used by downstream Flight results such as eightGateNeutral_shift_invariance and PulseCoherence, which enforce the 8-gate neutrality invariant. It encodes the T7 eight-tick octave landmark and supports the Recognition Composition Law through periodic signed contributions in technological access models. No open scaffolding is closed here; the type remains a structural primitive for later empirical falsifiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.