Pattern
plain-language theorem explainer
Pattern d is the type of all functions from a d-element finite set to booleans, i.e., the set of binary strings of exact length d. Workers on recognition loops in simplicial ledgers and on cross-domain pattern matrices cite it when they need to count configurations or prove surjections over pattern spaces. The declaration is a one-line type abbreviation with the simp attribute for rewriting.
Claim. A pattern of length $d$ is any map $p : {0,1,…,d-1} → {true,false}$.
background
In the Patterns module this supplies the basic combinatorial type for binary sequences. Upstream results in Streams and Streams.Blocks define the identical object as a finite window of length n, equipped with an integer functional Z that counts the number of true entries. The same abbreviation appears in Measurement as a layer-specific pattern. The local setting is the combinatorial substrate for all later arguments that treat patterns as states in recognition cycles or as inputs to monotone maps.
proof idea
Direct definition; the body is the type expression Fin d → Bool with no further reduction or lemma application.
why it matters
It is the common source type for forty downstream declarations, among them is_recognition_loop and recognition_loop_has_surjection in SimplicialLedger (which require a surjective pass through Pattern 3) and lambda_PBM_approx in the photobiomodulation device. The definition therefore supports the eight-tick octave (T7) by furnishing the discrete state space 2^d whose cardinality enters Nyquist-type obstructions and minimal-cover results. It also feeds ionization_monotone_within_period and anomaly_dissolved, closing the link from pattern counting to concrete physical predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.