Observable
plain-language theorem explainer
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.
Claim. An 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.