pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Flight.Schedule

show as:
view Lean formalization →

The Flight.Schedule module supplies the core scheduling primitives for eight-tick periodic control in the spiral-field propulsion model. It defines per-tick control data, DriveSchedule sequences, neutralityScore, and invariance lemmas under Periodic8. Researchers building φ-vortex drive schedules or falsifiers import it to enforce the eight-gate neutrality constraint. The module consists of lightweight definitions plus short algebraic lemmas on shifts and successors.

claimA DriveSchedule is a function from ticks to Control data; neutralityScore measures deviation from eight-gate balance on a Periodic8 sequence, with eightGateNeutral asserting score zero and shift-invariance.

background

The module sits inside the Flight subtheory of Recognition Science, which formalizes spiral-field propulsion under the φ-scaling and eight-tick gating introduced in Spiral.SpiralField. SpiralField supplies the variational ansatz for logarithmic spiral wavefields; Schedule adds the discrete control layer that realizes the eight-tick octave (period 2^3) constraint. Key objects are Control (minimal datum per tick), DriveSchedule (sequence of controls), Periodic8 (period-8 repetition), and neutralityScore (balance metric across the eight gates). The doc-comment notes that Control is kept intentionally small so hardware refinements can be added later.

proof idea

This is a definition module. It introduces the named objects via abbrevs and defs, then proves three short lemmas: neutralityScore_succ (additive property on successor ticks), neutralityScore_shift1_of_periodic8 (score unchanged under unit shift of a periodic sequence), and eightGateNeutral_shift_invariance (neutrality preserved under cyclic shift). All proofs are one-line or direct rewrites using the Periodic8 assumption.

why it matters in Recognition Science

Schedule supplies the discrete timing layer required by the parent Flight facade and by the downstream modules Flight.Falsifiers, Flight.GravityBridge, Flight.Report, Flight.SolidState.VirtualRotor, and Gravity.Candidates.Searl. It encodes the eight-tick gating that links the SpiralField ansatz to concrete drive schedules, allowing falsifiers to check recorded traces against neutrality and enabling the Searl-effect and virtual-rotor hypotheses to be stated with explicit periodic control.

scope and limits

used by (6)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)