windowSums
The W-block window-sum operator aggregates W consecutive terms of a sequence valued in an additive commutative monoid. Researchers working on cost functional equations cite it when deriving shift properties that preserve composition laws. The definition is realized directly as a finite sum over the window range with no lemmas applied.
claimLet $α$ be an additive commutative monoid. For window size $W ∈ ℕ$ and sequence $y : ℕ → α$, the W-block window-sum operator is the function sending each index $k$ to the sum of $y(Wk + j)$ for $j$ from 0 to $W-1$.
background
In the CostAlgebra module the W-block window-sum operator implements the block summation referenced in Proposition 2.8. The window size W is supplied by the wallpaper_groups constant (value 17) as defined in the mass anchor, lepton generation derivations, and mass topology modules, where it counts 2D symmetry groups or face symmetries. The module imports the J-cost functional equation and its Aczel variant, placing the operator in the algebraic setting that supports the Recognition Composition Law.
proof idea
The definition is a direct one-line construction that maps each $k$ to Finset.sum over the range 0 to $W-1$, selecting the terms $y(W·k + j)$. It relies only on the AddCommMonoid structure for the sum and invokes no lemmas or tactics.
why it matters in Recognition Science
The operator is required by the shift-equivariance theorem in the same module, which shows that advancing the input by one window shifts the output by one block index. It realizes Proposition 2.8 and supplies the block structure used in algebraic manipulations of the J-cost under the Recognition Composition Law. The fixed window size aligns with the eight-tick octave when it matches the wallpaper symmetry count appearing in mass and QFT derivations.
scope and limits
- Does not prove any algebraic properties such as equivariance or associativity.
- Does not constrain W to be positive or link it to specific physical constants beyond wallpaper groups.
- Does not incorporate the J-cost or defect functions directly.
- Does not address zero or infinite window cases.
formal statement (Lean)
562def windowSums {α : Type*} [AddCommMonoid α] (W : ℕ) (y : ℕ → α) : ℕ → α :=
proof body
Definition body.
563 fun k => Finset.sum (Finset.range W) (fun j => y (W * k + j))
564
565/-- Shifting the input sequence by one full window shifts the windowed output
566 by one index. -/