pith. sign in
module module high

IndisputableMonolith.Streams.Blocks

show as:
view Lean formalization →

The Streams.Blocks module defines Boolean streams as infinite displays together with patterns, cylinders, and eight-tick aligned block sums. Core.Streams and Measurement cite it to re-export the discrete invariants required for the measurement layer. The module consists solely of definitions with no theorems or proofs.

claimA Boolean stream is a map $s : ℕ → {0,1}$ viewed as an infinite display; Pattern denotes a finite window, Cylinder a periodic structure, extendPeriodic8 the period-8 extension, and blockSumAligned8 the sum over aligned 8-tick blocks.

background

The module sits in the Streams domain and supplies the discrete structures that realize the eight-tick octave (T7) of the forcing chain. It introduces Stream as an infinite Boolean sequence, Pattern and Z_of_window for local windows, Cylinder for periodic repetition, and the family of sum functions (sumFirst, subBlockSum8, blockSumAligned8) that compute invariants over successive blocks. These objects are imported only from Mathlib and carry no additional hypotheses.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions are re-exported by IndisputableMonolith.Core.Streams and supply the eight-tick stream invariants used throughout IndisputableMonolith.Measurement for the measurement-layer scaffold and CQ score. The module therefore supplies the concrete discrete display objects that later stages apply to the Recognition Composition Law and the eight-tick periodicity.

scope and limits

used by (2)

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

declarations in this module (17)