Periodic8
plain-language theorem explainer
Periodic8 encodes the condition that a schedule w from naturals to reals repeats every eight ticks. Flight-schedule proofs cite it as the hypothesis that makes neutrality scores invariant under unit shifts. The declaration is a direct one-line predicate definition with no further reduction.
Claim. A function $w : ℕ → ℝ$ is 8-periodic when $w(t+8) = w(t)$ holds for every natural number $t$.
background
The Flight.Schedule module supplies a minimal control surface for 8-tick schedules and re-uses the eight-window neutrality predicates already defined in SpiralField. Those predicates implement the eight-tick octave (period $2^3$) that appears as T7 in the unified forcing chain. Periodic8 is the predicate that asserts exact repetition of the schedule after eight steps, supplying the hypothesis needed for shift-invariance lemmas.
proof idea
The declaration is a direct definition. It expands immediately to the universal quantifier ∀ t, w (t + 8) = w t with no lemmas or tactics applied.
why it matters
Periodic8 is the hypothesis in eightGateNeutral_shift_invariance and neutralityScore_shift1_of_periodic8, both of which appear in the FlightReport summary of φ-geometry plus 8-gate results. It therefore places the eight-tick octave (T7) at the level of concrete schedules, ensuring that neutrality scores remain unchanged under shifts once periodicity holds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.