stateQuality
plain-language theorem explainer
stateQuality composes the observation and quality maps of a DisplayChannel to yield a real-valued function on states. RRF researchers cite it when defining optimality or comparing quality orderings across channels. The definition is a direct functional composition with no further steps.
Claim. For a display channel $C$ with observation map $observe : State → Obs$ and quality map $quality : Obs → ℝ$, the induced state quality is $quality ∘ observe : State → ℝ$.
background
The DisplayChannel structure pairs an observation map from states to an observation space with a quality map from observations to reals. This lets any state be projected and scored without reference to the underlying state representation.
proof idea
One-line definition that returns the composition of the quality and observe fields from the DisplayChannel structure.
why it matters
stateQuality supplies the quality function used by isOptimal and QualityEquiv in the same module and by the transfer theorems channel_quality_transfer and channel_mono_transfer. It therefore anchors the ordering and optimality arguments that connect RRF channels to the eight-tick octave and D = 3 steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.