sampleW
plain-language theorem explainer
The even-index 8-bit pattern supplies a concrete window with exactly four ones for testing stream measurements. Researchers in the Recognition Science streams and measurement layers cite it when verifying periodic extensions and block-sum identities. The definition is a direct functional assignment selecting true precisely on even indices in Fin 8.
Claim. The length-8 window $w : (Fin 8) → Bool$ with $w(i) = true$ exactly when the integer value of $i$ is even (hence $Z=4$).
background
Patterns are finite windows formalized as functions from Fin n to Bool, with Z_of_window the integer count of true entries. The module supplies the Pattern and Measurement layers for streams, periodic extensions of 8-bit windows, and aligned block sums. Upstream results include extendPeriodic8, which builds the infinite periodic stream from any such window, and observeAvg8, which averages observations over aligned blocks of length 8.
proof idea
Direct definition as the function literal that maps each index i in Fin 8 to true precisely when i.1 modulo 2 equals zero. No lemmas or tactics are applied; the body is a primitive construction serving as an example.
why it matters
The example anchors the eight-tick octave (T7) by furnishing a window with Z=4 for cylinder-set and block-sum checks in the Measurement layer. It illustrates the Pattern and Z_of_window interface that feeds sumFirst8_extendPeriodic_eq_Z and related identities, though it remains unreferenced downstream. It touches the periodic extension mechanism without closing scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.