extendPeriodic8_zero
plain-language theorem explainer
extendPeriodic8_zero asserts that the periodic extension of any 8-bit pattern w returns the zeroth entry of w when evaluated at time zero. Authors proving summation identities or periodicity lemmas over streams in the Recognition Science setting cite it to discharge base cases at multiples of the period. The argument is a one-line simp wrapper that unfolds the modular indexing in the extension definition.
Claim. For any map $w : {Fin} 8 → {Bool}$, the periodic extension satisfies $(extendPeriodic8 w)(0) = w(0)$.
background
The Streams module defines finite patterns and their periodic extensions to support repeating sequences and finite sums. Pattern n is the type Fin n → Bool, a window of n bits. extendPeriodic8 w produces the infinite stream that repeats w by sending each integer t to w(t mod 8), with the Fin 8 index constructed via Nat.mod_lt.
proof idea
The proof is a one-line simp wrapper that applies the definition of extendPeriodic8; the modular index at t = 0 reduces directly to the zero element of Fin 8.
why it matters
The lemma supplies a simp rule for the base case of periodic extensions inside the Streams module, which implements the eight-tick octave structure (T7) of the forcing chain. It supports downstream algebraic work on streams even though no explicit users are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.