pith. sign in
module module moderate

IndisputableMonolith.Streams

show as:
view Lean formalization →

The Streams module defines Boolean streams as infinite displays to support periodic pattern modeling in Recognition Science. It introduces Stream, Pattern, Cylinder, and extendPeriodic8 for eight-tick structures. Measurement and Core modules cite these primitives to access stream invariants. The module consists of definitions and basic lemmas with no complex proofs.

claimA stream is a map $S: ℕ → {0,1}$ as an infinite Boolean display; a pattern is a finite window; Cylinder denotes agreement on initial segments; extendPeriodic8 produces period-8 extensions.

background

The module sets the stream layer for Recognition Science's eight-tick octave (T7). Stream is the core infinite Boolean display; Pattern and Z_of_window handle local windows and zero counts; Cylinder and extendPeriodic8 manage periodic extensions of period 8. It imports only Mathlib and supplies the discrete display primitives used by downstream measurement scaffolds.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the eight-tick stream invariants into IndisputableMonolith.Core.Streams and IndisputableMonolith.Measurement, where the latter re-exports them for the measurement layer and CQ score. It supplies the stream primitives required for T7 in the unified forcing chain.

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)