sumFirst8_extendPeriodic_eq_Z
plain-language theorem explainer
Lemma establishing that the sum of the first eight bits in a periodically extended 8-bit pattern equals the integer count of ones in the original window. Block decomposition arguments in stream models within Recognition Science cite it to reduce infinite periodic sums to finite window counts. The tactic proof unfolds the sum and extension definitions, verifies index invariance under mod 8, equates the indicator functions by extensionality, and concludes via congruence on the finite sum operator.
Claim. Let $w$ be a pattern of length 8. Then the sum of the first eight entries of the periodic extension of $w$ equals the number of true entries in $w$.
background
In the Streams module, a pattern of length $n$ is a map from Fin $n$ to Bool representing a finite binary window. The functional $Z$ counts the number of true entries by summing the corresponding indicators over the window. Periodic extension repeats the window indefinitely to produce a stream, while sumFirst extracts the partial sum of the first $m$ bits from such a stream. The module treats periodic extensions and finite sums over streams. This lemma connects the finite window count directly to the stream sum for the case $m=8$ under periodic repetition of length 8. It relies on the periodic extension and sum operations defined in the Measurement module.
proof idea
The tactic proof begins with classical, then unfolds sumFirst, $Z$ of window, and the periodic extension. It proves that $i.val$ mod 8 equals $i.val$ for each $i$ in Fin 8 by Nat.mod_eq_of_lt. Function extensionality and simplification establish that the two indicator maps agree. Congruence is applied to the summation operator over Fin 8 to equate the sums.
why it matters
This result supports decomposition of streams into 8-tick blocks, consistent with the eight-tick octave in the forcing chain. It is invoked directly by the matching lemma in the Streams.Blocks submodule for further stream manipulations. In the Recognition framework it closes a consistency step between periodic extensions and window functionals, aiding treatment of periodic structures without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.