extendPeriodic8
plain-language theorem explainer
The definition builds an infinite Boolean stream by repeating a fixed 8-element pattern. Measurement lemmas cite it to reduce block sums and averages on periodic streams to multiples of the pattern's one-count. Implementation indexes the pattern at each time step via modular reduction.
Claim. For a pattern $w :$ Fin $8$ $→$ Bool, the periodic extension is the stream $s :$ Nat $→$ Bool defined by $s(t) = w(t$ mod $8)$.
background
Streams.Blocks handles pattern and measurement layers for streams, windows, and aligned block sums, porting the PatternLayer and MeasurementLayer cluster. Pattern n is a finite window of length n, realized as a map Fin n $→$ Bool. Stream is an infinite Boolean sequence, realized as a map Nat $→$ Bool. This definition supplies the periodic repetition of an 8-bit window that supports reduction of infinite measurements to finite pattern properties.
proof idea
The definition is a direct functional extension: for input pattern w and time t it forms the index i = t mod 8 via Nat.mod_lt and returns w i.
why it matters
This definition supports the lemmas blockSumAligned8_periodic, observeAvg8_periodic_eq_Z and subBlockSum8_periodic_eq_Z, which recover k times Z(w) or the window count itself from aligned sums and averages. It realizes the eight-tick octave (T7) of the forcing chain, enabling collapse of stream observations to finite pattern counts in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.