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

Stream

show as:
view Lean formalization →

Boolean streams model infinite binary sequences that represent periodic 8-tick patterns for discrete observations. A physicist constructing cylinder sets or aligned block sums over finite windows cites this when deriving measurement protocols from the eight-tick octave. The declaration is introduced as a direct type abbreviation with no proof obligations or additional axioms.

claimA boolean stream is a function $S : ℕ → {0,1}$ from the natural numbers to the booleans.

background

The Streams module supplies boolean streams to enable periodic extensions and finite sums over 8-tick windows. This setting follows the Recognition Science eight-tick octave where each tick updates at most eight local neighbors, as described in the PhysicsComplexityStructure upstream result on J-cost minimization being strictly convex with unique minimum at argument 1. The active edge count A equals 1 from IntegrationGap supplies the discrete tick balance at D=3.

proof idea

The declaration is a direct type abbreviation of the function space from naturals to booleans. No lemmas or tactics are invoked; it functions as the base type for sibling constructions such as Pattern and Cylinder.

why it matters in Recognition Science

This definition supplies the base type for the measurement layer, feeding directly into Cylinder, blockSumAligned8, observeAvg8, and firstBlockSum_eq_Z_on_cylinder. It realizes the eight-tick octave (T7) by permitting periodic extension of finite windows, linking to the phi-ladder mass formula and the J-cost structure from PhiForcingDerived. It closes the interface between discrete streams and the spectral emergence of gauge content and fermion generations.

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.