eightGateNeutral
plain-language theorem explainer
The eight-gate neutrality predicate requires that a real-valued signal sums to zero across any eight consecutive ticks. Researchers modeling spiral wavefields, periodic schedules, or coherence in virtual rotors and gravity candidates cite this predicate to enforce the gating constraint. The definition is a direct equational encoding of the eight-term sum condition with no lemmas or reductions applied.
Claim. A signal $w : ℕ → ℝ$ satisfies the eight-gate neutrality condition at starting index $t_0$ precisely when $∑_{k=0}^{7} w(t_0 + k) = 0$.
background
The SpiralField module supplies basic structures for a variational ansatz of logarithmic spiral fields under φ-scaling together with an eight-tick gating constraint; the module itself contains no theorems. The eight-tick window matches the period-$2^3$ octave in the unified forcing chain. Upstream, the predicate draws on the coherence score definitions from Measurement and CostModel (zero when the operations-per-second denominator vanishes) and on the meta-realization structure from UniversalForcingSelfReference.
proof idea
The declaration is a direct definition that equates the predicate to the vanishing of the sum over Finset.range 8 of the shifted signal values. No lemmas are applied; the body is a one-line equational definition.
why it matters
This predicate is re-exported into Flight.Schedule and supplies the core constraint for PulseCoherence in VirtualRotor and WaveformCompliance in Searl candidates. It implements the eight-tick gating of the spiral ansatz and corresponds to the T7 eight-tick octave step in the forcing chain (T0–T8). The immediate downstream consequence is the shift-invariance theorem for 8-periodic signals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.