extendPeriodic8_in_cylinder
plain-language theorem explainer
The periodic extension of any 8-bit pattern belongs to the cylinder set it generates. Researchers modeling streams or measures in Recognition Science cite this to verify that periodic repetition preserves the initial window. The proof unfolds the definitions and reduces membership via modular arithmetic on indices below 8.
Claim. Let $w$ map the set of indices $0$ to $7$ into the binary alphabet. Let $s$ be the function that repeats $w$ periodically with period 8. Then $s$ belongs to the cylinder set $C(w)$ consisting of all streams that agree with $w$ on the first eight positions.
background
In the Streams module a Pattern of length $n$ is a map from Fin $n$ to Bool, i.e., a finite binary window of length $n$. The Cylinder generated by such a window $w$ is the set of all infinite streams whose first $n$ bits exactly match $w$. The extendPeriodic8 operation builds the infinite stream by repeating the window via modular reduction: at position $t$ it returns the bit at index $t$ mod 8 inside $w$.
proof idea
The term proof introduces an arbitrary index $i$ from Fin 8, unfolds extendPeriodic8 and Cylinder, records that $i.val$ mod 8 equals $i.val$ by the standard lemma Nat.mod_eq_of_lt, and simplifies the membership predicate to obtain equality.
why it matters
The lemma supplies the basic membership fact needed to treat periodic extensions as legitimate elements of cylinder sets in the stream layer. It directly supports the eight-tick octave (T7) of the forcing chain by confirming that period-8 repetition stays inside the defining window. No downstream uses are recorded yet, so the result functions as a foundational closure for later summation and measure constructions on streams.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.