pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Streams

show as:
view Lean formalization →

The Streams module defines boolean streams as infinite displays together with patterns, window-to-Z maps, cylinders, and period-8 extensions. Researchers in the measurement layer cite it for the eight-tick stream invariants. The module consists entirely of definitions with no theorems or proofs.

claimA boolean stream is an infinite sequence $s : ℕ → {0,1}$ serving as a display. The module introduces finite patterns, a window-to-Z map, cylinder sets in the product topology, and the periodic extension operator with period 8.

background

Recognition Science models discrete sequences via the eight-tick octave (T7) of period 8. The module supplies the Stream type as boolean sequences for infinite displays, Pattern for finite segments, a map sending windows to integers Z, Cylinder for basic open sets, and the periodic extension with period 8 to enforce the octave periodicity. These objects are imported only from Mathlib and provide the discrete foundation before any continuous-time scaffold.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the stream definitions re-exported by IndisputableMonolith.Core.Streams and used in IndisputableMonolith.Measurement for eight-tick invariants plus the CQ score. It fills the discrete display structures required by T7 in the forcing chain before measurement-layer applications.

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)