Measurement Block Sum Aligned8 Periodic

Aligned block sums

One can have a stream of bits, each either 0 or 1, that repeats every eight positions. The framework's declaration blockSumAligned8_periodic states a precise arithmetic fact: if you take any such repeating eight-bit window, sum the bits in the first eight positions, and then sum the bits in each subsequent aligned block of eight, the total after k blocks is exactly k times that first block's sum. In symbols, for any window w and any natural number k, the aligned block sum equals k times Z(w), where Z(w) counts the ones in the window. The lemma is proved in the machine-checked library of formal theorems, so the equality holds for every window and every k, with no hidden assumptions about the stream's content beyond its period.

The statement is a direct consequence of two simpler facts, also in the library. First, on any stream that matches an eight-bit window in its first eight positions, the sum of those first eight bits equals the window's count Z(w). Second, for a stream built by repeating that window forever, every aligned block of eight positions has the same sum Z(w). The aligned block sum lemma then follows by adding up k identical block sums, which is exactly k times Z(w). The proof is short and formal: the library's checker accepts it without any extra axioms beyond the standard logical foundations.

In Recognition Science, this lemma belongs to the measurement layer, the part of the framework that turns a stream of recognition events into numbers an observer can use. The declaration does not claim that any physical stream is actually periodic, nor that real measurements must come from such repeating windows. It only establishes a conditional identity: if a stream is the periodic extension of an eight-bit window, then the aligned block sum behaves in this exact multiplicative way. The lemma also does not say anything about the average observation per block, though a related result in the library shows that when the number of blocks is nonzero, that average equals Z(w). That averaged statement is separate and carries its own proof.

The practical consequence is a clean accounting rule for periodic streams: the total count over any number of aligned blocks is just the per-block count times the number of blocks. This is the kind of invariant that lets the measurement layer reason about long observations without enumerating every bit. It is a small but load-bearing piece of the framework's claim that recognition events can be counted and aggregated in a disciplined way.

/-- For `s = extendPeriodic8 w`, summing `k` aligned 8-blocks yields `k * Z(w)`. -/
lemma blockSumAligned8_periodic (w : Pattern 8) (k : Nat) :
    blockSumAligned8 k (extendPeriodic8 w) = k * Z_of_window w := by
  simpa [blockSumAligned8, extendPeriodic8, Z_of_window]
    using MeasurementLayer.blockSumAligned8_periodic (w:=w) k

/-- On any stream lying in the cylinder of an 8-bit window, the first block sum equals `Z`. -/
lemma firstBlockSum_eq_Z_on_cylinder (w : Pattern 8) {s : Stream}
    (hs : s ∈ Cylinder w) :
    subBlockSum8 s 0 = Z_of_window w := by
  simpa [subBlockSum8, Cylinder, Z_of_window]
    using MeasurementLayer.firstBlockSum_eq_Z_on_cylinder (w:=w) (s:=s) hs

/-- 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 does not assert that any physical stream is periodic. It does not claim that the average observation per block equals Z(w); that is a separate result with its own proof. It does not establish any property of streams that are not periodic extensions of an eight-bit window.

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: