Pith. sign in
module module high

IndisputableMonolith.Measurement

show as:
view Lean formalization →

The Measurement module supplies the Boolean stream definitions, patterns, cylinders, and aligned block sums that implement the measurement layer. It would be cited by any work on periodic stream analysis or the Gap45 gating rule. The module is a port of the PatternLayer and MeasurementLayer cluster and contains only definitions and supporting lemmas.

claimBoolean streams $\text{Stream} \subseteq \{0,1\}^{\mathbb{Z}}$ equipped with periodic extension, window sums $Z_{\text{window}}$, cylinders, and 8-beat aligned block sums for measurement.

background

The module imports Streams (periodic extension and finite sums) and Streams.Blocks (patterns, windows, and aligned block sums). It defines the core objects Stream, Pattern, Z_of_window, Cylinder, extendPeriodic8, sumFirst, subBlockSum8, blockSumAligned8, observeAvg8 and the lemmas firstBlockSum_eq_Z_on_cylinder, subBlockSum8_periodic_eq_Z, blockSumAligned8_periodic. These constructs formalize the measurement layer that operates on Boolean streams.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the measurement primitives required by Gap45.Beat, which encodes the rule that experience is required exactly when the plan period is not a multiple of 8. It thereby implements the Source.txt policy that 8-beat alignment disables Gap45 gating.

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)