pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

extendPeriodic8

show as:
view Lean formalization →

Periodic extension of an 8-bit pattern repeats the window indefinitely by indexing modulo 8. Measurement lemmas on block sums and averages cite this operator to reduce periodic streams to the window sum Z. The definition is a direct re-export of the Streams implementation.

claimFor a pattern $w : Pattern 8$, the map extendPeriodic8$(w)$ produces the stream $s$ satisfying $s(t) = w(t mod 8)$ for all natural numbers $t$.

background

The module re-exports eight-tick stream invariants for the measurement layer. A Pattern 8 is a function from Fin 8 to the base type; Z_of_window extracts its invariant sum. The periodic extension constructs an infinite Stream by cycling the pattern via modular reduction. Upstream structures from PhiForcingDerived supply the J-cost convexity and from SpectralEmergence the gauge content that fix the 8-tick period.

proof idea

One-line alias that forwards to the Streams.extendPeriodic8 definition, which builds the stream by t % 8 indexing into the input pattern.

why it matters in Recognition Science

This operator supplies the periodic streams required by blockSumAligned8_periodic and observeAvg8_periodic_eq_Z, which establish that averages equal the window invariant Z. It realizes the eight-tick octave (T7) from the forcing chain, enabling reduction of observations to discrete pattern sums in the Measurement layer.

scope and limits

formal statement (Lean)

  29abbrev extendPeriodic8 := PatternLayer.extendPeriodic8

proof body

Definition body.

  30
  31/-- Sum of the first `m` bits of a stream. -/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.