extendPeriodic8_eq_mod
The lemma asserts that the periodic extension of an 8-bit pattern at time t equals the pattern value at index t mod 8. Workers on stream models in Recognition Science cite it to reduce time-indexed expressions in periodic settings. The proof is a direct reflexivity after unfolding the modular definition of the extension.
claimFor a pattern $w :$ Fin $8$ $to$ Bool and natural number $t$, the periodic extension satisfies extendPeriodic8$(w,t) = w(t mod 8)$.
background
In the Streams module, a Pattern of length n is a function from Fin n to Bool, here specialized to length 8. The periodic extension extendPeriodic8 lifts such a window to an infinite stream by repeating the pattern every 8 steps via modular indexing. The module focuses on periodic extensions and finite sums over streams. Upstream, the abbrev extendPeriodic8 in Measurement delegates to PatternLayer, while the core def in Streams and Blocks explicitly constructs the stream as fun t => w (t mod 8).
proof idea
The proof is a one-line wrapper that applies reflexivity. Once the definition of extendPeriodic8 is unfolded, the left-hand side matches the right-hand side by construction of the modular index.
why it matters in Recognition Science
This simp lemma supports reductions involving the eight-tick octave (T7) in the forcing chain, where period 8 follows from the self-similar fixed point phi. It supplies the basic identity needed for stream manipulations in Recognition Science, though no downstream uses are recorded yet. The result closes a definitional gap for periodic pattern analysis.
scope and limits
- Does not generalize to patterns of length other than 8.
- Does not compute sums or Z functionals over the extended stream.
- Does not address uniqueness or convergence properties of the extension.
formal statement (Lean)
50@[simp] lemma extendPeriodic8_eq_mod (w : Pattern 8) (t : Nat) :
51 extendPeriodic8 w t = w ⟨t % 8, Nat.mod_lt _ (by decide)⟩ := by
proof body
Decided by rfl or decide.
52 rfl
53