extendPeriodic8
plain-language theorem explainer
Periodic extension of an 8-bit pattern repeats the window indefinitely by indexing modulo 8. Measurement lemmas on block sums and averages cite this operator to reduce periodic streams to the window sum Z. The definition is a direct re-export of the Streams implementation.
Claim. For a pattern $w : Pattern 8$, the map extendPeriodic8$(w)$ produces the stream $s$ satisfying $s(t) = w(t mod 8)$ for all natural numbers $t$.
background
The module re-exports eight-tick stream invariants for the measurement layer. A Pattern 8 is a function from Fin 8 to the base type; Z_of_window extracts its invariant sum. The periodic extension constructs an infinite Stream by cycling the pattern via modular reduction. Upstream structures from PhiForcingDerived supply the J-cost convexity and from SpectralEmergence the gauge content that fix the 8-tick period.
proof idea
One-line alias that forwards to the Streams.extendPeriodic8 definition, which builds the stream by t % 8 indexing into the input pattern.
why it matters
This operator supplies the periodic streams required by blockSumAligned8_periodic and observeAvg8_periodic_eq_Z, which establish that averages equal the window invariant Z. It realizes the eight-tick octave (T7) from the forcing chain, enabling reduction of observations to discrete pattern sums in the Measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.