Observable
plain-language theorem explainer
Observable supplies the type of protocol-tagged maps from states S to values in α inside the RS-native measurement scaffold. Workers on recognition forcing theorems or observability limits cite it when they need to distinguish ledger extractions that carry explicit protocols and uncertainty. The declaration is a direct type abbreviation with no further reduction.
Claim. An observable on state space $S$ with value type $α$ is any function $S →$ Measurement$(α)$, where each Measurement record holds a value in $α$, an optional time window, a protocol, optional uncertainty, and a list of notes.
background
The module supplies a Lean-first measurement scaffold for Recognition Science whose primitives are ticks, voxels, coherence, and actualization with $τ_0 = 1$; SI/CODATA values remain external calibration. Measurement is the structure whose fields are value : α, window : Option Window, protocol : Protocol, uncertainty : Option Uncertainty, and notes : List String, with a map operation that preserves the auxiliary data. Upstream, RecognitionForcing.Observable is the simpler record value : S → ℝ; the present abbreviation lifts that record into the protocol-carrying form required by the measurement framework.
proof idea
One-line type abbreviation that directly composes the state-to-value function with the Measurement structure already defined in the same module.
why it matters
The definition is the observable type consumed by recognition_forcing_complete (which asserts that every distinguishing observable induces a RecognitionStructure) and by OptimalConfig in astrophysics. It also appears in the K-gate falsifier and in the Hamiltonian construction. It therefore supplies the concrete bridge between the cost-structure theorem recognition_is_cost_structure and the protocol-aware observables demanded by the RS measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.