Cylinder
plain-language theorem explainer
Cylinder re-exports the set of streams whose first n bits match a given pattern window w. Block-sum and periodic-extension lemmas cite it when restricting to matching initial segments. The declaration is realized as a direct abbreviation of the PatternLayer cylinder constructor.
Claim. For natural number $n$ and pattern $w$ of length $n$, the cylinder set consists of all streams $s$ such that the first $n$ bits of $s$ coincide with $w$.
background
The Measurement module re-exports eight-tick stream invariants. Stream denotes boolean sequences and Pattern denotes finite windows of length $n$, both drawn from PatternLayer. Upstream structures supply J-cost convexity, spectral emergence of gauge content, and nuclear density tiers on the phi-ladder.
proof idea
One-line wrapper that applies PatternLayer.Cylinder.
why it matters
Cylinder supports firstBlockSum_eq_Z_on_cylinder and Z_of_window, which equate sub-block sums to the window functional on matching streams. It supplies the measurement-layer interface for eight-tick periodic extensions (T7) and feeds the continuous-time CQ scaffold in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.