subBlockSum8_periodic_eq_Z
plain-language theorem explainer
For any 8-bit pattern w, every aligned 8-block in its periodic extension sums to the integer Z(w) counting the true entries in w. Stream measurement arguments cite this when reducing periodic block sums to fixed window counts. The tactic proof unfolds the definitions, proves modular index identities via add_mod and mul_mod, then applies congruence to the finite sum.
Claim. Let $w$ be a map from the set of 8 indices to booleans. Let $s$ be the infinite stream obtained by repeating $w$ periodically. For every natural number $j$, the sum of the eight consecutive values of $s$ starting at position $8j$ equals the number of true values in $w$.
background
The Streams.Blocks module develops the pattern and measurement layers for streams and aligned block sums, porting the PatternLayer/MeasurementLayer cluster. A pattern of length 8 is a function from the finite 8-element index set to boolean values. The window functional Z counts the number of true entries by summing 1 or 0 over those indices. The periodic extension repeats the pattern indefinitely to form an infinite stream. The sub-block sum extracts the total over any eight consecutive positions whose start index is a multiple of 8.
proof idea
Unfold subBlockSum8, Z_of_window and extendPeriodic8. Establish the modular identity ((j * 8 + i.val) % 8) = i.val for each Fin 8 by applying add_mod, mul_mod, add_comm, add_assoc and Nat.mod_eq_of_lt. Show the bit-extraction map is identical to the original pattern via funext and simp. Conclude by congruence of the summation over Fin 8.
why it matters
This lemma is invoked by blockSumAligned8_periodic to scale the single-block equality to k blocks, yielding k * Z(w). It supports the eight-tick octave (T7) in the forcing chain by guaranteeing constant sums over periodic 8-cycles, which feeds the self-similar fixed point and the derivation of three spatial dimensions. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.