pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Measurement

show as:
view Lean formalization →

This module defines boolean streams together with periodic extensions and aligned block sums for the measurement layer. Researchers formalizing observation of 8-tick patterns in Recognition Science would cite it when building gating or averaging lemmas. It is a definition module with no proofs, importing stream primitives from upstream and exposing them for downstream use.

claimBoolean streams $S : ℤ → {0,1}$ equipped with periodic extension over period 8, window functions, cylinder sets, and aligned block sums such as blockSumAligned8 and observeAvg8.

background

The module sits in the measurement layer and imports Streams (periodic extension and finite sums) together with Streams.Blocks (patterns, windows, and aligned block sums). It introduces sibling definitions including Stream, Pattern, Z_of_window, Cylinder, extendPeriodic8, sumFirst, subBlockSum8, blockSumAligned8, observeAvg8, and the three equality lemmas firstBlockSum_eq_Z_on_cylinder, subBlockSum8_periodic_eq_Z, blockSumAligned8_periodic. These realize the eight-tick octave structure for exact alignment of finite observations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the measurement primitives that feed the Gap45 gating rule. Downstream Gap45.Beat applies these definitions to enforce that experience is required exactly when the plan period is not a multiple of 8, capturing the policy that 8-beat alignment disables Gap45 gating. It thereby implements the periodic measurement step required by the eight-tick octave in the forcing chain.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (17)