pith. machine review for the scientific record. sign in
def definition def or abbrev high

Z_of_window

show as:
view Lean formalization →

Z_of_window defines the integer count of true entries in a finite Boolean pattern of length n. Measurement and stream researchers cite it when equating block sums or periodic observations to the underlying window bit count. The definition is a direct summation that converts each Boolean to 1 or 0 and adds them over Fin n.

claimFor a pattern $w : (Fin n) → Bool$, define $Z(w) := ∑_{i ∈ Fin n} [w(i)]$, where $[true] = 1$ and $[false] = 0$.

background

The Streams module treats periodic extensions of finite windows and the associated finite sums. Pattern is the type Fin n → Bool, a finite window of length n whose entries are Booleans. Z_of_window is the integer functional that counts the number of true entries in such a window.

proof idea

Direct definition: the body is the summation over i : Fin n of the Iverson bracket that returns 1 precisely when w i is true.

why it matters in Recognition Science

This supplies the basic Z count used by downstream lemmas such as blockSumAligned8_periodic (block sums equal k · Z(w) on periodic extensions) and firstBlockSum_eq_Z_on_cylinder (first block sum equals Z on the cylinder of w). It anchors the DNARP equations and periodic observation equalities that appear throughout the Measurement layer. The definition therefore closes the interface between raw stream data and the integer functionals required for later mass and observation formulas.

scope and limits

formal statement (Lean)

  17def Z_of_window {n : Nat} (w : Pattern n) : Nat :=

proof body

Definition body.

  18  ∑ i : Fin n, (if w i then 1 else 0)
  19

used by (18)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.