Measurement Observe Avg8 Periodic Eq Z

Averaged observations

An observation in this setting is a count. The framework's measurement layer works with streams of bits, a stream being an infinite sequence of 0s and 1s. A window is any finite block of eight consecutive bits. The count of 1s inside such a window is written Z. The lemma observeAvg8_periodic_eq_Z says this: take any eight-bit window, repeat it forever to make a periodic stream, and average the counts over any number of complete eight-tick blocks. The result is exactly Z, the count in the original window. The averaging changes nothing because every block is identical to the first.

The statement carries one condition: the number of blocks k must be nonzero. Averaging over zero blocks is undefined, so the lemma excludes it. The proof is a short chain of equalities, each step a definition unfolding. The framework's machine-checked library of formal theorems records this as a lemma, not a postulate. It follows from the definitions of periodic extension, block sums, and the averaging function.

In Recognition Science, this lemma is a small but load-bearing piece of the measurement layer. The framework models recognition events as discrete ticks, and an eight-tick cycle is a structural consequence of the forcing chain. This lemma confirms that a periodic eight-tick pattern is stable under the natural measurement operation: averaging over aligned blocks returns the same count, with no drift and no correction term. It is the kind of invariant that a theory of measurement needs before it can talk about anything like a stable observable.

The lemma does not say that all streams are periodic, nor that every observation averages to Z. It applies only to streams built by repeating a single eight-bit window, and only to blocks aligned to that window's boundaries. It also does not assign physical meaning to Z; it is a count of 1s in a window, nothing more. The result is a formal identity about a defined operation, not an empirical claim about the world.

/-- DNARP Eq.: on periodic extensions of an 8-bit window, the averaged observation equals `Z`. -/
lemma observeAvg8_periodic_eq_Z {k : Nat} (hk : k ≠ 0) (w : Pattern 8) :
    observeAvg8 k (extendPeriodic8 w) = Z_of_window w := by
  simpa [observeAvg8, extendPeriodic8, Z_of_window]
    using MeasurementLayer.observeAvg8_periodic_eq_Z (k:=k) (hk:=hk) (w:=w)

/-- DNARP Eq.: on periodic extensions of an 8-bit window, the averaged observation equals `Z`. -/
lemma observeAvg8_periodic_eq_Z {k : Nat} (hk : k ≠ 0) (w : Pattern 8) :
    observeAvg8 k (extendPeriodic8 w) = Z_of_window w := by
  simpa [observeAvg8, extendPeriodic8, Z_of_window]
    using MeasurementLayer.observeAvg8_periodic_eq_Z (k:=k) (hk:=hk) (w:=w)

What this page does not claim

The lemma does not claim that all streams are periodic. The lemma does not assign physical meaning to the count Z. The lemma does not cover averaging over blocks that are not aligned to the 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: