Pith. sign in
module module high

IndisputableMonolith.Streams

show as:
view Lean formalization →

The Streams module defines boolean streams as infinite displays together with patterns, cylinders, and period-8 extensions. Researchers building the measurement layer cite it for the eight-tick stream invariants. It is a pure definition module containing no proofs or theorems.

claimThe module introduces the type $\mathrm{Stream} := \mathbb{N} \to \mathbb{B}$ of infinite boolean sequences, finite $\mathrm{Pattern}$s, cylinder sets $\mathrm{Cylinder}$, the window map $Z_\mathrm{of\_window}$, and the periodic extension $\mathrm{extendPeriodic8}$ obeying $\mathrm{extendPeriodic8\_period}$ with period 8.

background

The module supplies the basic objects for boolean streams viewed as infinite displays. Stream is the type of sequences indexed by natural numbers; Pattern and Z_of_window capture finite windows and their integer values; Cylinder denotes the basic cylinder sets. The four extendPeriodic8 lemmas establish that any stream can be made periodic with period 8 while preserving the zero window and modular equivalence. This setting aligns with the eight-tick octave of period $2^3$ required by the forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions are re-exported by IndisputableMonolith.Measurement, which states they supply the eight-tick stream invariants used throughout the measurement layer plus the CQ-score scaffold. The module therefore supplies the concrete periodic structures needed for T7 in the UnifiedForcingChain and for all downstream continuous-time measurement constructions.

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)