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

Pattern

show as:
view Lean formalization →

Streams defines Pattern n as the type of all binary sequences of exact length n. Modelers of periodic forcing chains or ledger cycles cite this when constructing finite windows for J-cost calculations or recognition passes. The definition is a direct type abbreviation with no proof content or additional axioms.

claimA pattern of length $n$ is any function $P : [n] → {0,1}$, where $[n] = {0,…,n-1}$ denotes the standard finite set of size $n$.

background

The Streams module treats periodic extensions and finite sums over binary windows. Pattern n is the local abbreviation for a finite binary window of length n, matching the upstream definition in Patterns.Pattern (d : Nat) := Fin d → Bool and the sibling in Blocks.Pattern. It is used together with the integer map Z from Anchor, which counts the number of true entries in such a window to produce the sector-dependent integer employed in anchor relations and mass formulas.

proof idea

One-line definition that directly sets Pattern n equal to the function type Fin n → Bool, inheriting the structure already present in the upstream Patterns and Blocks modules.

why it matters in Recognition Science

This definition supplies the finite pattern type required by downstream results such as is_recognition_loop in SimplicialLedger (which demands a surjective pass through Pattern 3) and by ionization_monotone_within_period and lambda_PBM_approx. It supports the eight-tick octave construction (T7) by providing the basic objects that extend periodically with period 8, closing the interface between raw binary windows and the forcing-chain steps that reach D = 3 and the alpha band.

scope and limits

formal statement (Lean)

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

proof body

Definition body.

  15
  16/-- 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.