Cylinder
plain-language theorem explainer
Cylinder defines the set of all infinite Boolean streams whose initial segment of length n matches a prescribed finite pattern w exactly. Researchers working on block sums, periodic extensions, and window functionals in the Recognition Science streams layer cite this when localizing measurements to finite windows. The definition is realized directly as the set comprehension of streams s satisfying s(i) = w(i) for every i in Fin n.
Claim. Let $w$ be a pattern of length $n$, i.e., a map from the finite index set to Boolean values. The cylinder set consists of all streams $s : {N} {to} {0,1}$ such that $s(i) = w(i)$ for every $i < n$.
background
The Streams module develops periodic extensions and finite sums over Boolean sequences. A Pattern of length n is the type Fin n → Bool; a Stream is the type Nat → Bool. Cylinder assembles the basic localization sets used by window functionals such as Z_of_window. The construction is re-exported from the Measurement layer, where it supplies the domain restriction for first-block sums and defect counting.
proof idea
The definition is given directly by the set-builder { s | ∀ i : Fin n, s i.val = w i }, which encodes the initial-segment agreement condition without invoking any lemma or tactic.
why it matters
Cylinder supplies the domain sets required by Cylinder_zero, mem_Cylinder_zero, extendPeriodic8_in_cylinder, and the Measurement lemmas firstBlockSum_eq_Z_on_cylinder and Z_of_window. It anchors the interface between finite patterns and infinite streams needed for the eight-tick octave (T7) and the Recognition Composition Law. The definition closes the localization step that lets Z count defects inside periodic windows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.