subBlockSum8_periodic_eq_Z
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply to streams that are not periodic extensions of an 8-bit pattern.
- Does not generalize the equality to block lengths other than 8.
- Does not compute a numerical value for Z beyond the window sum definition.
- Does not address starting positions that are not multiples of 8.
Lean usage
have h : subBlockSum8 (extendPeriodic8 w) j = Z_of_window w := subBlockSum8_periodic_eq_Z w jformal statement (Lean)
99lemma subBlockSum8_periodic_eq_Z (w : Pattern 8) (j : Nat) :
100 subBlockSum8 (extendPeriodic8 w) j = Z_of_window w := by
proof body
Tactic-mode proof.
101 classical
102 unfold subBlockSum8 Z_of_window extendPeriodic8
103 have hmod : ∀ i : Fin 8, ((j * 8 + i.val) % 8) = i.val := by
104 intro i
105 have hi : i.val < 8 := i.isLt
106 have h0 : (j * 8) % 8 = 0 := by simpa using Nat.mul_mod j 8 8
107 calc
108 (j * 8 + i.val) % 8
109 = ((j * 8) % 8 + i.val % 8) % 8 := by
110 simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc, Nat.mul_comm]
111 using (Nat.add_mod (j*8) i.val 8)
112 _ = (0 + i.val) % 8 := by simpa [h0, Nat.mod_eq_of_lt hi]
113 _ = i.val % 8 := by simp
114 _ = i.val := by simpa [Nat.mod_eq_of_lt hi]
115 have hfun :
116 (fun i : Fin 8 => (if w ⟨(j*8 + i.val) % 8, Nat.mod_lt _ (by decide)⟩ then 1 else 0))
117 = (fun i : Fin 8 => (if w i then 1 else 0)) := by
118 funext i; simp [hmod i]
119 have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
120 simpa using this
121
122/-- For `s = extendPeriodic8 w`, summing `k` aligned 8‑blocks yields `k * Z(w)`. -/