windowSums_shift_equivariant
plain-language theorem explainer
The result shows that window-summing a sequence after a shift by exactly W positions yields the same output as taking the original window sums and then shifting that sequence forward by one index. Researchers manipulating windowed sums inside additive monoids or building equivariant operators for cost functionals would invoke it when composing shifts with block sums. The proof is a short term-mode argument that reduces the claim to an index identity inside a finite sum and closes it with ac_rfl.
Claim. Let $W$ be a natural number and let $y : ℕ → α$ where α is an additive commutative monoid. Define the window-sum operator by $(windowSums_W y)(k) = ∑_{j=0}^{W-1} y(W k + j)$. Then $windowSums_W (n ↦ y(n + W)) = seqShift(windowSums_W y)$, where seqShift advances its argument sequence by one step.
background
In the CostAlgebra module the windowSums operator extracts W-block sums from an arbitrary sequence valued in an additive commutative monoid: it sums the W consecutive terms whose starting indices are multiples of W. The companion seqShift operator simply advances any sequence by one index. Both appear as basic sequence tools inside the larger Cost Algebra structure, whose carrier is the positive reals equipped with multiplication, the J-cost function satisfying the Recognition Composition Law, and the involution x ↦ 1/x. The present theorem supplies a shift-equivariance property for these operators, which is a prerequisite for algebraic manipulations that later feed into the functional equation and cost-composition lemmas listed among the sibling definitions.
proof idea
The term proof begins with funext k to reduce the equality of functions to an equality at each output index k. It then unfolds the definitions of windowSums and seqShift, exposing a finite sum over Finset.range W. Finset.sum_congr reduces the claim to showing that each summand matches after the index rewrite W*(k+1) = W*k + W. The rewrite Nat.mul_add together with Nat.mul_one produces the required index shift, after which ac_rfl closes the equality by commutativity and associativity of addition in α.
why it matters
The lemma sits inside the Cost Algebra section that packages the complete algebraic data (carrier ℝ₊, multiplication, J satisfying RCL, identity 1, and involution) from which the Recognition Science framework derives all further structure. It guarantees that the window-sum operator commutes with full-window shifts, a property needed to keep the algebra closed under the sequence operations that appear in the functional-equation proofs and in the costCompose family of siblings. Because the used-by list is currently empty, the result functions as an internal algebraic fact whose main role is to support later derivations of the Recognition Composition Law and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.