QualityEquiv
plain-language theorem explainer
QualityEquiv declares two display channels equivalent precisely when their stateQuality maps induce identical orderings on the shared state space. Workers on order preservation and channel interchange in recognition models cite it to equate observation projections without altering optimality conclusions. The declaration is a direct biconditional abbreviation on pairwise quality comparisons.
Claim. Two display channels $C_1$ and $C_2$ are quality-equivalent if for all states $x,y$ one has $C_1.stateQuality(x) ≤ C_1.stateQuality(y) ↔ C_2.stateQuality(x) ≤ C_2.stateQuality(y)$.
background
A display channel is a structure carrying an observation map State → Obs together with a real-valued quality function Obs → ℝ. The stateQuality operation composes these maps to produce a direct real-valued quality on states. The module presents channels as distinct projections or observations of the same underlying state space.
proof idea
As an abbreviation the declaration directly encodes the biconditional on the orderings induced by the two stateQuality functions. No lemmas or tactics are invoked; the definition itself supplies the equivalence predicate used by the surrounding theorems.
why it matters
QualityEquiv supplies the relation that optimal_iff and optimal_transfer invoke to equate optimal states across channels. It also grounds the equivalence-relation theorems refl, symm and trans, and is re-exported as ChannelEquiv in the glossary. In the Recognition framework it supports consistency conditions by permitting interchangeable observation channels while preserving induced orderings on states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.