seqShift
plain-language theorem explainer
seqShift defines the one-step forward shift operator on sequences indexed by natural numbers. It is cited in the proof of windowSums_shift_equivariant to relate a shifted input sequence to a shifted window-sum output. The declaration is a direct lambda expression requiring no lemmas or tactics.
Claim. For any type $α$ and sequence $y : ℕ → α$, the shifted sequence satisfies $(seqShift y)(n) = y(n+1)$.
background
CostAlgebra works with sequences when forming window sums of length W, where W denotes the number of wallpaper groups (17) as defined in Masses.Anchor.W, TauStepDerivation.W and MassTopology.W. The upstream theorem from in PrimitiveDistinction reduces seven independent axioms to four structural conditions plus three definitional facts that support the cost functional equation and Recognition Composition Law. seqShift supplies the elementary index-shift operator needed to state equivariance for these window sums.
proof idea
The declaration is introduced by a direct one-line lambda abstraction that increments the index by one. No upstream lemmas are applied and no tactics are used.
why it matters
seqShift is the notational prerequisite for the theorem windowSums_shift_equivariant, which states that shifting the input sequence by one full window shifts the windowed output by one index. This algebraic identity supports manipulations of cost sequences derived from the Recognition Composition Law and the eight-tick octave periodicity in the forcing chain. It fills a supporting role rather than a core physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.