sumFirst8_extendPeriodic_eq_Z
The lemma equates the sum of the first eight terms in the periodic extension of an 8-bit pattern to the integer count Z of ones inside the original window. Workers on stream alignments, cylinder sets, or block sums in the Recognition Science measurement layer would cite this identity to collapse periodic extensions back to finite windows. The proof is a short tactic sequence that unfolds the three definitions, verifies modular reduction on Fin 8, and applies congruence to the summation operator.
claimFor a pattern $w$ of length 8, let $Z(w)$ be the number of true entries in $w$. Let $s$ be the periodic extension of $w$ with period 8. Then the sum of the first eight values of $s$ equals $Z(w)$.
background
In the PatternLayer a Pattern n is defined as a function Fin n → Bool, i.e., a finite binary window of length n. Z_of_window counts the true entries by summing the corresponding indicators over Fin n. The module develops streams, windows, and aligned block sums inside the eight-tick octave structure of Recognition Science. Upstream results supply the fundamental tick as the RS time quantum and the J-cost and ledger-factorization structures that support the forcing chain from T0 to T8.
proof idea
The proof unfolds sumFirst, Z_of_window and extendPeriodic8. It establishes that i.val % 8 = i.val for every i : Fin 8 by Nat.mod_eq_of_lt. It then shows the two indicator functions coincide by funext and simplification. Finally it applies congrArg to the summation operator and finishes with simpa.
why it matters in Recognition Science
The identity supports block-sum alignments in the measurement layer and is used by the parent lemma sumFirst8_extendPeriodic_eq_Z in the Streams module. It instantiates the eight-tick period (T7) by showing that periodic extension preserves the Z-count for the fundamental octave. The result closes a reduction step from infinite streams to finite windows inside the Recognition framework.
scope and limits
- Does not generalize to windows of length other than 8.
- Does not apply to non-periodic extensions.
- Does not compute explicit Z values for concrete patterns.
Lean usage
lemma use_site (w : Pattern 8) : sumFirst 8 (extendPeriodic8 w) = Z_of_window w := sumFirst8_extendPeriodic_eq_Z wformal statement (Lean)
50lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) :
51 sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
proof body
Tactic-mode proof.
52 classical
53 unfold sumFirst Z_of_window extendPeriodic8
54 have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by
55 intro i; exact Nat.mod_eq_of_lt i.isLt
56 have hfun :
57 (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ (by decide)⟩ then 1 else 0))
58 = (fun i : Fin 8 => (if w i then 1 else 0)) := by
59 funext i; simp [hmod i]
60 have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
61 simpa using this
62
63end PatternLayer
64
65namespace MeasurementLayer
66
67open scoped BigOperators
68open Finset PatternLayer
69
70/-- Sum of one 8‑tick sub‑block starting at index `j*8`. -/