Stream
plain-language theorem explainer
Boolean streams are introduced as the base type for infinite binary sequences in the streams and measurement layers. Researchers modeling discrete observations, block sums, and cylinders over eight-tick windows would cite this definition when building pattern recognition structures. It is supplied as a direct type definition with no further axioms or structure.
Claim. A stream is a function $S : ℕ → {true, false}$ that represents an infinite sequence of boolean values indexed by natural numbers.
background
The Streams.Blocks module supplies the pattern and measurement layers, including streams, finite windows of length n, and aligned block sums over eight-tick periods; the file ports the PatternLayer/MeasurementLayer cluster. Upstream structures supply the surrounding context: IntegrationGap.A fixes the active edge count per tick at 1, while PhysicsComplexityStructure.of records that J-cost minimization is convex with local 8-tick dynamics updating at most eight neighbors. SpectralEmergence.of and PhiForcingDerived.of supply the gauge and J-cost scaffolding that later measurement lemmas rely upon.
proof idea
This is a direct definition that equates the stream type with the function space Nat → Bool; no lemmas or tactics are applied.
why it matters
The definition supplies the common type used by the Measurement module's own Stream abbrev and by the 26 downstream declarations that include blockSumAligned8, Cylinder, firstBlockSum_eq_Z_on_cylinder, observeAvg8, subBlockSum8, and sumFirst. It therefore anchors the eight-tick octave (T7) constructions that appear in the Recognition framework and in the Flight.Medium.VorticityVoxel proxy. The module doc-comment states that the file ports the PatternLayer/MeasurementLayer cluster, closing the interface between the foundation layer and concrete measurement statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.