Measurement

Measurement as recognition

Measurement is the act of turning an ongoing stream of events into a number. In the Recognition Science framework, that stream is a ledger, a discrete record of recognition events, and the number is a count of events inside a fixed window. The framework's measurement layer builds on an eight-tick cycle, a repeating pattern of eight steps that the underlying theory derives from its cost function. The core objects are simple: a stream is an infinite sequence of bits, and a pattern is a finite window of length n drawn from that stream. The count of ones in that window is written Z, and a cylinder is the set of all streams that share a given window.

The lemmas establish what happens when you count over aligned blocks. If a stream lies in the cylinder of an 8-bit window, the first block sum equals Z, the count for that window. For a periodic extension, a stream built by repeating the same 8-bit window forever, every sub-block sums to Z, and summing k aligned blocks gives k times Z. The averaged observation over k blocks, when k is not zero, also equals Z. These are not empirical claims; they are proved facts about the definitions, each one a theorem in the machine-checked library of formal theorems.

The measurement layer also includes a scaffold for continuous time. A measurement map carries a positive time constant T and a function that turns a state history into an observation. The lightweight helper avg samples the state at the midpoint of each interval. The coherence quotient, or CQ score, combines three numbers: listens per second, operations per second, and a coherence value between 0 and 1. The score is zero when operations per second is zero, and otherwise it is the ratio of listens to operations, scaled by coherence.

What this establishes in plain language is that counting works. If the world presents itself as a stream of recognition events, and you have agreed on an 8-bit window, then averaging over aligned blocks recovers the window's count exactly, with no drift and no noise. The periodic case is the clean one: repeat the window, and every block tells you the same Z. That is the sense in which measurement here is forced, not chosen. The framework does not claim this is how laboratory instruments work; it claims this is what measurement is when reality keeps a discrete ledger.

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

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

This module does not define how laboratory instruments measure physical quantities. The CQ score is a scaffold, not a derived physical observable. No claim here connects the eight-tick cycle to empirical measurement data.

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: