QualityEquiv
plain-language theorem explainer
QualityEquiv declares two display channels equivalent precisely when their stateQuality functions induce identical orderings on the shared state space. RRF workers on consistency and optimality transfer cite it to interchange observation models without changing recognized states. The abbrev is the direct biconditional on the pairwise inequalities.
Claim. Two display channels $C_1$ and $C_2$ (from a common state space to possibly different observation spaces) are quality-equivalent when, for every pair of states $x,y$, the inequality $C_1.stateQuality(x) ≤ C_1.stateQuality(y)$ holds if and only if $C_2.stateQuality(x) ≤ C_2.stateQuality(y)$.
background
A DisplayChannel is the structure with an observe map State → Obs and a quality map Obs → ℝ. The stateQuality definition composes these maps to produce the real-valued quality function on states. The module presents display channels as the basic mechanism for projecting states into observation spaces where quality is assessed.
proof idea
The declaration is the primitive definition of the relation; it directly encodes the biconditional on stateQuality comparisons with no lemmas or tactics applied.
why it matters
It supplies the hypothesis for optimal_iff (quality-equivalent channels share optimal states) and for the equivalence relation theorems refl, symm, trans. It is re-exported as ChannelEquiv in the Glossary and used by optimal_transfer in OrderPreservation. Within RRF this relation lets distinct observation channels be substituted while preserving the ordering that determines recognized states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.