mem_Cylinder_zero
Every boolean stream belongs to the cylinder set of any length-zero pattern. Researchers in the Recognition Science measurement layer cite this base case when reducing zero-window statements to the full stream space. The proof is a one-line wrapper that introduces the membership condition and eliminates the empty Fin type.
claimFor any pattern $w$ of length 0 and any stream $s$, $s$ belongs to the cylinder set defined by $w$, that is, the set of all streams satisfying the (vacuous) agreement condition on the empty finite index set.
background
The Streams module treats periodic extensions of windows and finite sums. Pattern n is the type of functions from Fin n to Bool, representing finite windows. Stream is the type of functions from Nat to Bool. Cylinder w is the set of streams that match w on the first n positions, expressed as the set of s such that for all i in Fin n, s(i) equals w(i).
proof idea
This is a one-line wrapper proof. It introduces the universal quantifier over the index in Fin 0 and discharges the goal by Fin.elim0, which holds vacuously for the empty type.
why it matters in Recognition Science
The lemma is invoked by Cylinder_zero to establish that the cylinder of the empty pattern equals the full set of streams. It supplies the base case for zero-length windows in the Recognition Science treatment of streams and measurements, consistent with the framework's handling of finite patterns in the forcing chain.
scope and limits
- Does not apply to patterns of positive length.
- Does not involve the Z functional or counting ones in windows.
- Does not address periodic extensions or sums.
- Does not apply outside boolean streams.
Lean usage
ext s; constructor; · intro _; exact Set.mem_univ _; · intro _; exact (mem_Cylinder_zero w s)formal statement (Lean)
33@[simp] lemma mem_Cylinder_zero (w : Pattern 0) (s : Stream) : s ∈ Cylinder w := by
proof body
One-line wrapper that applies intro.
34 intro i; exact (Fin.elim0 i)
35