mem_Cylinder_zero
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.