Cylinder
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not define periodic extension of the window.
- Does not compute the Z functional or any block sums.
- Does not impose dynamics beyond the initial matching condition.
- Does not address the continuous-time CQ-score construction.
formal statement (Lean)
26abbrev Cylinder {n : Nat} (w : Pattern n) : Set Stream := PatternLayer.Cylinder w
proof body
Definition body.
27
28/-- Periodic extension of an 8-bit window. -/