Measurement Sub Block Sum8 Periodic Eq Z

A periodic window's stable count

A stream is a discrete record of events, here a sequence of bits. A window is a fixed-length slice of that stream. The lemma subBlockSum8_periodic_eq_Z concerns an eight-bit window that repeats forever, and it states a simple counting fact: in such a periodic stream, every aligned block of eight consecutive bits contains exactly the same number of ones as the original window. The count is written Z, a natural number.

The proof is a direct calculation. The declaration defines the sum of a sub-block as the number of ones in positions j*8 through j*8+7. For a stream built by repeating a window w, the lemma shows this sum equals Z_of_window w for any block index j. The argument unfolds the definitions and applies a previously established lemma about the first block. No measure theory, no probability, no approximation enters; it is an exact identity about finite sequences.

This lemma is part of a small family in the framework's measurement layer. A companion result shows that summing k aligned blocks of a periodic stream gives k times Z, and another shows that the average observation over k nonempty blocks equals Z. Together they say that a periodic eight-bit pattern presents a stable, reproducible count to any aligned measurement procedure.

In Recognition Science, the eight-tick cycle is a derived structure, and this lemma is a tool for working with streams that follow it. The framework models measurement as a map from a stream to an observation, and this lemma supports the claim that aligned observations of a periodic stream do not drift. It does not say anything about streams that are not periodic, nor about windows that are not aligned to the eight-bit boundary.

The practical consequence is that any code or argument that assumes a periodic eight-bit pattern yields a constant block count has a machine-checked warrant for that assumption. The lemma is a small but load-bearing piece of the measurement scaffold, and it is proved in the framework's library of formal theorems.

/-- For periodic extensions of an 8-bit window, each sub-block sums to `Z`. -/
lemma subBlockSum8_periodic_eq_Z (w : Pattern 8) (j : Nat) :
    subBlockSum8 (extendPeriodic8 w) j = Z_of_window w := by
  simpa [subBlockSum8, extendPeriodic8, Z_of_window]
    using MeasurementLayer.subBlockSum8_periodic_eq_Z (w:=w) j

What this page does not claim

The lemma says nothing about streams that are not periodic. It does not establish any property of windows that are not aligned to the eight-bit boundary. It does not derive the eight-tick cycle itself; it assumes such a pattern and analyzes its block sums.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: