Observable
plain-language theorem explainer
An observable on a state space is simply a real-valued map from states. Anyone proving that measurement forces recognition structure cites this carrier type. It is a bare structure definition with a single field, no proof obligations.
Claim. An observable on a state space $S$ is a function $\mathrm{value}: S \to \mathbb{R}$ assigning a real measurement to each state.
background
The module Recognition Structure Necessity shows that any framework that extracts observables must already contain a recognition structure: the capacity to distinguish and identify states. The strategy is three-step: measurable quantities imply distinguishable states; distinction requires comparison; comparison without an external reference is self-recognition. The Meta Principle then rules out empty recognition and forces nontrivial structure.
Here an observable is the minimal carrier of that idea: a real-valued readout on states. Sibling notions in the same file (distinction, comparison mechanisms, recognition events) build on this map. Upstream, related value maps appear in the primitive recognition calculus as evaluations of certified analytic protocols and transformers to reals; this structure is the abstract counterpart used in the necessity argument rather than a concrete registry evaluation.
proof idea
No proof body. The declaration is a structure with one field value : StateSpace → ℝ. It packages the textbook notion of a real observable on an arbitrary state type and introduces no axioms or lemmas of its own.
why it matters
This type is the input language for the necessity chain. Downstream, recognition_necessary takes an observable with two states of unequal value and produces a nonempty recognition pair. The master theorem recognition_forcing_complete quantifies over all such observables: any non-constant observable forces a recognition structure, and every extraction mechanism yields one. A parallel Observable structure appears in RecognitionForcing and feeds the same forcing results.
In the broader framework this sits under the recognition-forcing half of the T0–T8 chain (analytic recognition refinement T4 and related exclusivity arguments). It is also reused in astrophysics observability limits and K-gate falsifiers wherever a real readout on configurations is needed. Core definitions are complete; main theorems remain modulo deep measurement-theory hypotheses, with no axioms beyond the Meta Principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.