Pattern
plain-language theorem explainer
A finite binary window of length n is formalized as any function assigning true or false to each of the first n positions. Researchers modeling stream measurements, block sums, or recognition cycles cite this when building discrete windows for integer functionals. The declaration is a direct type definition with no reduction steps or lemmas.
Claim. A pattern of length $n$ is a function $p : [0..n-1] → {true, false}$.
background
The module introduces pattern and measurement layers for streams, windows, and aligned block sums, porting the PatternLayer cluster. Patterns act as finite binary sequences whose ones are counted by the integer functional Z from the anchor relation. Upstream results define identical pattern types as maps from Fin d to Bool in the Patterns, Measurement, and Streams modules, with Z computing the count of true entries for sector-based mass anchors.
proof idea
The declaration is a direct definition that sets the pattern type to the function space Fin n → Bool. It inherits the structure from the sibling pattern definitions in the imported Streams and Patterns modules without additional tactics or reductions.
why it matters
This supplies the pattern type underlying forty downstream results, including the recognition-loop surjection in SimplicialLedger and the ionization monotonicity theorem. It supports the eight-tick octave (T7) by enabling periodic block extensions of length 8 and the aligned sums used in J-cost impulses. The definition closes the measurement-layer interface for stream-based recognition processes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.