extendPeriodic8_period
The lemma shows that the periodic extension of any 8-element pattern repeats exactly every 8 steps. Modelers of discrete eight-tick streams in Recognition Science cite it to shift time indices by multiples of the octave without altering stream values. The tactic proof unfolds the extension, applies modular arithmetic to confirm the residue class is invariant under addition of 8, and equates the corresponding Fin 8 indices.
claimLet $w : [0,7] → {0,1}$ be any finite window of length 8 and let $t ∈ ℕ$. Then the periodic extension of $w$ satisfies $w^♯(t+8) = w^♯(t)$.
background
In the Streams module a Pattern n is defined as a map Fin n → Bool, i.e., a finite binary window of length n. The periodic extension extendPeriodic8 repeats this window indefinitely, producing a bi-infinite stream whose value at any integer time is read from the window via modular reduction. The module focuses on periodic extensions together with finite sums over such streams. The lemma depends on the abbrev extendPeriodic8 imported from Measurement, which itself aliases the core definition in PatternLayer.
proof idea
The tactic proof first applies dsimp to unfold extendPeriodic8, exposing the modular index computation. It then rewrites with Nat.add_mod and simp to obtain (t+8) % 8 = t % 8. A Fin.mk_eq_mk step equates the two Fin 8 elements whose underlying values are identical, after which a single rw closes the goal.
why it matters in Recognition Science
The result supplies the basic periodicity property required by the eight-tick octave (T7) in the UnifiedForcingChain. It ensures that stream-based models of J-cost minimization and spectral emergence remain consistent under time shifts that are multiples of the fundamental period. Although no downstream declarations are listed, the lemma is a prerequisite for any later work that manipulates periodic 8-bit patterns in measurement or complexity structures.
scope and limits
- Does not establish periodicity for windows whose length differs from 8.
- Does not treat non-periodic or aperiodic extensions of patterns.
- Does not derive any relation to J-cost, phi-ladder masses, or physical constants.
- Does not address convergence or summation properties of the resulting streams.
formal statement (Lean)
54lemma extendPeriodic8_period (w : Pattern 8) (t : Nat) :
55 extendPeriodic8 w (t + 8) = extendPeriodic8 w t := by
proof body
Tactic-mode proof.
56 dsimp [extendPeriodic8]
57 have hmod : (t + 8) % 8 = t % 8 := by
58 rw [Nat.add_mod]
59 simp
60 have h8 : 0 < 8 := by decide
61 have hfin : (⟨(t + 8) % 8, Nat.mod_lt _ h8⟩ : Fin 8)
62 = ⟨t % 8, Nat.mod_lt _ h8⟩ := by
63 apply Fin.mk_eq_mk.mpr
64 exact hmod
65 rw [hfin]
66
67/-- Sum of the first `m` bits of a stream. -/