pith. sign in
module module high

IndisputableMonolith.Measurement

show as:
view Lean formalization →

The Measurement module defines boolean streams, patterns, window sums, cylinders, and aligned block operations for the measurement layer. It would be cited by any proof that needs periodic 8-beat extensions or finite block sums in the Recognition framework. This is a definition module that ports the PatternLayer and MeasurementLayer cluster with no proofs inside.

claimBoolean streams $S : \mathbb{Z} \to \{0,1\}$, pattern objects, cylinder windows with associated $Z$ sums, periodic extensions of period 8, and aligned block sums together with their averages.

background

The module imports the Streams file, whose doc-comment states it supplies periodic extension and finite sums, and the Streams.Blocks file, whose doc-comment states it ports the PatternLayer/MeasurementLayer cluster. These imports supply the basic objects for boolean streams used by the measurement layer. The local setting is therefore the construction of periodic boolean sequences and their block-wise measurements, with emphasis on 8-tick alignment.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module is imported by Gap45.Beat, whose doc-comment states it defines the Gap45 gating rule that experience is required exactly when the plan period is not a multiple of 8, capturing the Source.txt policy that 8-beat alignment disables Gap45 gating. It therefore supplies the stream primitives required for that gating construction.

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)