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