pith. sign in
module module high

IndisputableMonolith.Streams

show as:
view Lean formalization →

The Streams module defines Boolean streams as infinite displays with eight-tick periodicity. Measurement-layer code cites it for stream invariants and the CQ score. Core.Streams also imports the definitions. The module is purely definitional and contains no proofs.

claimA stream is a map $S : ℤ → {0,1}$ viewed as an infinite Boolean display; auxiliary objects include finite patterns, the zero-count function $Z$ on windows, cylinders, and the period-8 extension operator.

background

The module sits inside the Recognition Science derivation of physics from a single functional equation. It supplies the discrete-time objects required by the eight-tick octave (T7). Sibling definitions introduce Stream, Pattern, Z_of_window, Cylinder, and extendPeriodic8 together with their basic properties (non-negativity, zero cases, periodicity).

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the eight-tick stream primitives re-exported by IndisputableMonolith.Measurement for the measurement layer and CQ score. It also supports IndisputableMonolith.Core.Streams. These definitions realize the period-2^3 structure demanded by the forcing chain at T7.

scope and limits

used by (2)

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

declarations in this module (19)