Observable
Observable equips any state type S with a real-valued extraction map. Researchers on recognition forcing cite it to connect cost minima to measurable distinctions. The structure is introduced by direct definition with a single field and no supporting lemmas.
claimAn observable on a state space $S$ is a function $value : S → ℝ$.
background
The RecognitionForcing module shows that recognition structures are forced by the underlying cost foundation. Recognition events carry a ratio whose associated J-cost vanishes exactly when the ratio equals 1 and is strictly positive otherwise, via the identity J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The present Observable supplies the extraction map that turns state distinctions into real numbers for use in those cost calculations.
proof idea
The declaration is a direct structure definition consisting of a single field value : S → ℝ. No lemmas are invoked and no tactics are required.
why it matters in Recognition Science
Observable is the interface used by recognition_forcing_complete to conclude that any observable with at least two distinct values forces a nonempty Recognize relation. It thereby completes the step from cost structure to recognition necessity inside the T0–T8 forcing chain. The same structure appears in recognition_necessary and in the falsifier registry for K-gate mismatch.
scope and limits
- Does not attach units or semantic labels to the extracted real value.
- Does not enforce self-adjointness or operator properties required in the quantum setting.
- Does not connect the value map to the phi-ladder or mass formulas.
- Does not specify how the extracted value enters the J-cost computation.
formal statement (Lean)
84structure Observable (S : Type) where
85 value : S → ℝ
86