isNeutralWindow
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert that any concrete pattern satisfies the neutrality condition.
- Does not interpret the signed sum in terms of physical observables or energy.
- Does not extend the definition to window lengths other than 8.
- Does not derive ledger exactness or gap-weight uniqueness by itself.
formal statement (Lean)
23def isNeutralWindow (w : Pattern 8) : Prop :=
proof body
Definition body.
24 ∑ i : Fin 8, (if w i then (1 : ℤ) else (-1 : ℤ)) = 0
25
26/-- Eight-tick neutral window implies existence of potential -/