Z_of_window_nonneg
plain-language theorem explainer
Lemma Z_of_window_nonneg shows that for every natural number n and every pattern w of length n the integer counting the number of true entries in the window is non-negative. Workers building finite sums or measures over streams in Recognition Science cite this basic property to guarantee non-negative counting functionals. The term-mode proof unfolds the sum definition and applies Finset.sum_nonneg, with a case split that decides each term evaluates to 0 or 1.
Claim. For any natural number $n$ and any map $w : Fin n → Bool$, the sum $Z(w) = ∑_{i ∈ Fin n} 1_{w(i)}$ satisfies $Z(w) ≥ 0$, where the indicator $1_{w(i)}$ equals 1 if $w(i)$ is true and 0 otherwise.
background
In the Streams module, which addresses periodic extensions and finite sums, Pattern n is the type of finite windows given by functions Fin n → Bool. Z_of_window is the associated integer functional that sums the indicators of true entries over the finite index set, returning a natural number that simply counts the ones present in the window. This construction re-uses the identical Pattern and Z_of_window definitions imported from the Measurement and Patterns modules, which supply the core finite-window abstractions.
proof idea
The term-mode proof first unfolds Z_of_window to expose the explicit Finset sum. It then applies Finset.sum_nonneg, which reduces the goal to showing every summand is non-negative. The intro tactic supplies the index i; a split on the if-then-else expression followed by decide confirms that each term is either 0 or 1.
why it matters
The lemma secures non-negativity of the basic counting functional Z inside the streams layer, a prerequisite for any later measure or cost built from finite windows. It supports downstream constructions involving sums over patterns even though no immediate users appear in the dependency graph. The result aligns with the framework's reliance on integer functionals for counting in finite windows as a step toward cylinders and periodic extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.