trans
plain-language theorem explainer
Quality equivalence of display channels is transitive. Researchers working with chained observation projections in RRF models would cite this result when composing channels. The proof is a one-line term that chains the two biconditionals via transitivity of logical equivalence on the induced state orderings.
Claim. Let $C_1$, $C_2$, $C_3$ be display channels sharing a common state space. If $C_1$ and $C_2$ induce identical orderings on states via their composed quality functions and $C_2$ and $C_3$ induce identical orderings, then $C_1$ and $C_3$ induce identical orderings.
background
A display channel consists of an observation map from states to an observation space together with a real-valued quality function on observations. The composed state quality is obtained by applying the quality function after the observation map. Quality equivalence is the relation that holds precisely when two channels produce the same preorder on states under this composed quality measure.
proof idea
The proof is a one-line term that applies transitivity of the biconditional: for arbitrary states x and y the ordering equivalence supplied by the first hypothesis is chained with the ordering equivalence supplied by the second hypothesis.
why it matters
The result completes the demonstration that quality equivalence is an equivalence relation on display channels, supporting downstream statements about optimal states and global optimality by permitting channel composition without altering the induced ranking. It sits inside the RRF core module whose purpose is to furnish consistent observation projections for the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.