pith. sign in
module module high

IndisputableMonolith.Core.Streams

show as:
view Lean formalization →

Core.Streams aggregates the stream primitives for Recognition Science by importing periodic extensions with finite sums and the pattern/measurement layers. Researchers building pattern recognition or measurement models cite it for the foundational stream handling. The module is an import aggregator containing no proofs.

claimStreams $s$ equipped with periodic extension and finite sums, together with aligned block sums in the pattern and measurement layers.

background

The module imports IndisputableMonolith.Streams, whose doc-comment states it covers periodic extension and finite sums, and IndisputableMonolith.Streams.Blocks, whose doc-comment states it ports the PatternLayer/MeasurementLayer cluster for streams, windows, and aligned block sums. These imports place the stream infrastructure inside the core domain of the framework. The setting is therefore the stream layer that supports periodic data handling and block-wise measurement before higher Recognition Science constructions are applied.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the stream definitions that feed pattern and measurement operations throughout the Recognition Science framework. It connects the upstream streams and blocks modules to core usage, supporting the pattern layer that precedes forcing-chain steps such as J-uniqueness and the phi-ladder.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.