Cylinder
plain-language theorem explainer
Cylinder is the set of all boolean streams whose initial segment of length n exactly matches a given finite pattern window w. Measurement and stream-invariance researchers cite it to restrict attention to streams compatible with an observed 8-bit window before applying block-sum or Z functionals. The declaration is realized as a one-line abbreviation that directly re-exports the underlying PatternLayer construction.
Claim. Let $w$ be a finite pattern of length $n$. The cylinder set consists of all boolean streams $s$ such that $s_i = w_i$ for every index $i < n$.
background
In the Measurement module streams are boolean sequences and patterns are finite windows of length $n$, both re-exported from PatternLayer. The module supplies the eight-tick stream invariants used for measurement together with a lightweight continuous-time CQ-score scaffold. This construction sits atop foundational structures including J-cost minimization (strictly convex with unique minimum at 1) and the spectral emergence that forces SU(3)×SU(2)×U(1) gauge content together with exactly three generations.
proof idea
One-line wrapper that directly aliases PatternLayer.Cylinder w.
why it matters
Cylinder supplies the domain restriction for downstream lemmas such as firstBlockSum_eq_Z_on_cylinder, which equates the first block sum to Z_of_window on any stream inside the cylinder. It thereby anchors the eight-tick octave (T7) inside the measurement layer and supports the periodic-extension results used for Z evaluation on 8-bit windows. The declaration closes a small part of the measurement scaffold that feeds the continuous-time CQ score.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.