Measurement First Block Sum Eq Z On Cylinder

The first block sum

In the framework's measurement layer, a stream is a discrete record of events, a sequence of bits. A window is a finite pattern of eight bits. The lemma firstBlockSum_eq_Z_on_cylinder states: if a stream lies in the cylinder of an 8-bit window (meaning its first eight bits match that window exactly), then the sum of those first eight bits equals the window's own count of ones, written Z(w). The proof is direct: it unfolds the definitions of block sum, cylinder membership, and the count function, then applies a pre-existing invariant from the measurement layer.

The statement is a formal identity, not an empirical claim. It says nothing about what real streams exist, only that for any stream satisfying the cylinder condition, the first block sum is forced to equal Z(w). The lemma is one of several in the same module: a companion lemma guarantees that for periodic extensions of an 8-bit window, every sub-block sums to Z(w), and a third lemma extends this to aligned sums over k blocks, giving k times Z(w). These are the building blocks of the framework's averaged observation map, which reads a stream through aligned 8-tick windows.

In Recognition Science, the framework models measurement as a forced operation on such streams, and this lemma is the first step in that model: it pins down what a single aligned observation must return. It does not, however, claim anything about the eight-tick cycle's origin, the golden ratio, or the forcing chain that derives constants like hbar and G. Those results live in other modules and are not touched by this lemma. The lemma is a local, mechanical fact about counting within a fixed window, not a statement about the physical meaning of the count.

The practical consequence is that the framework's measurement scaffold can rely on a checked invariant: when a stream matches a window, the first block sum is exactly the window's count, with no averaging, no error term, and no dependence on later bits. This makes the scaffold's CQ score, which combines listening rate, operations per second, and a coherence measure, well-defined on the streams it accepts. The lemma is a small gear in a larger machine, but it is a gear that turns without slipping.

/-- 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

/-- 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

What this page does not claim

This lemma does not derive the golden ratio, the eight-tick cycle, or any physical constant. This lemma does not claim that any particular stream exists in reality, only that if one matches a window, the sum is forced. This lemma does not establish any property of the framework's continuous-time measurement scaffold beyond the discrete 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: