 559def seqShift {α : Type*} (y : ℕ → α) : ℕ → α := fun n => y (n + 1)
 560
 561/-- The `W`-block window-sum operator from Proposition 2.8. -/
 562def windowSums {α : Type*} [AddCommMonoid α] (W : ℕ) (y : ℕ → α) : ℕ → α :=
 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. -/
 567theorem windowSums_shift_equivariant {α : Type*} [AddCommMonoid α]
 568    (W : ℕ) (y : ℕ → α) :
 569    windowSums W (fun n => y (n + W)) = seqShift (windowSums W y) := by
 570  funext k
 571  unfold windowSums seqShift
 572  refine Finset.sum_congr rfl ?_
 573  intro j hj
 574  rw [Nat.mul_add, Nat.mul_one]
 575  ac_rfl
 576
 577/-! ## §6. The Cost Algebra Structure -/
 578
 579/-- **The Cost Algebra**: a structure packaging the complete algebraic data.
 580
 581    This is the fundamental algebraic object of Recognition Science:
 582    - Carrier: ℝ₊ (positive reals)
 583    - Binary operation: multiplication (inherited from ℝ)
 584    - Cost function: J satisfying RCL
 585    - Identity: 1 with J(1) = 0
 586    - Involution: x ↦ 1/x preserving J
 587
 588    From this single structure, all of RS is derived. -/
 589structure CostAlgebraData where
 590  /-- The cost function -/
 591  cost : ℝ → ℝ
 592  /-- Satisfies the Recognition Composition Law -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.