Observable
plain-language theorem explainer
Observable assigns a real number to each state in type S. It is cited in the recognition forcing completeness theorem and in astrophysics observability limits. The definition is a direct structure with one field.
Claim. An observable on a state space $S$ is a map $value : S → ℝ$.
background
The RecognitionForcing module proves recognition is forced by the cost foundation. Observable here extracts a real value from states, distinct from the abbrev in Measurement.RSNative.Core (S → Measurement α) and the self-adjoint operator in Quantum.Observables. Upstream results include the ILG action S and spin value, which supply the broader measurement context.
proof idea
Direct structure definition with single field value : S → ℝ.
why it matters
Supplies the observable type for the master theorem recognition_forcing_complete, which shows non-constant observables force recognition structures. It feeds recognition_necessary and OptimalConfig. Connects to the forcing chain T0-T8 and the Recognition Composition Law via cost minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.