Stream
plain-language theorem explainer
Stream introduces the type of infinite boolean sequences as maps from naturals to booleans. Measurement and Flight modules cite it to build cylinders, block sums, and vorticity proxies. The declaration is a direct type definition with no reduction steps.
Claim. A stream is a function $s : ℕ → {true, false}$.
background
The Streams module develops periodic extensions and finite sums over boolean sequences for measurement. This definition supplies the base type used by Cylinder and blockSumAligned8. Upstream results supply the active edge count A (IntegrationGap) and the convex J-cost minimization (PhysicsComplexityStructure).
proof idea
The declaration is a one-line type definition that sets Stream equal to the function type Nat → Bool.
why it matters
This type feeds the Measurement layer definitions of Cylinder and observeAvg8, which implement the eight-tick window sums required by the forcing chain at T7. It also supports the VorticityVoxel proxy in Flight. The module doc-comment frames the surrounding work on periodic extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.