blockSumAligned8_periodic
The lemma states that summing k aligned 8-blocks on the periodic extension of any 8-bit pattern w equals k times the number of ones in w. Researchers modeling periodic stream observations or deriving averaged measurements in Recognition Science cite this for the DNARP relation. The proof works by showing each sub-block sum is constantly Z(w) via the periodic sub-block lemma, then applying Finset cardinality and constant-sum rules to scale by k.
claimLet $w$ be a finite pattern of length 8 and let $k$ be a natural number. For the infinite stream obtained by repeating $w$ periodically, the sum of the first $k$ aligned 8-blocks equals $k$ times the integer count of ones in $w$.
background
In the Streams.Blocks module, a Pattern of length n is a finite window given by a function from Fin n to Bool. Z_of_window counts the number of true entries in such a window, yielding an integer that later anchors mass formulas. extendPeriodic8 repeats the 8-bit window indefinitely to produce a bi-infinite stream, while blockSumAligned8 totals the ones across k consecutive aligned 8-blocks starting at multiples of 8.
proof idea
The tactic proof first unfolds blockSumAligned8, then uses subBlockSum8_periodic_eq_Z to prove every sub-block sum equals the constant Z_of_window w. It next invokes the cardinality of Fin k together with the Finset sum-of-constants identity to obtain the factor k, and finally composes the two equalities via congrArg and transitivity.
why it matters in Recognition Science
This lemma supplies the key step for observeAvg8_periodic_eq_Z, which states that the per-window averaged observation on a periodic 8-stream equals Z(w). It thereby realizes the DNARP equation at the eight-tick scale and connects directly to the T7 octave in the forcing chain, where periodic repetition of length 2^3 appears in measurement averaging. The result closes one link between stream observations and the integer Z functional used in anchor relations.
scope and limits
- Does not apply to streams that are not periodic extensions of an 8-bit pattern.
- Does not hold for windows whose length differs from 8.
- Assumes the blocks are strictly aligned at multiples of 8; overlapping or shifted sums are excluded.
- Treats k = 0 as the trivial zero sum; no separate non-zero hypothesis is imposed.
formal statement (Lean)
123lemma blockSumAligned8_periodic (w : Pattern 8) (k : Nat) :
124 blockSumAligned8 k (extendPeriodic8 w) = k * Z_of_window w := by
proof body
Tactic-mode proof.
125 classical
126 unfold blockSumAligned8
127 have hconst : ∀ j : Fin k, subBlockSum8 (extendPeriodic8 w) j.val = Z_of_window w := by
128 intro j; simpa using subBlockSum8_periodic_eq_Z w j.val
129 have hsum : (∑ _j : Fin k, Z_of_window w) = k * Z_of_window w := by
130 simpa using
131 (Finset.card_univ : Fintype.card (Fin k) = k) ▸
132 (by simpa using (Finset.sum_const_natural (s:=Finset.univ) (a:=Z_of_window w)))
133 have hmap := congrArg (fun f => ∑ j : Fin k, f j) (funext hconst)
134 simpa using hmap.trans hsum
135
136/-- Averaged (per‑window) observation equals `Z` on periodic extensions. -/