Observable
Observable defines a map from state space S to a Measurement of type α. Researchers formalizing RS measurement protocols cite this when every extracted quantity must carry explicit protocol, window, and uncertainty data. The definition is a direct type abbreviation that composes the state-to-value function with the Measurement record.
claimAn observable is a function from states of type $S$ to a measurement of quantity type $α$, where each measurement record contains a value, optional time window, protocol, optional uncertainty, and notes.
background
The RS-Native Measurement Framework supplies a Lean-first scaffold for Recognition Science. Measurements are structured records that attach a protocol and optional metadata to any value α, keeping SI calibration outside the core. The module sets τ₀ = 1 and treats ticks, voxels, and coherence as primitive, with concrete observables deferred to Catalog files.
proof idea
This is a direct type abbreviation. It aliases the function type S → Measurement α with no lemmas or tactics applied.
why it matters in Recognition Science
The definition supplies the Observable extraction mechanism required by recognition_forcing_complete and recognition_is_cost_structure. It is used in OptimalConfig for astrophysical limits and in falsifier_K_gate_mismatch checks. Within the framework it enforces explicit protocols, supporting the RecognitionForcing structure that encodes recognition as a cost structure and the eight-tick octave at D = 3.
scope and limits
- Does not define concrete observables for specific physical quantities.
- Does not incorporate external SI or CODATA calibrations.
- Does not enforce validation rules or falsifiers inside the type.
- Does not restrict the choice of state type S or value type α.
formal statement (Lean)
162abbrev Observable (S α : Type) : Type := S → Measurement α
proof body
Definition body.
163
164/-! ## Tagged quantities (type-safe units) -/
165
166/-- A real-valued quantity tagged with a unit/semantic label. -/