Pattern
plain-language theorem explainer
Defines finite binary patterns of length n as functions from Fin n to Bool. Workers on recognition loops and pattern matrices cite this type for window constructions in streams. The definition is a direct type alias with no additional axioms or operations.
Claim. A pattern of length $n$ is any function from the set of the first $n$ natural numbers to the two-element boolean set.
background
The Streams module treats periodic extensions and finite sums over binary sequences. Pattern is the local definition of a finite window of length n. Upstream, Patterns.Pattern supplies the same Fin d → Bool shape, Measurement.Pattern aliases it via PatternLayer, and Anchor.Z supplies the integer counting functional that later acts on these windows.
proof idea
Direct definition as Fin n → Bool.
why it matters
Supplies the pattern type used by is_recognition_loop to require a surjective pass through Pattern 3, closing the eight-tick cycle step. Also appears in ionization_monotone_within_period, anomaly_dissolved, and CrossPatternMatrix.entries_distinct. Ties directly to the T7 eight-tick octave and the recognition composition law via finite windows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.