isNeutralWindow
plain-language theorem explainer
A length-8 window is neutral when the sum of its signed indicators equals zero. Researchers on eight-tick periodicity in Recognition Science cite this definition when linking neutrality to ledger exactness and gap weight. It is introduced directly as the signed-sum condition with no auxiliary lemmas.
Claim. A pattern $w$ of length 8 is neutral if $sum_{i in Fin 8} sigma_i = 0$, where $sigma_i = +1$ if position $i$ of $w$ holds and $sigma_i = -1$ otherwise.
background
The module axiomatizes eight-tick window neutrality and its connection to ledger exactness, with an extension that determines the gap weight $w_8$ appearing in the alpha inverse derivation via scheduler invariants. Pattern 8 denotes binary sequences of length 8 aligned to the fundamental octave. Upstream, the tick definition sets the RS time quantum to 1 with one octave equal to 8 ticks; structures from PhiForcingDerived supply J-cost and from SpectralEmergence supply the gauge and generation content that fix the periodicity.
proof idea
The definition is stated directly by the equality of the signed sum to zero over the eight positions.
why it matters
This definition supplies the hypothesis for the theorem eight_tick_neutral_implies_exact, which shows that neutral windows imply existence of a potential function. It formalizes the eight-tick neutrality constraint that uniquely determines gap weight $w_8$ in the alpha inverse derivation, consistent with the eight-tick octave (T7) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.