isNeutralWindow
plain-language theorem explainer
A length-8 pattern counts as neutral exactly when the signed sum of its eight states equals zero. Researchers deriving ledger exactness or gap-weight uniqueness in the eight-tick octave cite this when moving from neutrality to potential functions. The declaration is a direct one-line summation that encodes the zero-net condition with no additional lemmas.
Claim. A pattern $w$ on eight positions is neutral when $∑_{i=0}^7 s_i = 0$, where each $s_i = +1$ if position $i$ is active and $s_i = -1$ otherwise.
background
The module axiomatizes eight-tick window neutrality and its link to ledger exactness, with an extension to the gap weight $w_8$ that enters the $α^{-1}$ derivation via scheduler invariants such as sumFirst8. The Pattern type is imported from the Measurement namespace and represents binary configurations over a fixed length; here the length is fixed at 8 to match the octave period. Upstream, the tick is defined as the fundamental RS time quantum with one octave equal to exactly eight ticks, while structures from PhiForcingDerived and SpectralEmergence supply the J-cost and discrete tier context that motivate the signed-sum condition.
proof idea
This is a one-line definition whose body is the summation $∑ i : Fin 8, (if w i then 1 else -1) = 0$. No lemmas or tactics are invoked; the expression itself is the complete content of the declaration.
why it matters
The definition supplies the hypothesis for the downstream theorem eight_tick_neutral_implies_exact, which extracts an integer-valued potential from any neutral window. It occupies the T7 eight-tick octave slot in the forcing chain and supplies the neutrality constraint that the module doc states uniquely determines the gap weight $w_8$ appearing in the $α^{-1}$ band. The result therefore closes one link between the signed-sum condition and the ledger-factorization structures imported from DAlembert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.