Cylinder
The Cylinder definition introduces the set of infinite Boolean streams whose initial segment of length n matches a fixed finite pattern w. Researchers formalizing block-sum identities and periodic extensions in Recognition Science streams cite this when equating window functionals Z to partial sums. The construction is realized directly as a set comprehension with no auxiliary lemmas.
claimLet $w$ be a pattern of length $n$, i.e., a map from the finite set of indices $0$ to $n-1$ into the Boolean values. The cylinder set consists of all infinite streams $s$ such that $s(i)=w(i)$ for every index $i<n$.
background
In the Streams.Blocks module, a Stream is an infinite sequence of Booleans while a Pattern of length n is a finite map from Fin n to Bool. The cylinder collects every stream that agrees exactly with the given window on the first n positions. This set-theoretic object is re-exported as an abbreviation in the Measurement module and underpins lemmas that equate the integer functional Z (counting ones in the window) to aligned block sums.
proof idea
The definition is realized directly by set comprehension: the collection of all streams s satisfying s i.val = w i for each index i in Fin n. No tactics or upstream lemmas are applied; it functions as a pure definitional abbreviation.
why it matters in Recognition Science
Cylinder supplies the basic localization sets used by firstBlockSum_eq_Z_on_cylinder, sumFirst_eq_Z_on_cylinder, and extendPeriodic8_in_cylinder in both Streams and Measurement. These identities in turn support the eight-tick octave and the alignment of finite windows with the Z-functional required for discrete measurements in the Recognition framework. The definition closes the interface between finite patterns and infinite streams without invoking J-cost or phi-ladder structure.
scope and limits
- Does not equip the cylinder with any probability measure or topology.
- Does not extend the construction to streams taking values in alphabets other than Bool.
- Does not constrain the tail of the stream after position n.
- Does not reference J-cost, phi-ladder, or spatial dimension D=3.
formal statement (Lean)
26def Cylinder {n : Nat} (w : Pattern n) : Set Stream :=
proof body
Definition body.
27 { s | ∀ i : Fin n, s i.val = w i }
28
29/-- Periodic extension of an 8‑bit window. -/