observeAvg8
plain-language theorem explainer
Averaged observation function that returns the per-window mean of aligned block sums on Boolean streams. Researchers verifying discrete measurement invariants in Recognition Science cite it to link 8-tick patterns to the anchor integer Z. The declaration is a one-line wrapper delegating directly to the MeasurementLayer implementation.
Claim. For natural number $k$ and Boolean stream $s$, the averaged observation is defined by $observeAvg8(k,s) := blockSumAligned8(k,s)/k$, where the block sum is taken over aligned 8-tick windows.
background
The Measurement module re-exports eight-tick stream invariants together with a lightweight continuous-time scaffold. Stream is the alias for PatternLayer.Stream, i.e., Boolean sequences on which block sums are computed. Upstream structures supply the Z anchor (Masses.Anchor.Z) that maps rational charges to integers via quadratic forms on sectors, the J-cost convexity from PhiForcingDerived, and the spectral emergence of gauge content from SpectralEmergence. The eight-tick period originates in the T7 octave of the forcing chain.
proof idea
One-line wrapper that applies MeasurementLayer.observeAvg8 k s.
why it matters
The definition supplies the measurement map used by observeAvg8_periodic_eq_Z, which establishes the DNARP equation equating the average to Z_of_window on periodic extensions of an 8-bit window. It thereby connects the measurement layer to the anchor policy and the eight-tick octave (T7). The declaration closes the scaffold that lets downstream lemmas certify that periodic streams reproduce the integer Z without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.