Cylinder_zero
The lemma shows that the cylinder generated by the empty pattern coincides with the full stream space. Researchers handling base cases in periodic bit-stream constructions or measure spaces within Recognition Science would cite it when initializing cylinder sets. The argument proceeds by set extensionality on an arbitrary stream, with one inclusion immediate from the universal set and the reverse direction supplied by the zero-membership characterization.
claimLet $w$ be a finite binary window of length zero. Then the cylinder set consisting of all streams that agree with $w$ on the initial positions equals the entire space of streams.
background
In the Streams module a Pattern of length $n$ is a map from the finite set Fin $n$ to Bool, serving as a finite binary window. The Cylinder of such a window is the collection of streams whose values on the first $n$ positions match the window exactly. The module itself treats periodic extensions of these windows together with finite sums over the resulting streams.
proof idea
The proof applies set extensionality to an arbitrary stream $s$. It then constructs the two directions of the set-membership equivalence: the forward direction follows because every element lies in the universal set, while the reverse direction invokes the specialized membership lemma for the zero-length pattern.
why it matters in Recognition Science
The result supplies the base case for cylinder sets, allowing uniform treatment of degenerate windows inside the periodic-extension constructions that appear later in the module. It supports the eight-tick octave framework by furnishing a trivial starting point for stream measures. No downstream theorems are recorded as direct users, yet the lemma closes a necessary edge case in the Pattern and Cylinder apparatus.
scope and limits
- Does not address patterns of positive length.
- Does not construct the periodic extension itself.
- Does not compute measures or sums over cylinders.
- Does not invoke J-cost or the phi-ladder.
formal statement (Lean)
36@[simp] lemma Cylinder_zero (w : Pattern 0) : Cylinder w = Set.univ := by
proof body
Term-mode proof.
37 ext s; constructor
38 · intro _; exact Set.mem_univ _
39 · intro _; exact (mem_Cylinder_zero w s)
40
41/-- Periodic extension of an 8‑bit window. -/