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

Stream

show as:
view Lean formalization →

Stream is the type of infinite boolean sequences used to represent continuous displays for periodic patterns in Recognition Science. Measurement protocols cite it when defining cylinders over 8-tick windows and computing aligned block sums. The definition is a direct type alias to the function space Nat to Bool with no computation or proof obligations.

claimA stream is a function from the natural numbers to the booleans.

background

The Streams module treats streams as infinite displays supporting periodic extension of finite patterns and finite sums over 8-tick periods. Upstream structures supply the discrete tick model: A defines the active edge count per fundamental tick with the identity φ^(A − gap) · φ^gap = φ at D = 3, while PhiForcingDerived supplies the J-cost structure J(x) = (x + x^{-1})/2 − 1. SpectralEmergence and PhysicsComplexityStructure add the local 8-tick neighbor updates and convex minimization at x = 1.

proof idea

The declaration is a direct definition with no lemmas applied and no tactics used.

why it matters in Recognition Science

This definition supplies the base type for the Measurement layer, where it is re-exported and used to form Cylinder sets of streams matching a window and to define blockSumAligned8 and observeAvg8. It anchors the periodic 8-tick octave (T7) and enables the firstBlockSum_eq_Z_on_cylinder lemma that equates subBlockSum8 on a cylinder to Z_of_window. The placement closes the interface between the forcing chain and concrete observation protocols.

scope and limits

formal statement (Lean)

  11def Stream := Nat → Bool

proof body

Definition body.

  12
  13/-- A finite window/pattern of length `n`. -/

used by (26)

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

depends on (10)

Lean names referenced from this declaration's body.