observeAvg8
plain-language theorem explainer
observeAvg8 defines the per-window averaged observation of a boolean stream s over k aligned blocks as the integer division of blockSumAligned8 by k. Measurement-layer authors cite it when equating stream observations to the window integer Z on periodic 8-bit extensions. The definition is a direct one-line wrapper around blockSumAligned8.
Claim. For $k : Nat$ and stream $s : Nat → Bool$, the averaged observation is defined by $observeAvg8(k,s) := blockSumAligned8(k,s) / k$.
background
The Streams.Blocks module defines Stream as the type Nat → Bool, an infinite boolean sequence. Pattern n denotes a finite window of length n, with Z_of_window extracting the integer value of an 8-bit pattern. blockSumAligned8 computes the sum of the first k aligned 8-bit blocks in the stream. The module ports the PatternLayer and MeasurementLayer cluster, centering on aligned sums for periodic extensions of windows.
proof idea
The definition is a one-line wrapper that applies blockSumAligned8 k s and divides the result by k.
why it matters
This definition supplies the averaged observation that enters the DNARP equation, which equates observeAvg8 k (extendPeriodic8 w) to Z_of_window w on periodic extensions. It is invoked by the Measurement module's observeAvg8 abbrev and by lemmas observeAvg8_periodic_eq_Z and sampleW. In the Recognition framework it supports the eight-tick octave (T7) and the mapping of observations onto the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.