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

IndisputableMonolith.Streams.Blocks

show as:
view Lean formalization →

Boolean streams are formalized as infinite displays of 0s and 1s. The module supplies the Stream type, Pattern, Cylinder, Z_of_window, extendPeriodic8, and aligned block-sum operations that enforce eight-tick periodicity. Measurement and Core.Streams layers import these objects to build their invariants and CQ score. The content is entirely definitional with supporting equalities on cylinders and no top-level theorems.

claimA boolean stream is a map $S:ℤ→{0,1}$. The window sum is $Z(S,w)$ over a finite window $w$. The operator extendPeriodic8$(S)$ produces the unique 8-periodic extension. Block sums blockSumAligned8$(S,k)$ and firstBlockSum equal $Z$ when restricted to cylinders.

background

The module lives in the Streams domain of Recognition Science and treats boolean sequences as discrete observation displays. Stream is the base type of infinite {0,1}-valued sequences; Pattern encodes repeating units; Cylinder denotes finite segments; Z_of_window computes the bit sum inside a window. extendPeriodic8 and sumFirst8_extendPeriodic_eq_Z enforce the eight-tick octave (period 2^3) required by the forcing chain. The module imports only Mathlib and supplies the discrete scaffolding later re-exported for measurement.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds IndisputableMonolith.Core.Streams and supplies the eight-tick stream invariants re-exported by IndisputableMonolith.Measurement for its CQ score. It closes the discrete stream layer that connects window sums to the phi-ladder and mass formulas. The constructions realize the T7 octave inside the Recognition framework.

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)