Pattern
plain-language theorem explainer
Pattern(d) denotes the type of all binary sequences of length d. Applied modules in photobiomodulation, ionization energies, flyby anomalies, and simplicial ledgers cite it when they need finite windows for recognition loops or cross-pattern matrices. The declaration is a direct type definition with the simp attribute.
Claim. For each natural number $d$, let Pattern$(d)$ be the set of all functions from the finite set with $d$ elements to the two-element set of booleans.
background
Upstream modules define the same object as a finite window of length $n$ (Measurement.Pattern, Streams.Pattern, Streams.Blocks.Pattern). Each such window supports an integer functional that counts the number of true entries. The Patterns module re-exports the construction so that downstream files can import a single canonical name without module-qualified references.
proof idea
Direct definition: the body is the function type Fin d → Bool, annotated with @[simp] for automatic rewriting.
why it matters
This type is the common substrate for 40 downstream declarations, including lambda_PBM_approx, ionization_monotone_within_period, anomaly_dissolved, is_recognition_loop, and octavePeriod_eq_eight. It supplies the finite binary states required by the eight-tick octave (T7) and by recognition-loop surjections in the simplicial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.