extendPeriodic8
plain-language theorem explainer
The definition constructs an infinite boolean stream by repeating a given 8-element pattern indefinitely via modular indexing. Measurement and pattern theorists cite it to reduce sums and averages over streams to multiples of the finite window count Z(w). It is realized by a direct lambda that casts t % 8 into Fin 8 and applies the pattern.
Claim. Let $w :$ Fin$(8) → {true, false}$ be a finite pattern. The periodic extension is the stream $s : ℕ → {true, false}$ defined by $s(t) := w(t mod 8)$.
background
The Streams module treats periodic extensions and finite sums over boolean sequences. Here Pattern n is the type Fin n → Bool for a finite window of length n, while Stream is the type Nat → Bool for an infinite display. The local setting centers on lifting 8-bit windows to periodic streams so that measurement operations such as block sums become multiples of the window count Z_of_window. Upstream aliases in the Measurement layer re-export the same construction for use in averaging lemmas.
proof idea
The definition is a direct functional construction: it introduces a proof that 0 < 8 by decide, forms the Fin 8 index i = ⟨t % 8, Nat.mod_lt _ h8⟩, and returns w i. No external lemmas are applied beyond the standard library facts for Nat.mod_lt and Fin construction.
why it matters
This definition supplies the periodic streams required by downstream lemmas such as blockSumAligned8_periodic and observeAvg8_periodic_eq_Z, which establish that aligned 8-block sums equal k · Z(w) and that averaged observations recover Z. It thereby supports the DNARP equation in the measurement layer. Within the Recognition framework the fixed period 8 realizes the eight-tick octave (T7), allowing stream measurements to be reduced to finite pattern properties on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.