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

Pattern

show as:
view Lean formalization →

Pattern(d) is the type of all binary sequences of length d, formalized as functions from the finite set Fin d to Bool. Workers on recognition loops, cross-domain matrices, and ionization proxies cite it when they need a uniform space of finite windows for counting ones or checking surjections. The declaration is a one-line type alias with no further axioms or reductions.

claimFor each natural number $d$, the pattern space Pattern$(d)$ consists of all functions from the finite set Fin $d$ to the Boolean values true and false.

background

In the Patterns module the declaration supplies the basic finite-window type used throughout Recognition Science. Upstream results in Streams and Streams.Blocks define the identical type Fin n → Bool and equip it with an integer functional Z that counts the number of true entries; Measurement re-exports the same abbreviation for windows of length n. The local setting therefore treats Pattern(d) as the discrete configuration space on which recognition composition, octave periods, and simplicial cycles operate.

proof idea

The declaration is a one-line definition that directly identifies Pattern(d) with the function type Fin d → Bool, inheriting the structure already present in the three upstream modules.

why it matters in Recognition Science

The definition feeds the parent results is_recognition_loop and recognition_loop_has_surjection in SimplicialLedger (which require surjective maps into Pattern 3) as well as entries_distinct in CrossPatternMatrix and ionization_monotone_within_period. It supplies the concrete pattern space for the T7 eight-tick octave and the recognition-loop construction that closes the forcing chain from T0 to T8.

scope and limits

formal statement (Lean)

   9@[simp] def Pattern (d : Nat) := (Fin d → Bool)

proof body

Definition body.

  10

used by (40)

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

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.