balancedSchedule_neutral
plain-language theorem explainer
The balanced schedule, with +1 on the first four ticks and -1 on the last four of an eight-tick cycle, satisfies the zero-sum neutrality constraint. Engineers modeling Nautilus-class power tiers cite this to confirm a concrete neutral schedule exists for Class C access paths. The proof reduces the claim by unfolding both definitions and simplifying the finite sum over Fin 8.
Claim. Let $S: Fin 8 → ℝ$ be defined by $S(i) = 1$ if $i.val < 4$ and $S(i) = -1$ otherwise. Then $∑_{i: Fin 8} S(i) = 0$.
background
The module encodes the Nautilus-class technological access path for Class C powers, treating power tiers and mappings as structural definitions while drawing engineering parameters from the NTL provisional patent stack. scheduleNeutral requires the sum of any aligned eight-tick window to vanish, implementing the eight-tick octave periodicity. balancedSchedule supplies the explicit function that places +1 in the first half and -1 in the second half of each window of length 8.
proof idea
One-line wrapper that unfolds scheduleNeutral and balancedSchedule, then simplifies the sum via Fin.sum_univ_eight.
why it matters
The result verifies that a neutral schedule is achievable inside the Nautilus framework, directly supporting the engineering parameters listed in the module documentation. It instantiates the eight-tick octave structure from the Recognition Science forcing chain (T7). No downstream theorems are recorded, leaving open its integration with tier-power and safety calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.