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

Stream

show as:
view Lean formalization →

The Stream abbreviation re-exports the boolean stream type from the underlying streams module into the Measurement layer. Researchers modeling discrete observations over periodic windows cite this when defining block sums and cylinder sets. It supplies the base type for eight-tick window functions without adding new structure. The implementation is a direct alias with no verification steps required.

claimA stream is a function $s : ℕ → {0,1}$ that supplies an infinite binary sequence for windowed observations.

background

The Measurement module re-exports eight-tick stream invariants to support discrete observation. Upstream, Stream is defined as Nat → Bool, an infinite display of binary states. This type connects to J-cost minimization structures (strictly convex at x=1) and spectral emergence results that fix gauge content and fermion counts from the Q₃ face-pair construction.

proof idea

One-line abbreviation that aliases the Stream definition from the PatternLayer module, inheriting the Nat → Bool type directly.

why it matters in Recognition Science

This supplies the stream type used by Cylinder, blockSumAligned8, observeAvg8 and firstBlockSum_eq_Z_on_cylinder in the same module, plus VorticityVoxel in Flight. It anchors the eight-tick octave (T7) for periodic window analysis and feeds the Recognition Composition Law applications in measurement. The re-export closes the interface between the streams foundation and the lightweight CQ-score scaffold.

scope and limits

formal statement (Lean)

  17abbrev Stream := PatternLayer.Stream

proof body

Definition body.

  18
  19/-- Finite windows of length `n`. -/

used by (26)

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

depends on (7)

Lean names referenced from this declaration's body.