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

Z_of_window

show as:
view Lean formalization →

Z_of_window counts the number of 1-bits inside a finite pattern window of length n. Measurement and stream theorists cite it when equating block sums on periodic extensions or cylinders to the window content. The declaration is a one-line re-export from the underlying PatternLayer.

claimFor a pattern $w$ of length $n$, let $Z(w)$ denote the integer equal to the number of positions at which $w$ equals 1.

background

The Measurement module re-exports eight-tick stream invariants together with a lightweight continuous-time scaffold. Pattern n is the type of finite binary windows of length n. Z_of_window is the integer functional that simply tallies the 1-bits inside such a window. Upstream structures supply the J-cost convexity, the phi-ladder tiers, and the spectral emergence that fix the discrete measurement rules used throughout the layer.

proof idea

One-line wrapper that applies PatternLayer.Z_of_window to the supplied pattern.

why it matters in Recognition Science

The definition is the common target of the measurement lemmas blockSumAligned8_periodic, firstBlockSum_eq_Z_on_cylinder, observeAvg8_periodic_eq_Z and subBlockSum8_periodic_eq_Z. It supplies the right-hand side for the DNARP equations on periodic 8-tick streams and thereby closes the measurement step inside the eight-tick octave (T7) of the forcing chain.

scope and limits

formal statement (Lean)

  23abbrev Z_of_window {n : Nat} (w : Pattern n) : Nat := PatternLayer.Z_of_window w

proof body

Definition body.

  24
  25/-- Cylinder set of streams matching a window. -/

used by (18)

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

depends on (14)

Lean names referenced from this declaration's body.