pith. machine review for the scientific record. sign in
def definition def or abbrev high

Pattern

show as:
view Lean formalization →

Finite patterns of length n are maps from an n-element index set to boolean values, encoding binary windows for stream measurements. Researchers modeling recognition loops in simplicial ledgers or monotone ionization proxies cite this as the base type. The declaration is a direct type definition that reuses the Fin n to Bool structure from the core Patterns module.

claimA pattern of length $n$ is a function from the finite set of $n$ positions to the boolean values.

background

The Streams.Blocks module defines patterns within the measurement layer for streams, windows, and aligned block sums, porting the PatternLayer cluster. Upstream, the Z functional counts the number of true entries in a pattern for anchor relations in mass calculations, as in the Anchor.Z definition that maps sectors and rationals to integers via quadratic and quartic terms. The identical type appears in the Patterns module as Fin d to Bool and in Measurement as an abbreviation for finite windows.

proof idea

The declaration is a direct definition that sets the pattern to the function type Fin n to Bool, matching the structure from the imported Patterns.Pattern without further reduction or lemmas.

why it matters in Recognition Science

This supplies the base type for 40 downstream uses, including recognition loops that demand surjective passes over Pattern 3 in the SimplicialLedger and distinct-entry theorems in CrossPatternMatrix. It feeds ionization monotonicity results and experimental claims such as anomaly dissolution under thermal hypotheses. In the framework it anchors the T7 eight-tick octave through periodic extensions and block sums aligned to Z counts.

scope and limits

formal statement (Lean)

  19def Pattern (n : Nat) := Fin n → Bool

proof body

Definition body.

  20
  21/-- Integer functional `Z` counting ones in a finite window. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.