Stream
plain-language theorem explainer
The declaration supplies a re-export of the boolean stream type (functions from naturals to booleans) for the measurement layer. Workers on cylinder sets, block sums, or eight-tick invariants cite this alias to keep measurement code independent of the core streams module. It is realized as a one-line abbreviation delegating directly to PatternLayer.Stream.
Claim. The type of boolean streams is the set of functions $f : {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,
background
The Measurement module re-exports eight-tick stream invariants for use in pattern matching and observation. Upstream, Streams.Stream is defined as the type Nat → Bool, described as a boolean stream serving as an infinite display. PatternLayer.Stream is the immediate source of the alias. Related upstream structures include J-cost minimization (strictly convex with minimum at x=1), phi-forcing, spectral emergence of gauge content and three generations, and nuclear density tiers on the phi-ladder. The local setting is a lightweight scaffold for continuous-time measurement (CQ score) built on these discrete streams.
proof idea
One-line wrapper that aliases PatternLayer.Stream, which itself delegates to the core Streams.Stream definition Nat → Bool.
why it matters
This supplies the stream type consumed by downstream declarations including Cylinder, blockSumAligned8, observeAvg8, subBlockSum8, firstBlockSum_eq_Z_on_cylinder, and VorticityVoxel. It supports the eight-tick octave (T7) and the measurement layer's use of periodic windows on the phi-ladder. It fills the basic data-type slot required by the Recognition Composition Law applications and the cylinder-set lemmas that equate block sums to Z_of_window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.